T0_Logic_Forced
plain-language theorem explainer
T0 packages the claim that classical logic is not primitive: on the Boolean recognition-work floor, consistency is exactly zero cost and inconsistency is strictly positive cost, with additivity on independent joins. Anyone citing the absolute-floor forcing chain or the T0→T1 Meta-Principle bridge uses this interface. It is a Prop-valued structure bundling five cost axioms, not a proved theorem by itself.
Claim. T0 asserts five properties of the Boolean recognition-work cost $C$: (i) a recognition-work constraint certificate exists on $\mathrm{Bool}$; (ii) $C(\mathsf{false})=0$ (the consistent floor state is free); (iii) every inconsistent Boolean configuration $\Gamma$ satisfies $C(\Gamma)>0$; (iv) $C(\Gamma)=0$ if and only if $\Gamma$ is consistent; (v) if $\Gamma_1$ and $\Gamma_2$ are independent, then $C(\Gamma_1\mathbin{\ast}\Gamma_2)=C(\Gamma_1)+C(\Gamma_2)$.
background
The Unified Forcing Chain module aims to derive T0–T8 as inevitabilities from the cost foundation (Recognition Composition Law, normalization, calibration), starting from an absolute floor rather than assuming logic.
A configuration space supplies an empty config, a join, a consistency predicate, and an independence relation. A cost function $C$ on that space obeys dichotomy (zero cost iff consistent) and independent additivity. The recognition-work constraint certificate packages such a $C$ with calibration and non-vacuity consequences: empty cost vanishes, and some inconsistent config is pinned to a positive cost.
Here the carrier is the Boolean floor from the T−1 absolute-floor witness. The Boolean recognition cost is the minimal pre-analytic cost used before the analytic $J$-cost appears. T0 is the statement that this floor already forces the zero/positive split that classical logic treats as primitive.
proof idea
No proof body: this is a Prop-valued structure (definitional interface). Inhabitants are built by filling the five fields. Downstream, t0_holds constructs one by supplying the Boolean recognition-work certificate, reflexivity for $C(\mathsf{false})=0$, and the cost-function lemma that positive cost is equivalent to inconsistency, together with the dichotomy and independent-additivity fields of the Boolean cost. The structure itself only names the obligations.
why it matters
T0 is the first forced step after the absolute floor in the complete inevitability chain: logic emerges as the zero/positive split of recognition work, rather than being assumed beneath the Meta-Principle. Downstream, the T−1→T1 bridge uses this interface for t0_holds, the T0→T1 bridge, and t1_corollary_of_t0 (T1 follows by reading inconsistency-positive and zero-cost-consistent off T0). The full T−1→T8 certificate also depends on it. Framework landmark: without T0, the chain would still smuggle classical consistency; with it, T1 (nothing has infinite cost / MP) is a corollary of cost dichotomy on the Boolean floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.