refactor: introduce reduced Step-1 frontier and related theorems

[beanapologist]

Note

Medium Risk
Moderate risk because it rewires core assumption packaging (Step1ApproximationFrontier -> Step1ReducedFrontier) and endpoint proofs/bridges, which could break downstream lemmas if any equivalence or instantiation is wrong.

Overview
Introduces Step1ReducedFrontier (four independent clauses) and proves a bidirectional equivalence Step1ApproximationFrontier ↔ Step1ReducedFrontier, then updates the endpoint route to assume Step1ReducedFrontier_assumption and derive the full frontier when needed.

Adds a lattice-native phase-lock transfer interface PhaseLockLatticeBridge, shows it is equivalent to the legacy window-limit bridge, and updates WindowLimitFrontier instantiation to use the new bridge wiring. Separately adds small coherence/defect utilities (coherence_lt_one, RH_defect/RH_defectC and related equivalences) and refreshes the .lake/lakefile.olean.trace config hash.

^{Reviewed by Cursor Bugbot for commit f732889. Bugbot is set up for automated code reviews on this repo. Configure here.}

[cursor]

Cursor Bugbot has reviewed your changes and found 2 potential issues.

^{❌ Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, enable autofix in the Cursor dashboard.}

^{Reviewed by Cursor Bugbot for commit f732889. Configure here.}

[cursor]

Chained iff statement is mathematically false at h=1

Medium Severity

The theorem RH_defect_off_equilibrium_bundle states (0 < RH_defectC h) ↔ (h ≠ 1) ↔ (coherenceC h < 1), but this is provably false when h = 1 (with hh = zero_lt_one). Since coherenceC 1 = 1, we get RH_defectC 1 = 0, making the left clause False. Under either associativity of ↔, the overall proposition evaluates to False. The docstring intends pairwise equivalence of three conditions, which requires a conjunction of two separate iffs rather than chaining ↔.

 

^{Reviewed by Cursor Bugbot for commit f732889. Configure here.}

[cursor]

New theorem inserted before its dependency definition

High Severity

The newly inserted phase_lock_lattice_bridge_holds at line 3812 calls phase_lock_from_F_lattice_limit, which is defined later at line 3844. In Lean 4, declarations cannot reference identifiers that appear later in the file. The new block of code (lines 3801–3840) was inserted between phase_lock_from_window_limit and phase_lock_from_F_lattice_limit, creating a forward reference that prevents compilation.

Additional Locations (1)

• RH.lean#L3843-L3850

 

^{Reviewed by Cursor Bugbot for commit f732889. Configure here.}