t5_to_canonical_existent_bridge_holds
plain-language theorem explainer
Under T5 (unique J-cost from RCL, reciprocity, normalization, calibration), the unique RS-existent real is exactly 1, nothing near zero is RS-existent, and consistent configurations hit cost 0 only at ratio 1. Forcing-chain and spine-to-extras authors cite this bridge certificate. The proof is a term-mode structure fill that wires existing ontology and LogicFromCost lemmas into the bridge fields.
Claim. Assume $J$ is the unique cost on $(0,\infty)$ fixed by reciprocity, normalization $J(1)=0$, the Recognition Composition Law, calibration, and continuity, so $J(x)=\frac12(x+1/x)-1$. Then $1$ is RS-existent; for all real $x$, $x$ is RS-existent if and only if $x=1$; there is a unique RS-existent; values near $0$ are not RS-existent; and every consistent configuration has nonnegative cost, with cost zero precisely when its ratio equals $1$ (and such a zero-cost consistent configuration exists).
background
The Unified Forcing Chain module shows T-1 through T8 as forced from the cost foundation (RCL plus normalization and calibration), not merely compatible with it. T5 is the uniqueness step: those hypotheses pin $J(x)=\frac12(x+1/x)-1$ on $(0,\infty)$.
RS-existence is the ontology predicate that a positive real is a legitimate recognition-scale witness (defect-bounded). The bridge replaces a legacy $\exists!$ surface by a canonical iff: the only RS-existent value is $1$. Separately, LogicFromCost treats consistent configurations and their cost (a defect of the ratio): minimum cost is $0$, achieved exactly at ratio $1$, and zero-cost consistent configs exist.
Upstream, consistent_minimum_cost states cost $\ge 0$ with equality iff ratio $=1$; consistent_zero_cost_possible exhibits a witness; nothing_not_rs_exists is the operational content of "Nothing cannot recognize itself" (an $\varepsilon$-neighborhood of $0$ contains no RS-existent).
proof idea
Term-mode structure construction for T5_To_CanonicalExistent_Bridge, not a fresh analytic argument. Each field is discharged by an existing lemma:
one_rs_exists←OntologyPredicates.rs_exists_oners_exists_iff_one←rs_exists_unique_oneunique_existent_legacy←rs_exists_uniquenothing_not_rs_exists← the same-named ontology theorem- cost nonnegativity and zero-at-ratio-one ← the two projections of
LogicFromCost.consistent_minimum_cost - legacy zero-cost existence ←
consistent_zero_cost_possible
The hypothesis T5_J_Unique is carried only as the bridge parameter; the cited lemmas already encode the T5 cost minimum at $1$.
why it matters
This is the T5 → canonical unique-existent certificate in the complete inevitability chain. Downstream, spine_to_extras_bridge_holds sources t5_forces_unique_existent and zero-cost consistency from this bridge (alongside the T5→canonical-reference bridge). complete_forcing_chain threads it into the unconditional T-1…T8 package, and ultimate_inevitability_extended exposes the extended canonical surface (gap-45, $D=3$, cyclic shift) on top of that package.
Framework landmark: T5 J-uniqueness, $J(x)=\cosh(\log x)-1$, is what forces the unique zero of the cost and therefore the unique RS-existent at the identity ratio. Without this bridge the spine still has abstract $\exists!$ statements; with it the chain names the canonical value $1$ and the nothing-boundary, which later steps (T6 $\varphi$, ledger calibration, constants) treat as fixed reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.