J_phi

formal source

 120
 121/-- J(φ) = (2φ - 1)/2 - 1 = φ - 3/2 (cost of the golden ratio).
 122    Note: J(φ) ≠ 0 because φ ≠ 1. -/
 123theorem J_phi : LawOfExistence.J φ = φ - 3/2 := by
 124  simp only [LawOfExistence.J]
 125  rw [phi_inv]
 126  ring
 127
 128/-! ## Self-Similarity -/
 129
 130/-- A self-similar structure with scale ratio r. -/
 131structure SelfSimilar where
 132  /-- The scale ratio -/
 133  ratio : ℝ
 134  ratio_pos : 0 < ratio
 135  ratio_ne_one : ratio ≠ 1
 136  /-- Scale invariance is witnessed by a closed geometric scale sequence. -/
 137  scale_invariant :
 138    ∃ S : PhiForcingDerived.GeometricScaleSequence,
 139      S.ratio = ratio ∧ S.isClosed
 140
 141/-- Self-similarity in a discrete ledger requires the scale ratio to satisfy
 142    a specific algebraic constraint: x² = x + 1.
 143
 144    The argument:
 145    - In a self-similar ledger, scaling by r should be composable: r · r = r + 1 (in ledger terms)
 146    - This is because the "next scale" (r²) should equal "current + base" (r + 1)
 147    - The Fibonacci-like structure forces this constraint -/
 148def satisfies_golden_constraint (r : ℝ) : Prop := r^2 = r + 1
 149
 150/-- Closed geometric self-similarity forces the golden constraint. -/
 151theorem self_similar_forces_golden_constraint (S : SelfSimilar) :
 152    satisfies_golden_constraint S.ratio := by
 153  rcases S.scale_invariant with ⟨G, hratio, hclosed⟩