T5_To_T6_SelfSimilarity_Bridge
plain-language theorem explainer
Certificate interface from T5 (unique recognition cost J) to T6 (scale ratio forced to φ). It packages hierarchy, closed-scale, admissible-orbit, and recognition-work routes that all force the golden ratio, plus the obstruction that a bare closed framework is too weak. Downstream T5→T6 producer bridges cite it. Definitional Prop bundle; the inhabiting theorem is separate.
Claim. Given T5 uniqueness of the recognition cost $J(x)=\frac12(x+x^{-1})-1$, the T5$\to$T6 self-similarity bridge is the package of statements that: (i) that uniqueness is available under the usual RCL/reciprocity/normalization/calibration/continuity hypotheses; (ii) any closed observable framework with a realized hierarchy (or realized closed-scale model) has ladder ratio equal to $\varphi$; (iii) self-similarity implies the golden constraint $r^2=r+1$, uniquely solved by $\varphi>0$; (iv) recognition-work additivity forces additive scale composition on the nonnegative domain; (v) canonical uniform-scale, growth, and seed-posting data force the multilevel hierarchy ratio to be $\varphi$; together with the matching normal-form and support/quotient certificates.
background
The module builds the complete inevitability chain T−1 through T8 from the cost foundation: Recognition Composition Law, normalization $F(1)=0$, and calibration $F''(1)=1$. T5 asserts uniqueness of the cost $J(x)=\frac12(x+x^{-1})-1$ (equivalently $H(x)=J(x)+1$ satisfying d'Alembert). T6 is the claim that the discrete self-similar scale ratio is the golden number $\varphi$.
A closed observable framework supplies a state space, evolution, and positive scale observable, but not by itself ratio self-similarity or additive seed posting. Realized hierarchy / closed-scale models and admissible-orbit reflection add exactly those fields. The golden constraint is $r^2=r+1$ with $r>0$, whose unique solution is $\varphi$. Multilevel compositions carry level sizes; uniform scale, growth orientation, and seed closure (level $2$ as level $0$ plus level $1$) are the canonical normal-form data that force the hierarchy ratio.
Recognition-work cost from distinction is nonnegative and additive on independent events. On the correct nonnegative domain this forces additive scale composition (ledger compose), linking cost additivity to geometric scale closure used in $\varphi$-forcing.
proof idea
No proof body: this is a structure (definitional Prop interface) indexed by a T5 uniqueness hypothesis. Each field is a named obligation, not a tactic script.
The inhabiting construction is the sibling theorem that builds an instance field-by-field: T5 uniqueness is re-exported from the T5 package; internal and closed-scale $\varphi$-forcing come from hierarchy-dynamics bridges; self-similarity $\to$ golden constraint and uniqueness of the positive root are the standard $\varphi$-forcing lemmas; recognition-work and support/quotient fields are discharged by the cost-from-distinction and nonnegative-work models; multilevel uniform/growth/seed routes reduce to hierarchy forcing plus seed-closed normal form. Treat the structure as the checklist those lemmas jointly satisfy.
why it matters
This is the honest T5→T6 link in the unified forcing chain: T5 unique $J$, T6 $\varphi$ as the self-similar fixed point. The doc-comment stresses the route through internal hierarchy dynamics and the formal obstruction that bare closed frameworks do not force hierarchy fields, so nothing is smuggled past the chain.
Downstream, the producer bridge packages this certificate with the actual T6 theorem surface, so T6 is not inserted independently of T5→T6. The same bridge is re-exported in the T−1-to-T8 bridge module. Framework landmarks: RCL as the single axiom bundle, T5 J-uniqueness, T6 $\varphi$ forced, and the later mass/constants ladder that sits on $\varphi$.
It also records recognition-work and support-event routes that tie seed posting back to cost additivity and the Boolean absolute floor, tightening the story from distinction atoms up to geometric scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.