TMinus1_AbsoluteFloor
plain-language theorem explainer
T-1 packages the absolute floor of distinguishability as a single Prop: possession of the joint absolute-floor closure certificate. Anyone citing the start of the RS forcing chain (before T0 logic and the J-cost surface) uses this record. As a structure definition it is just a one-field wrapper around the already-closed AbsoluteFloorClosureCert.
Claim. T-1 (absolute floor) is the proposition that the joint absolute-floor closure certificate holds: self-bootstrap, the equivalence between existence of distinct elements and a nontrivial specification on every nonempty type, and a Boolean absolute-floor witness.
background
This module isolates the first three rungs of the Recognition Science forcing chain without importing the analytic $J$-cost surface. T-1 is the absolute floor of distinguishability; T0 is the minimal recognition-work cost interface; T1 is the cost-form Meta-Principle (inconsistent floor states cannot be selected at zero cost).
The absolute-floor closure certificate is the joint package: a self-bootstrap certificate, a route equating "two distinct elements exist" with a nontrivial specification on every nonempty type, and an absolute-floor witness on Bool. Upstream, UnifiedForcingChain states the same T-1 as the floor below the Law of Logic: meta-language proposition distinguishability plus a non-singleton universe of discourse.
The Boolean witness is the minimal object-level configuration space that later bridges feed into the recognition-work cost on Bool.
proof idea
No proof body: this is a Prop-valued structure with a single field closure of type AbsoluteFloorClosureCert. Inhabitation is supplied downstream by tminus1_holds, which fills the field with the closed certificate absoluteFloorClosureCert. Compatibility aliases in TMinus1ToT8Bridge and UnifiedForcingChain re-export the same structure.
why it matters
T-1 is the bottom of the forcing chain (the primer's T0–T8 spine begins one step later at logic). Downstream, tminus1_holds asserts the structure is inhabited; tminus1_to_t0_bridge turns the floor's Boolean witness into the T0 cost interface; TMinus1ToT1Cert and CompleteForcingChainT8 / CompleteForcingChain carry tminus1 as the first field of the public bridge certificates.
The module deliberately stops before analytic $J$. The honesty note on CompleteForcingChainT8 records that T5 uniqueness does not consume the T-1..T4 floor beyond re-export; T-1 still anchors the pre-analytic spine and the Boolean recognition-work split that T0 and T1 require.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.