t5_to_analytic_refinements_bridge_holds
plain-language theorem explainer
From T5 uniqueness of the recognition cost, every analytic alias of J used in the T0–T4 scaffolding is forced equal to the canonical closed form, and the five analytic refinements attach. Anyone wiring the complete forcing chain cites this bridge. The proof applies T5 uniqueness to each named cost, discharges pointwise identities by definitional equality, and links the discreteness log-cost via the cosh identity.
Claim. Assume the unique-cost package: reciprocity, normalization, the Recognition Composition Law, calibration, and continuity force $J(x)=\frac12(x+x^{-1})-1$ on $(0,\infty)$. Then the analytic-refinement bridge holds: uniqueness applies to the canonical cost and to the Law-of-Existence and Ledger-Forcing analytic names; those names agree pointwise with the canonical cost; the discreteness log-cost equals the exponential form of the canonical cost; and the T0–T4 analytic refinements hold.
background
The Unified Forcing Chain module shows that T-1 through T8 are forced from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). T5 is the uniqueness step: those axioms plus continuity determine the closed form $J(x)=\frac12(x+x^{-1})-1$ on $(0,\infty)$, equivalently $\cosh(\log x)-1$.
Earlier chain steps (logic, MP, discreteness, ledger, recognition) also speak in analytic $J$-names: Law-of-Existence $J$, Ledger-Forcing $J$, and Discreteness-Forcing $J_{\log}$. The bridge certificate packages the claim that T5 uniqueness forces those names onto the same closed form, and that the T0–T4 analytic refinements therefore sit on a single forced cost.
Upstream, reciprocal symmetry $J(x)=J(x^{-1})$ is the algebraic double-entry identity; the composition law is the RCL functional equation. The bridge consumes the full T5 uniqueness field rather than only collecting definitional equalities.
proof idea
Tactic construction of the bridge structure, field by field.
For the three uniqueness fields, introduce an Aczel smoothness package and a positive $x$, then apply the T5 uniqueness theorem to the target cost (canonical $J$, Law-of-Existence $J$, or Ledger-Forcing $J$), feeding reciprocity, normalization, composition, calibration, and continuity. For the two analytic aliases, simpa rewrites those five properties along the definitional identification with the canonical cost.
The three pointwise equalities (Law-of-Existence, defect, Ledger-Forcing versus canonical cost) are pure rfl. The discreteness identity rewrites $J_{\log}(t)=\cosh t-1$ and applies the library fact that the exponential form of the canonical cost is $\cosh t-1$. The five T0–T4 refinement fields are one-line citations of the already-proved analytic refinement theorems.
why it matters
This is the T5-to-analytic-scaffolding link inside the complete inevitability chain. Downstream, complete_forcing_chain assembles T-1 through T8 by threading bridges; this declaration is the explicit hypothesis discharge that lets later steps treat every analytic $J$-name as the unique forced cost rather than an independent assumption.
Framework landmark: T5 J-uniqueness, $J(x)=\frac12(x+x^{-1})-1=\cosh(\log x)-1$, forced by RCL plus normalization and calibration. Without the bridge, T0–T4 analytic refinements would float free of the uniqueness theorem. With it, the closed-form identities of the analytic scaffolding become consequences of T5, so the chain from cost foundation through unique $J$ is continuous before T6 forces $\varphi$ as the self-similar fixed point.
Doc-comment summary: the analytic-refinement bridge follows from T5 plus the closed-form identities of the analytic $J$-scaffolding. No open scaffold remains here; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.