absolute_floor_from_nothing
plain-language theorem explainer
The absolute-floor witness on Bool is obtained with its meta-language precondition discharged from absolute nothing, not assumed. Anyone citing the T-2/T-1 closure or the Nothing-to-Distinction certificate needs this. The proof is a term that packs propositional distinction forced from Empty with the preexisting Bool nontrivial-specifiability field.
Claim. There is an absolute-floor witness on $\mathrm{Bool}$: propositional distinguishability $\exists P,Q:\mathrm{Prop},\, P\neq Q$ holds by derivation from absolute nothing, and $\mathrm{Bool}$ admits a nontrivial specification.
background
This module sits at T-2 $\to$ T-1, the floor beneath the Recognition Science forcing chain (T0–T8). Absolute nothing is encoded as the empty type $\mathrm{Empty}$: no inhabitants, unique map into every type. Naming $\mathrm{Empty}$ already populates $\mathrm{Type}$, and $\mathrm{Empty}\neq\mathrm{Unit}$ is the first distinction; type-, object-, and propositional distinctions then follow with no premises.
An absolute-floor witness for a nonempty carrier $K$ is a structure with two fields: meta-language proposition distinguishability $\exists P,Q:\mathrm{Prop},,P\neq Q$, and a nonempty nontrivial specification of $K$. The prior absolute-floor module took the meta field as a given precondition and showed that $\mathrm{Bool}$ realizes the floor once bare distinguishability is granted.
Here the meta field is supplied by the derived fact that $\mathrm{True}\neq\mathrm{False}$ (equality would transport a proof of $\mathrm{True}$ into $\mathrm{False}$). That is exactly the precondition the earlier floor assumed.
proof idea
Term-mode construction of the absolute-floor witness structure on $\mathrm{Bool}$. The meta-distinguishes field is filled by the already-proved propositional distinction $\exists P,Q,,P\neq Q$ forced from nothing. The nontrivial-specifiable field is copied from the preexisting Bool absolute-floor theorem, which already packages a nontrivial specification of $\mathrm{Bool}$ once bare distinguishability is available. No new tactics or algebraic work; it is a structure pack of two upstream results.
why it matters
Closes the last open precondition under the absolute floor: meta-language proposition distinguishability is no longer an assumption but a theorem from the encoding of absolute nothing. Downstream, the joint Nothing-to-Distinction certificate consumes this witness together with universe population, type/object/Bool distinctions, all derived in the same module.
In the broader framework this is the T-2/T-1 step that feeds the public T-1 through T8 bridge. The forced Boolean distinction is the carrier the later spine (J-uniqueness, $\varphi$, eight-tick octave, $D=3$) sits on. The module deliberately does not import that later spine; it only discharges the floor those steps consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.