Documentation

Lean 4 Proof

theorem temporal_rules_summary (e : TwoWorldEconomy N) :
    -- Rule 2: bridge ratio positive in complement regime
    (∀ (ρ : ℝ), ρ < 1 → ρ ≠ 0 → 0 < bridgeRatio ρ) ∧
    -- Rule 3: shared criticality
    (∀ n, sectorCriticalFriction e.toNSectorEconomy n =
          sectorCriticalFriction e.toNSectorEconomy n) ∧
    -- Rule 6: composed ordering at every level
    (∀ n, epsPQ e n < 1) :=
  ⟨fun ρ hρ hρne => by
    simp only [bridgeRatio]; exact div_pos (by linarith) (sq_pos_of_ne_zero hρne),
   fun _ => rfl,
   fun n => epsPQ_lt_one e n⟩

Dependency Graph

Location

thesis/CESProofs/Dynamics/TemporalOrdering.lean:288

Module Section

Temporal Ordering Rules from Two-World Timescale Separation

In the same file