140theorem bridge_T5_T6 141 (L : UniformScaleLadder) 142 (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b) 143 (hrec : L.levels 2 = (a : ℝ) * L.levels 1 + (b : ℝ) * L.levels 0) 144 (hmin : max a b = 1) : 145 L.ratio = φ := by
proof body
Term-mode proof.
146 have ⟨ha1, hb1⟩ := zero_param_forces_unit_coefficients a b ha hb hmin 147 have hfib := unit_coefficients_give_fibonacci L a b ha1 hb1 hrec 148 exact hierarchy_emergence_forces_phi L hfib 149 150/-! ## Structure-Based Interface 151 152For downstream code that prefers a bundled representation. -/ 153 154/-- A uniform scale ladder with local binary recurrence: the level 155at position k+2 is determined by a linear combination of levels k+1 156and k with positive integer coefficients. 157 158Physical motivation: in a discrete ledger, composing a recognition event 159at level k+1 with one at level k produces an event at level k+2. The 160coefficients count how many sub-events of each type participate. Since 161the ledger is discrete, these counts are positive natural numbers. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.