t3_holds_eq_corollary
plain-language theorem explainer
Audit-grade equality: the standalone T3 (ledger forcing) certificate coincides with the T3 corollary fed by routed T0 and T2 surfaces. Chain auditors cite it to confirm T3 is not a second independent proof path. Proof is one-line Subsingleton elimination on the two certificates.
Claim. The certificate that T3 (ledger forcing from cost symmetry $J(x)=J(1/x)$) holds is equal, as a proof term, to the T3 corollary applied to (i) the T0 logic-forced surface built from the canonical T$-1\to$T0 bridge and (ii) the T2 discreteness surface obtained as the corollary of T1, itself the corollary of that same T0.
background
The Unified Forcing Chain module claims every level T$-1$ through T8 is forced from the cost foundation (Recognition Composition Law plus normalization and calibration). In that ladder, T3 is ledger forcing: cost symmetry under reciprocal ratios, i.e. the ledger event that swaps source/target and inverts the ratio, matching the reciprocal automorphism of the $J$-cost algebra.
Upstream, the T$-1\to$T0 bridge packages the Boolean absolute floor, its floor config and recognition cost, and the work constraint, with consistency at zero cost. From that bridge one builds the T0 surface (logic forced by cost minimization). T1 (meta-principle: nothing has infinite cost) is a corollary of T0; T2 (discreteness) is a corollary of T1. The T3 corollary then takes those T0 and T2 surfaces and produces the ledger certificate.
Standalone t3_holds is the direct assertion that T3 is forced. This declaration equates that standalone certificate with the fully routed corollary chain, so auditors see a single proof object rather than two competing constructions.
proof idea
Both sides inhabit a subsingleton type (proofs of the same proposition, or a structure whose equality is unique). The term proof is simply Subsingleton.elim _ _, which identifies any two inhabitants. No algebraic rewriting of $J$ or ledger events is performed here; the work is already in t3_corollary_of_t0_t2, t0_from_tminus1_to_t0_bridge, t1_corollary_of_t0, t2_corollary_of_t1, and tminus1_to_t0_bridge_holds.
why it matters
In the Complete Inevitability Chain, T3 is the ledger step forced by cost symmetry $J(x)=J(1/x)$, sitting between T2 (discreteness) and T4 (recognition from ledger plus observables). This equality is an audit seal: it pins the standalone T3 hold to the unique routed path T$-1\to$T0$\to$T1$\to$T2$\to$T3, so the chain cannot silently fork.
It does not itself derive $\varphi$, the eight-tick octave, or $D=3$ (those are T6–T8). It closes the bookkeeping gap that would otherwise let a referee ask whether t3_holds is a second axiom. Downstream use count is currently zero; its role is certification inside the unified chain module rather than a lemma consumed by later physics derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.