t3_holds
plain-language theorem explainer
The ledger is forced at the pre-analytic recognition-work floor: empty consistent entries cost zero, empty joins are neutral, and independent joins add costs. Anyone assembling the complete T0–T8 inevitability chain cites this step. The proof is a short term chain that routes the absolute-floor bridge through T0, T1, and T2, then reads off the T3 surface from the T0+T2-to-T3 bridge.
Claim. At the pre-analytic recognition-work floor, the ledger is forced: the empty consistent entry has cost $0$; joining any floor state with the empty configuration leaves the state unchanged and does not change cost; independent joins add costs. (The reciprocal scalar ledger $J(x)=J(1/x)$ is an analytic refinement below this floor.)
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$), not merely compatible with it. In that ladder, T3 is the ledger step: additive bookkeeping of recognition work before the analytic scalar cost is introduced.
T3_Ledger_Forced packages the floor ledger axioms: empty consistent entry has zero recognition cost; empty join is identity on boolean floor configurations; empty join is cost-neutral; and (via the bridge) independent joins add costs. The reciprocal identity $J(x)=J(1/x)$ is recorded as a later analytic refinement, not as the floor statement itself.
Upstream, the canonical T−1→T0 bridge supplies the boolean absolute floor, floor config, and recognition-work constraint. T0 (logic from cost) yields T1 (modus ponens / no infinite cost) and T2 (discreteness: continuous states cannot stabilize). The T0+T2→T3 bridge then assembles ledger neutrality and additivity from floor empty-join, T0 additive independence, and T2 state dichotomy.
proof idea
Term-mode routing, not a fresh calculation. Bind the canonical T−1→T0 bridge, extract forced T0 from it, then obtain T1 from the T0→T1 bridge and T2 from the T1→T2 bridge (still carrying the T−1→T0 bridge data). Finally apply the T0+T2→T3 bridge and project its .t3 field.
That last bridge is the contentful step: it fills empty-join neutrality from the floor config, additivity from T0's independent-cost law, and the floor split from T2's state dichotomy. Everything above is just wiring those hypotheses in order.
why it matters
T3 is the ledger rung in the complete inevitability chain (MODULE_DOC: "Ledger ← Cost symmetry"). Without a forced additive bookkeeping structure on recognition work, later steps (recognition observables, unique $J$, $\varphi$, eight-tick, $D=3$) have nothing discrete to act on.
Downstream, T0_T8_holds_proven in the gravity master theorem includes this theorem as the T3 conjunct of the full T0–T8 package. The sibling audit theorem t3_holds_eq_corollary pins definitional equality between this standalone proof and the corollary applied to the routed T0 and T2 surfaces, so the chain cannot silently fork.
In framework terms this closes the pre-analytic half of the ledger story before T5's unique $J$ (and RCL) take over on the scalar side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.