NothingToDistinctionCert
plain-language theorem explainer
Joint certificate packaging every distinction forced by encoding absolute nothing as the empty type: nonempty Type, distinct types, distinct propositions, distinct objects, Boolean inequality, and an absolute-floor witness on Bool. Anyone citing the T-2→T-1 floor or the full T-2→T8 bridge uses this bundle. As a Prop-structure it is pure packaging; the companion theorem fills each field from the forced lemmas.
Claim. A certificate asserting: the universe of types is inhabited; there exist types $\alpha\neq\beta$; there exist propositions $P\neq Q$; there exist a type $\alpha$ and objects $x\neq y$ in $\alpha$; there exist Booleans $b_1\neq b_2$; and an absolute-floor witness for $\mathrm{Bool}$ holds (meta-language distinguishability of propositions together with a nontrivial specification of $\mathrm{Bool}$).
background
This module closes the floor beneath the Recognition Science forcing chain (T-2 → T-1). Absolute nothing is encoded as the empty type: no inhabitants, unique map into every type (the initial object). Naming that empty type already places an object in Type, so the universe is populated. From the empty type versus the unit type one obtains the first inequality, and from it type-level, propositional, and object-level distinctions follow with no extra axioms.
The prior absolute-floor package (AbsoluteFloorWitness K) took meta-language proposition distinguishability and a nontrivial specification of a discourse universe K as given preconditions. The present certificate is designed so that those preconditions become derived conclusions when K = Bool.
Upstream, the canonical Boolean distinction ∃ x y : Bool, x ≠ y is already available as a one-line witness (false, true). The certificate simply records that fact alongside the other forced distinctions and the discharged floor witness.
proof idea
No proof body: this is a Prop-valued structure definition whose six fields are the joint claim. The companion theorem nothingToDistinctionCert constructs an inhabitant by assigning each field to a previously proved lemma (naming_nothing_populates_universe, type_distinction_forced, prop_distinction_forced, object_distinction_forced, bool_distinction_from_nothing, and the absolute-floor witness on Bool). The structure itself only names the interface.
why it matters
This certificate is the public T-2→T-1 hand-off. Downstream, nothingToDistinctionCert proves the structure is inhabited, and CompleteForcingChainTMinus2ToT8 takes a field tminus2_to_tminus1 : NothingToDistinctionCert as the starting leg of the full forcing spine through T8 (J-uniqueness, φ fixed point, eight-tick octave, D = 3). By packaging universe population, all three distinction levels, Boolean distinction, and the discharged absolute-floor witness in one Prop, later bridge theorems can cite a single object rather than a scattered list of lemmas. It closes the last open precondition that earlier absolute-floor work had left as a meta-language assumption.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.