t1_holds_eq_routed
plain-language theorem explainer
Standalone T1 (cost forbids infinite price; MP/existence side) is identical, as theorem content, to the T1 corollary taken along the routed T-1→T0 bridge. Forcing-chain auditors cite this to lock the two presentations together. Proof is one-line subsingleton elimination (proof irrelevance on the shared Prop).
Claim. The proposition ``T1 holds'' is equal to the T1-corollary of T0 applied to the T0 surface obtained from the absolute-floor-to-T0 bridge certificate. In other words, the direct T1 certificate and the bridge-routed corollary certificate are the same theorem content.
background
Module UnifiedForcingChain builds the complete inevitability spine from the cost foundation (Recognition Composition Law, normalization, calibration): T-1 absolute floor, then T0 logic from cost minimization, then T1, and onward through unique $J$, $\phi$, eight-tick, and $D=3$.
T1 is the MP/existence step forced by cost: nothing is assigned infinite cost. Upstream, the defect functional of the law of existence is the scalar $J$ on positive reals (defect at unity vanishes). The routed path builds T0 from the T-1 bridge, then applies a T1-corollary-of-T0 constructor so T1 is not an independent axiom.
This declaration sits after those certificates exist and only compares them. Sibling holdings (tminus1_holds, t0_holds, and the analytic T1 refinement) are the live spine objects; the equality is audit glue between the standalone and routed surfaces.
proof idea
Term proof: Subsingleton.elim _ _. Both sides inhabit the same proposition type (the T1 holding certificate). In Lean every Prop is a subsingleton, so any two proofs are equal. No algebraic unfolding of $J$, no bridge reconstruction, and no appeal to RCL identities is required; the term only discharges proof irrelevance once the types match.
why it matters
In the Complete Inevitability Chain the module claims every level T-1 through T8 is forced from cost, not merely compatible. T1 is the first post-logic cost consequence (``nothing has infinite cost''). Routing T1 as a corollary of the bridged T0 surface prevents placing existence/MP payload before cost uniqueness later in the spine (the analytic T1 refinement comment makes that ordering explicit).
This equality is audit-grade bookkeeping: it certifies that the standalone T1 holds' surface and the routed corollary surface carry identical content, so downstream readers cannot fork the chain by picking one presentation over the other. No used_by' edges are recorded; the value is local integrity of the forcing spine rather than a new lemma consumers rewrite with. Framework landmarks touched: the T0→T1 segment of the T-1..T8 forcing chain and the cost-foundation axiom bundle (RCL + normalization + calibration).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.