structure
definition
def or abbrev
SelfSimilar
show as:
view Lean formalization →
formal statement (Lean)
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 -/