IndisputableMonolith.Foundation.NothingToDistinction
Module encoding absolute nothing as the empty type and deriving forced distinctions from the act of naming it. Shows that Nothing has no inhabitants, eliminates into any goal, and that naming it populates a universe containing Something, with Nothing ≠ Something. Type-, proposition-, object-, and Boolean-level distinctions follow. Supplies the T-1 absolute distinguishability floor used by the T-1–T8 bridge. Argument is constructive empty-type reasoning plus inhabitation asymmetry.
claimAbsolute nothing is the empty type $\emptyset$ (no inhabitants). Naming $\emptyset$ forces a non-empty counterpart (Something), yields $\emptyset \neq$ Something, and forces distinctions at the levels of types, propositions, objects, and Booleans. Nothing eliminates into any type (ex falso).
background
The absolute-floor program (AbsoluteFloorClosure) treats distinguishability as equivalent to non-trivial specifiability on an inhabited carrier; the meta-language already distinguishes propositions. The remaining floor is therefore not an RS-specific physical postulate but the precondition that there is a coherent empty starting point.
This module supplies that starting point. Absolute nothing is the type with no inhabitants, the strongest encoding of "there is no object." It is kept as a definition (not an abbreviation) so the name does not silently unfold; unfolding is invoked explicitly where needed. Something is the inhabited counterpart. Sibling lemmas record that nothing has no object, that nothing eliminates (ex falso), and that naming nothing populates the universe of discourse.
From the inhabitation asymmetry one obtains forced distinctions: type-level, propositional, object-level, and a Boolean distinction derived from nothing. These are pure type-theoretic facts, not dynamical postulates.
proof idea
Definition-and-lemma module, not a single theorem. Nothing is introduced as the empty type; nothing_has_no_object and nothing_eliminates are the standard no-inhabitant and ex-falso facts. naming_nothing_populates_universe records that referring to Nothing places a named empty type (and thus a contrast class) into the universe. Something is an inhabited type; something_has_object and nothing_ne_something separate the two by inhabitation. type_distinction_forced, prop_distinction_forced, object_distinction_forced, and bool_distinction_from_nothing package the resulting separations at each logical level. No analytic or measure-theoretic machinery is used.
why it matters in Recognition Science
Feeds the public T-1 through T8 forcing spine via TMinus1ToT8Bridge, where T-1 is the absolute distinguishability floor. Also imported by the Foundation aggregator and the root IndisputableMonolith export of the Shape of Logic core.
Without a rigorous empty-type floor, later steps (T0 Boolean recognition-work split, T1 cost-form Meta-Principle, T5 J-uniqueness, T6 phi fixed point, T7 eight-tick octave, T8 D = 3) lack a logical zero point. The module closes the "why is there distinction at all" precondition that AbsoluteFloorClosure states is not an RS-specific physical postulate, so the forcing chain can begin from pure logic rather than an extra axiom.
scope and limits
- Does not derive J-cost, RCL, phi, or any physical constant.
- Does not prove T0–T8; only supplies T-1 floor material.
- Does not address continuum, measure, or spacetime emptiness.
- Does not claim ontological uniqueness beyond type-theoretic emptiness.
- Does not encode dynamics, recognition work, or the eight-tick octave.
used by (3)
depends on (1)
declarations in this module (16)
-
theorem
of -
def
Nothing -
theorem
nothing_has_no_object -
def
nothing_eliminates -
theorem
naming_nothing_populates_universe -
def
Something -
theorem
something_has_object -
theorem
nothing_ne_something -
theorem
type_distinction_forced -
theorem
prop_distinction_forced -
theorem
object_distinction_forced -
theorem
bool_distinction_from_nothing -
theorem
nothingForcesDistinction -
theorem
absolute_floor_from_nothing -
structure
NothingToDistinctionCert -
theorem
nothingToDistinctionCert