tminus1_holds
plain-language theorem explainer
The absolute floor (T-1) is established: meta-language proposition distinguishability and a non-singleton universe of discourse sit below the Law of Logic. Anyone citing the complete inevitability chain from T-1 through T8 needs this entry certificate. The proof is a one-field term that installs the absolute-floor closure certificate.
Claim. The absolute-floor claim holds: there is a certified absolute-floor closure witnessing meta-language proposition distinguishability together with a non-singleton universe of discourse (the floor below the Law of Logic).
background
The Unified Forcing Chain module aims to show that every level T0 through T8 is forced from the cost foundation (Recognition Composition Law, normalization, calibration), rather than merely compatible with it. The chain is stated only after a still lower precondition: T-1, the absolute floor.
T-1 packages two preconditions of statability itself: that the meta-language can distinguish propositions, and that the universe of discourse is not a singleton. The structure is a proposition whose sole field is an absolute-floor closure certificate. Upstream, that certificate is already theorem-backed: it records a self-bootstrap route, a distinguishability-versus-nontrivial-specifiability route, and a Boolean absolute-floor witness.
Locally this sits strictly below T0 (logic forced by cost minimization). The Boolean configuration space that the floor supplies (empty/consistent versus marked-inconsistent) is what later bridges use as the minimal object-level cost interface.
proof idea
One-line term proof. The structure for the absolute-floor claim has a single field closure; the proof fills it with the upstream theorem that the absolute-floor closure certificate holds (self-bootstrap route, distinguishability route, and Boolean witness). No further tactics or algebraic reduction.
why it matters
This is the bottom rung of the complete inevitability chain. Downstream, the T-1-to-T0 bridge takes the floor certificate and builds the minimal Boolean cost/consistency interface; the public T-1-to-T1 certificate and the full T-1-to-T8 forcing chain both begin by invoking this theorem. Inside the same module it feeds complete_forcing_chain and the T-1-to-T0 bridge lemmas.
Framework-wise it is the precondition that makes the forcing ladder (T0 logic, T1 MP, T2 discreteness, through T5 unique J, T6 phi, T7 eight-tick, T8 D=3) statable at all. Without a certified absolute floor, the stronger claim that every level is forced from cost would have a gap at the meta-language boundary. It does not itself derive phi or the constants; it only locks the floor so those later steps can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.