tminus1_to_t0_bridge_holds
plain-language theorem explainer
The absolute-floor level (T-1) bridges non-vacuously to logic-from-cost (T0): the Boolean floor yields a normalized two-point recognition cost whose zeros are exactly the consistent configurations, so classical logic emerges by cost minimization. Anyone citing the complete forcing chain or the routed T0–T2 corollaries needs this edge. The proof is an explicit structure witness built from the Bool absolute-floor certificate and the CostFromDistinction dichotomy lemmas.
Claim. There is a bridge certificate from the absolute floor (T-1) to logic-from-cost (T0): the Boolean absolute-floor witness induces a canonical two-point floor normalization, a Boolean configuration interface, and a unit-normalized recognition-work cost $C$ satisfying dichotomy ($C(\Gamma)=0$ iff $\Gamma$ is consistent) and independent additivity, from which the T0 payload (consistency is cheap, contradiction is expensive, logic emerges, additive independence) follows.
background
The Unified Forcing Chain module claims that every level T-1 through T8 is forced from the cost foundation (Recognition Composition Law plus normalization and calibration). T-1 is the absolute floor: a meta-language with proposition distinguishability and a non-singleton universe of discourse. The concrete carrier is Bool, via the theorem that Bool realizes an absolute-floor witness from bare distinguishability of false and true.
A cost function on a configuration space obeys two axioms: dichotomy (cost vanishes exactly on consistent configurations) and independent additivity (cost adds over joins of configurations that share no predicates). The T-1 → T0 bridge is the missing non-vacuous edge in older aggregates: the absolute floor supplies a Boolean distinction; that distinction carries a recognition-work cost with dichotomy and additivity; the existing LogicFromCost T0 payload is then reached through this cost/consistency interface.
Locally, the bridge structure packages the Boolean floor witness, its canonical two-point normalization, the extracted configuration and cost interfaces, the recognition-work constraint, the zero-on-consistency identity, the positive-cost-iff-inconsistent direction, and the nested T0 logic-forced record.
proof idea
Term-mode explicit record literal for the bridge structure. The Boolean floor field is the upstream absolute-floor theorem on Bool. The normalized floor is obtained by applying the canonical two-point floor normalization to that witness. Configuration and cost interfaces are the corresponding extraction maps from the same witness. Recognition work is the Boolean recognition-work constraint; floor consistency at zero is definitional (rfl). The positive-cost-iff-inconsistent field is the CostFromDistinction dichotomy lemma specialized to the Boolean recognition cost.
The nested T0 payload is read off the normalized floor: recognition work and the cheap-consistency / expensive-contradiction / logic-emergent clauses come from the normalized floor's cost record (zero on empty, positive iff inconsistent, zero iff consistent); additive independence is the additivity field of the Boolean recognition cost.
why it matters
This is the concrete T-1 → T0 edge that makes the complete inevitability chain start below logic rather than assuming logic. Downstream, the routed T0 surface is definitionally identified with the standalone T0 theorem via this bridge; T1 (Meta-Principle from cost) and T2 (discreteness) are then obtained as corollaries by chaining T0→T1 and T1→T2 bridges through the same witness. The complete forcing chain structure records this bridge as a required field between the absolute-floor level and T0.
In the primer landmarks, this sits before T5 (J-uniqueness), T6 (φ), T7 (eight-tick), and T8 (D=3): without a cost-derived logic floor, the later forcing steps have no grounded starting point. The doc-comment notes the witness is extensionally identical to the universe-routed form used inside the bundled complete chain; the explicit literal exists only to pin universes at the top level. No open scaffold remains: claim status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.