T5_To_T6_SelfSimilarity_Bridge
plain-language theorem explainer
Packages the T5→T6 bridge certificate: given J-cost uniqueness, five fields record that realized self-similar hierarchies force the scale ratio to equal φ. Forcing-spine authors cite it when wiring T6 into the public T−1..T8 chain. It is a Prop-structure (definitional interface), discharged downstream by t5_to_t6_bridge_holds rather than proved here.
Claim. Given the T5 package (uniqueness of the canonical reciprocal cost $J(x)=(x+x^{-1})/2-1$), the bridge asserts: (1) any $F:\mathbb{R}\to\mathbb{R}$ obeying Aczél smoothness, reciprocity, normalization, the composition law, calibration, and continuity on $(0,\infty)$ equals $J$ pointwise on positives; (2) every realized hierarchy on a closed observable framework has scale ratio $\varphi$; (3) every self-similar ratio satisfies the golden-ratio constraint; (4) the unique positive solution of that constraint is $\varphi$; (5) every self-similar discrete-ledger ratio equals $\varphi$.
background
This module exposes the public theory-only T−1 through T8 forcing spine. T5 is uniqueness of the canonical reciprocal recognition cost $J$; T6 is that $\varphi$ is forced by a realized self-similar hierarchy. The structure is indexed by a T5 uniqueness hypothesis so the $\varphi$ layer cannot float free of cost uniqueness.
The cost $J(x)=(x+x^{-1})/2-1$ is the unique continuous positive-ratio cost satisfying reciprocity $J(x)=J(x^{-1})$, normalization $J(1)=0$, the Recognition Composition Law, and calibration $\lim_{t\to 0} 2J(e^t)/t^2=1$. The shifted form $H=J+1$ converts RCL into d'Alembert's equation. Aczél smoothness upgrades continuous d'Alembert solutions to $C^\infty$, enabling the classification that pins $J$.
Self-similarity and discrete ledgers live in the PhiForcing layer: a ratio $r>0$ is golden when it solves the fixed-point constraint that forces $r=\varphi=(1+\sqrt{5})/2$. HierarchyDynamics supplies the internal theorem that a closed observable framework equipped with a realized hierarchy has ladder ratio $\varphi$.
proof idea
No proof body: this is a structure definition packaging five Prop fields. Downstream, t5_to_t6_bridge_holds fills the fields by direct projection and named lemmas: t5_uniqueness_available is h5.uniqueness; internal_hierarchy_forces_phi is HierarchyDynamics.bridge_T5_T6_internal; self_similar_forces_golden is PhiForcing.self_similar_forces_golden_constraint; uniqueness of the golden constraint and the discrete-ledger ratio identity are discharged by the corresponding PhiForcing lemmas. The structure itself only states the interface.
why it matters
This is the T5→T6 bridge certificate on the public forcing spine (primer landmark: T5 J-uniqueness, T6 $\varphi$ as self-similar fixed point). Downstream, T5_To_T6_Forced_Bridge consumes it as the self_similarity field and exposes the T6 theorem surface, so T6 is produced from the bridge rather than inserted independently. The same shape is re-exported in UnifiedForcingChain, whose doc states the bridge routes through the internal hierarchy-dynamics theorem and records the formal obstruction: bare ClosedObservableFramework fields alone do not force hierarchy data (ratio_self_similar, additive_posting).
The honesty note on the preceding T4→T5 arrow still matters contextually: T5 uniqueness is proved from CostUniqueness and law_of_logic_forces_jcost, not from the T−1..T4 floor; the continuous comparison surface remains an imported hypothesis. This T5→T6 package does not close that gap. It does lock the $\varphi$ step to T5 so the chain cannot skip cost uniqueness when claiming golden-ratio forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.