T5_To_AnalyticRefinements_Bridge
plain-language theorem explainer
Certificate structure linking T5 uniqueness of the reciprocal cost to the five analytic refinements of T0–T4. It records that Law-of-Existence, ledger, and discreteness J-names coincide with the canonical closed form, and packages the T0–T4 analytic payloads under an explicit T5 hypothesis. Downstream CompleteForcingChain and the companion holds theorem cite it. As a Prop structure it is definitional packaging, not a proved theorem.
Claim. Given a T5 uniqueness certificate for $J(x)=\frac{1}{2}(x+x^{-1})-1$ on $(0,\infty)$, the bridge asserts: under the Aczél smoothness package, uniqueness applied to the canonical cost and to the Law-of-Existence and ledger $J$ names; the pointwise identities $\mathrm{LawOfExistence}.J=J_{\mathrm{cost}}$, $\mathrm{defect}=J_{\mathrm{cost}}$, $\mathrm{Ledger}.J=J_{\mathrm{cost}}$, and $J_{\log}(t)=J_{\mathrm{cost}}(e^{t})$; and the five analytic refinement packages for T0–T4.
background
The Unified Forcing Chain module aims to show T-1 through T8 as forced from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$). T5 is the uniqueness step: those hypotheses plus continuity force $J(x)=\frac12(x+x^{-1})-1$ on $(0,\infty)$, equivalently $\cosh(\log x)-1$.
Before uniqueness is available, several modules introduce analytic names for the same closed form: Law-of-Existence $J$ and defect, LedgerForcing $J$, and DiscretenessForcing $J_{\log}$ in log coordinates. The five $T*\mathrm{Analytic}*\mathrm{Refinement}$ structures preserve older LogicFromCost / MP / discreteness / ledger / recognition payloads without placing the closed form before uniqueness on the spine.
The Aczél smoothness package supplies the classical fact that continuous d'Alembert solutions are $C^\infty$, which T5 uniqueness consumes. Canonical $J_{\mathrm{cost}}$ is the shared closed form $(x+x^{-1})/2-1$.
proof idea
This declaration is a Prop-valued structure (definitional certificate), not a theorem with a proof body. Fields fall into three groups: (1) uniqueness applications that force the bridge to consume the T5 uniqueness field under Aczél smoothness rather than mere definitional equality of $J_{\mathrm{cost}}$ with itself; (2) closed-form identities equating Law-of-Existence $J$/defect, LedgerForcing $J$, and $J_{\log}(t)$ with $J_{\mathrm{cost}}$ (or $J_{\mathrm{cost}}(e^t)$); (3) bundled payloads $t0_\mathrm{refinement}$ through $t4_\mathrm{refinement}$.
The companion theorem t5_to_analytic_refinements_bridge_holds constructs an inhabitant from a T5 hypothesis by applying h5.uniqueness and the scaffolding identities; this structure only states the interface that construction must meet.
why it matters
In the forcing chain, T5 is the hinge where the reciprocal cost becomes the unique $J$. Analytic refinements of T0–T4 historically used that closed form in parallel scaffolding. This bridge reattaches those refinements to the spine: they are no longer freestanding analytic layers but consequences recorded under an explicit T5 hypothesis.
CompleteForcingChain consumes the bridge so the full T-1–T8 package can claim that analytic T0–T4 surfaces sit downstream of uniqueness rather than beside it. The companion holds theorem discharges the structure from T5 plus closed-form identities.
Framework landmark: T5 J-uniqueness and the RCL-forced form $J(x)=(x+x^{-1})/2-1$. Without this bridge, the complete chain would either duplicate $J$ definitions or leave analytic refinements unlinked to the uniqueness theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.