TMinus1_AbsoluteFloor
plain-language theorem explainer
Absolute floor (T-1) is the Prop that packages the closed certificate making the forcing chain statable at all: meta-language proposition distinguishability and a non-singleton universe of discourse. Anyone citing the complete T-1 through T8 inevitability spine, or the T-1→T0 cost bridge, starts from this record. It is a one-field structure whose sole content is the joint absolute-floor closure certificate.
Claim. The absolute-floor stage $T_{-1}$ holds precisely when the joint absolute-floor closure certificate is present. That certificate bundles (i) self-bootstrap of the meta-language, (ii) for every nonempty type $K$, the equivalence between existence of distinct elements of $K$ and existence of a nontrivial specification on $K$, and (iii) a Boolean absolute-floor witness.
background
The Unified Forcing Chain module claims that T0 through T8 are forced from the cost foundation (Recognition Composition Law, normalization $F(1)=0$, calibration $F''(1)=1$), rather than merely compatible with it. The chain is written
$T_{-1}\to T0\ (\mathrm{logic})\to T1\ (\mathrm{MP})\to\cdots\to T8\ (D=3)$.
$T_{-1}$ sits below the Law of Logic. It records preconditions of statability itself: that the meta-language can distinguish propositions, and that the universe of discourse is not a singleton. Without those, no later cost or ledger statement can even be written.
Upstream, the joint closure certificate packages three pieces: a self-bootstrap certificate for the meta-language; a universal equivalence linking nontriviality of a nonempty type $K$ to existence of a nontrivial specification on $K$; and an absolute-floor witness on Bool, which supplies the minimal object-level configuration space for the Boolean recognition-work cost used by the T0 interface.
proof idea
No proof body: this is a Prop-valued structure definition with a single field. Inhabiting it means exhibiting the joint absolute-floor closure certificate. Downstream theorems such as tminus1_holds fill that field by applying the already-constructed absolute-floor closure certificate from AbsoluteFloorClosure.
why it matters
This is the formal bottom of the Complete Inevitability Chain. The T-1→T1 bridge certificate requires it as its first field; the T-1→T0 bridge theorem consumes an absolute-floor inhabitant to extract the Boolean floor witness, floor configuration, and Boolean recognition-work cost that seed T0 (logic from cost minimization). The full T-1 through T8 spine (CompleteForcingChainT8) likewise opens with this record.
In framework terms it is the stage below T0 in the forcing chain primer: everything from unique $J$ (T5), forced $\varphi$ (T6), the eight-tick octave (T7), and $D=3$ (T8) is only meaningful once the chain is statable. An honesty note on the T8 spine records that T5 uniqueness does not consume T-1..T4 content; T-1 still anchors the public narrative that the chain bottoms out rather than floating on an assumed logic layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.