TMinus1_AbsoluteFloor
plain-language theorem explainer
Compatibility alias that re-exports the T-1 absolute-floor proposition into the public T-1–T8 spine. Anyone citing the forcing chain bottom (distinguishability floor below the Law of Logic) uses this name. The body is a pure universe-polymorphic abbrev of the TMinus1ToT1Bridge structure; no new proof content.
Claim. T-1 (absolute floor) is the proposition that the absolute distinguishability floor is closed: there exists a certificate that meta-language proposition distinguishability and a non-singleton universe of discourse hold. This declaration is only a public alias of that proposition.
background
The module exposes the public theory-only forcing spine from T-1 through T8, stopping before private operator and measurement layers. T-1 is the bottom rung: absolute distinguishability floor.
Upstream, the same name is a Prop-structure with a single field closure : AbsoluteFloorClosureCert. UnifiedForcingChain states the content: the chain bottoms out at two preconditions of statability itself (meta-language proposition distinguishability and a non-singleton universe of discourse), the floor below the Law of Logic. The T-1→T1 bridge module packages that closed certificate as the chain start.
Sibling aliases in this file (Boolean recognition-work cost, T0 logic forced, T1 meta-principle) likewise re-export the first bridge so the full T-1–T8 spine can be cited from one module.
proof idea
No proof. One-line abbrev that fixes universe parameters {0, 0} and points at TMinus1ToT1Bridge.TMinus1_AbsoluteFloor. All mathematical content lives in that structure and in the upstream AbsoluteFloorClosure certificate.
why it matters
Anchors the public complete forcing chain. Downstream, CompleteForcingChainT8 and CompleteForcingChain carry a tminus1 field of this type; tminus1_holds supplies an inhabitant; tminus1_to_t0_bridge consumes a floor witness to build the T0 Boolean cost interface; TMinus1ToT1Cert bundles T-1 with the T0/T1 bridges.
In the Recognition Science primer this is the start of the forcing chain before T5 J-uniqueness, T6 φ, T7 eight-tick, and T8 D = 3. Without a named T-1 floor the spine has no stated bottom. The honesty note on CompleteForcingChainT8 records that T5 uniqueness does not actually depend on T-1–T4 proofs; the alias still keeps the public narrative order intact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.