t0_holds
plain-language theorem explainer
At the pre-analytic Boolean floor, logic is forced by recognition-work cost: the consistent state costs zero and every inconsistent state costs positively, with dichotomy and independent additivity. Citers of the Unified Forcing Chain, the T-1→T1 bridge, or the public spine certificate need this T0 pack. The proof is a term-mode structure constructor wiring existing Boolean cost facts and the cost-positive-iff-inconsistent lemma.
Claim. The T0 logic-forced certificate holds on the pre-analytic Boolean recognition-work floor: there is a recognition-work cost on $\mathrm{Bool}$ such that the consistent configuration has cost $0$, every inconsistent configuration has strictly positive cost, cost vanishes if and only if the configuration is consistent, and cost is additive over independent joins.
background
The Unified Forcing Chain module claims T0–T8 are forced from the cost foundation (Recognition Composition Law plus normalization and calibration). T0 is the first analytic step after the absolute floor (T-1): logic is not assumed as a primitive, but read off the zero/positive split of recognition work.
A cost function on a configuration space satisfies dichotomy (cost zero iff the configuration is consistent) and independent additivity (cost adds over joins that share no predicates). Upstream, cost_pos_iff_inconsistent records the positive half of dichotomy: $0 < C(\Gamma)$ if and only if $\Gamma$ is inconsistent. On the Boolean floor the recognition cost is already constructed so that the false (consistent) state has cost zero and the true (inconsistent) state is expensive.
T0 packages those facts as the claim that classical logic emerges from cost minimization: consistency is cheap, contradiction is expensive.
proof idea
Term-mode structure pack, not a tactic script. Recognition-work is filled by the existing Boolean recognition-work constraint certificate. Consistency-cheap is rfl on the Boolean cost at the consistent state. Contradiction-expensive applies cost_pos_iff_inconsistent to the Boolean recognition cost and takes the reverse direction. Logic-emergent and additive-independence are the dichotomy and additivity fields of that same Boolean cost function.
why it matters
T0 is the first forced level in the complete inevitability chain after the absolute floor: logic from cost, not logic as a free assumption. Downstream it is consumed by the T-1→T1 bridge (which lifts T0 to the Meta-Principle), by the public spine certificate, by the routed equality form of T0, by classical-negation impossibility plus unique RS-existent, and by the constants-from-phi path in the same module.
In framework terms this is the T0 landmark of the forcing chain: the zero/positive cost split that makes later steps (discreteness, ledger reciprocity $J(x)=J(1/x)$, unique $J$, $\varphi$, eight-tick, $D=3$) speak a forced logic rather than an imported one. Without this certificate the stronger claim that every level is forced, not merely compatible, does not start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.