pith. sign in
theorem

phi_unique_self_similar

proved
show as:

Self-similar closure forces the golden ratio: r² = r + 1.

module
IndisputableMonolith.Foundation.PhiForcing
domain
Foundation
line
186 · github
papers citing
3 papers (below)

plain-language theorem explainer

The golden constraint r² = r + 1 forces the scale ratio to equal the golden ratio φ among all positive reals. Researchers deriving self-similar discrete ledgers from J-cost would cite this uniqueness when closing the forcing chain to φ. The proof is a one-line application of the algebraic uniqueness theorem for the quadratic.

Claim. Let $r > 0$ satisfy the golden constraint $r^2 = r + 1$. Then $r = \phi$, where $\phi = (1 + \sqrt{5})/2$.

background

The PhiForcing module shows that self-similarity in a discrete ledger with J-cost forces φ. The predicate satisfies_golden_constraint r is defined as r² = r + 1; this encodes the requirement that scaling by r composes as r · r = r + 1 in ledger terms, arising from the Fibonacci-like structure of the ledger.

The local setting is given by the module argument: a discrete ledger admits self-similar scales only when the ratio satisfies the golden constraint, and the only positive solution is φ. This rests on upstream results including golden_constraint_unique (the algebraic uniqueness of the positive root) and the definitions of J-cost and LedgerForcing imported from prior modules.

proof idea

One-line wrapper that applies golden_constraint_unique to the hypotheses 0 < r and satisfies_golden_constraint r.

why it matters

This theorem is invoked by phi_harmonic_forced and the matching uniqueness result in FrequencyLadder. It supplies the uniqueness step in the Phi Forcing chain (self-similar ledger implies ratio = φ), directly supporting the framework landmark that φ is forced as the self-similar fixed point (T6). It closes the algebraic part of the argument that scale ratios in the eight-tick octave must be φ.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.