discrete_fibonacci_from_minimality

formal source

 157
 158This theorem proves that natural-number coefficients with
 159`max(a, b) = 1` forces the Fibonacci recurrence. -/
 160theorem discrete_fibonacci_from_minimality
 161    (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b) (hmin : max a b = 1) :
 162    a = 1 ∧ b = 1 := by
 163  constructor
 164  · exact Nat.le_antisymm (by omega) ha
 165  · exact Nat.le_antisymm (by omega) hb
 166
 167/-! ## Complete Posting-Extensivity Bridge -/
 168
 169/-- **End-to-end theorem**: From the forced RCL combiner structure
 170(specifically, the d'Alembert identity on posting potentials),
 171a geometric scale sequence closed under additive posting, with
 172discrete minimal coefficients, forces φ.
 173
 174This chains the entire derivation:
 175  RCL → posting d'Alembert → additive closure → golden equation → φ -/
 176theorem posting_extensivity_forces_phi
 177    (L : UniformScaleLadder)
 178    (closure : L.levels 2 = L.levels 1 + L.levels 0) :
 179    L.ratio = PhiForcing.φ :=
 180  hierarchy_emergence_forces_phi L closure
 181
 182/-! ## Posting-Derived Recurrence Data
 183
 184Instead of assuming `HasAdditiveComposition` or `HasDiscreteAdditiveComposition`,
 185we provide the recurrence data directly from posting extensivity. -/
 186
 187/-- The additive closure gives recurrence coefficients (1, 1). -/
 188theorem posting_gives_unit_recurrence
 189    (L : UniformScaleLadder)
 190    (closure : L.levels 2 = L.levels 1 + L.levels 0) :