ledgerCompose_assoc

formal source

  89  unfold ledgerCompose; ring
  90
  91/-- Composition is associative -/
  92lemma ledgerCompose_assoc (a b c : ℝ) :
  93    ledgerCompose (ledgerCompose a b) c = ledgerCompose a (ledgerCompose b c) := by
  94  unfold ledgerCompose; ring
  95
  96/-! ## Axiom 3: Closure Under Composition
  97
  98The composed scale must be in the scale sequence.
  99For a geometric sequence, this means 1 + r must equal some rⁿ.
 100-/
 101
 102/-- A scale sequence is closed if composing the first two scales
 103    gives the third scale (minimal closure condition) -/
 104def GeometricScaleSequence.isClosed (S : GeometricScaleSequence) : Prop :=
 105  ledgerCompose (S.scale 0) (S.scale 1) = S.scale 2
 106
 107/-! ## The Main Derivation -/
 108
 109/-- **THEOREM**: Closure forces the golden ratio equation.
 110
 111If a geometric scale sequence is closed under additive composition,
 112then the ratio r must satisfy r² = r + 1. -/
 113theorem closure_forces_golden_equation (S : GeometricScaleSequence)
 114    (h_closed : S.isClosed) : S.ratio ^ 2 = S.ratio + 1 := by
 115  -- Unfold the closure condition
 116  unfold GeometricScaleSequence.isClosed at h_closed
 117  unfold ledgerCompose at h_closed
 118  unfold GeometricScaleSequence.scale at h_closed
 119  -- h_closed : r^0 + r^1 = r^2
 120  -- This simplifies to: 1 + r = r^2
 121  simp only [pow_zero, pow_one] at h_closed
 122  -- Rearrange to r^2 = r + 1