- Self-similar closure forces r^2 = r + 1
A geometric scale sequence closed under additive ledger composition (ledgerCompose a b = a + b) requires that the composition of the first two scales equals the third: scale 0 + scale 1 = scale 2. This yields the algebraic constraint 1 + r = r^2, or r^2 = r + 1, as proved by closure_forces_golden_equation and lifted to self-similar structures by self_similar_forces_golden_constraint.
- phi is the unique positive solution
The quadratic equation r^2 = r + 1 has exactly one positive real root, φ = (1 + √5)/2. Uniqueness among positive reals is established by phi_unique_self_similar, which solves the quadratic, discards the negative root, and confirms positivity via phi_pos and phi_gt_one.
- Cited Lean anchors
The forcing of φ follows from the self-similarity axioms in the discrete ledger (DiscreteLedger and SelfSimilar) combined with the above theorems; the full phi_forced statement then concludes that any self-similar discrete ledger has scale ratio φ.