zero_param_forces_unit_coefficients

formal source

  83/-- Minimal integer coefficients (1,1) are forced by the zero-parameter
  84posture. This is `HierarchyForcing.additive_composition_is_minimal`
  85restated in the bridge context. -/
  86theorem zero_param_forces_unit_coefficients
  87    (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b)
  88    (hmin : max a b = 1) :
  89    a = 1 ∧ b = 1 :=
  90  additive_composition_is_minimal a b ha hb hmin
  91
  92/-! ## Step 6a: Unit Coefficients → Fibonacci Relation -/
  93
  94/-- Integer recurrence with unit coefficients reduces to the
  95Fibonacci relation L₂ = L₁ + L₀. -/
  96theorem unit_coefficients_give_fibonacci
  97    (L : UniformScaleLadder)
  98    (a b : ℕ) (ha : a = 1) (hb : b = 1)
  99    (hrec : L.levels 2 = (a : ℝ) * L.levels 1 + (b : ℝ) * L.levels 0) :
 100    L.levels 2 = L.levels 1 + L.levels 0 := by
 101  have ha_real : (a : ℝ) = 1 := by exact_mod_cast ha
 102  have hb_real : (b : ℝ) = 1 := by exact_mod_cast hb
 103  have h1 : (a : ℝ) * L.levels 1 = L.levels 1 := by rw [ha_real, one_mul]
 104  have h2 : (b : ℝ) * L.levels 0 = L.levels 0 := by rw [hb_real, one_mul]
 105  linarith
 106
 107/-! ## Step 6b: Fibonacci → Golden Equation → φ -/
 108
 109/-- The golden equation σ² = σ + 1 follows from minimal integer
 110recurrence on a uniform scale ladder. -/
 111theorem minimal_recurrence_forces_golden_equation
 112    (L : UniformScaleLadder)
 113    (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b)
 114    (hrec : L.levels 2 = (a : ℝ) * L.levels 1 + (b : ℝ) * L.levels 0)
 115    (hmin : max a b = 1) :
 116    L.ratio ^ 2 = L.ratio + 1 := by