preferred_scale_fixed_point
plain-language theorem explainer
Any self-similarity witness forces its preferred scale s to obey the golden-ratio equation s² = s + 1. Cited by anyone closing the phi-necessity pipeline from discrete scale recurrence. The proof multiplies the recurrence through by the base level, rewrites via the two ratio axioms, then cancels the positive base level.
Claim. Let $S$ be an inhabited type equipped with a self-similarity witness: a preferred scale $s > 1$ and three real levels $\ell_0,\ell_1,\ell_2$ with $\ell_0 > 0$, $\ell_1 = s\,\ell_0$, $\ell_2 = s\,\ell_1$, and $\ell_2 = \ell_1 + \ell_0$. Then $s^2 = s + 1$.
background
The module isolates a minimal self-similarity structure for the inevitability pipeline: enough data to force the golden ratio without committing to a full physical state space. The structure packages a preferred scale $s > 1$ together with three successive levels linked by exact scaling and a linear recurrence.
Concretely, HasSelfSimilarity supplies $\ell_1 = s,\ell_0$, $\ell_2 = s,\ell_1$, and $\ell_2 = \ell_1 + \ell_0$ with $\ell_0 > 0$. The two ratio axioms say consecutive levels differ by the same multiplicative factor; the recurrence says the third level is the sum of the previous two (Fibonacci-style discrete self-similarity).
Algebraic support comes from the foundation layer: associativity and commutativity of addition and multiplication on the primitive recognition integers and on logic naturals, used here only through ordinary real-field rewriting (mul_assoc, right_distrib, etc.).
proof idea
Tactic proof. First record $\ell_0 \neq 0$ from positivity. Build the scaled identity $s^2,\ell_0 = (s+1),\ell_0$ by a five-step calc:
- Expand $s^2,\ell_0$ as $s,(s,\ell_0)$ via
pow_twoand mul reordering. - Replace $s,\ell_0$ by $\ell_1$ using the level-1 ratio.
- Replace $s,\ell_1$ by $\ell_2$ using the level-2 ratio (symmetrized).
- Apply the recurrence $\ell_2 = \ell_1 + \ell_0$.
- Factor $\ell_1 + \ell_0 = (s+1),\ell_0$ via the level-1 ratio and right distributivity.
Apply congrArg (· / ℓ₀) and simplify with $\ell_0 \neq 0$ to cancel the common factor, yielding $s^2 = s + 1$.
why it matters
This is the algebraic heart of phi necessity inside the verification layer. Downstream, phi_result packages the fixed-point equation with positivity and uniqueness against Constants.phi, so any self-similarity witness is forced to the golden ratio.
In the Recognition Science forcing chain this is the local content of T6: phi is the self-similar fixed point. The structure axioms encode discrete scale recurrence (Fibonacci addition of successive levels under a common ratio); the only number compatible with both is the positive root of $x^2 - x - 1 = 0$.
Sibling lemmas (self_similarity_forces_phi, phi_is_mathematically_necessary) lift this identity to the full inevitability claim. No scaffolding remains: the lemma is fully proved and feeds a single private consumer that closes the golden-ratio identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.