bool_distinction_from_nothing
plain-language theorem explainer
Two distinct Boolean values exist: false and true. The nothing-to-distinction certificate cites this as the Boolean instance of forced distinction in the shape the object floor consumes. The proof is a one-line term that exhibits the pair and discharges inequality by decidability.
Claim. There exist Boolean values $x$ and $y$ such that $x \neq y$. Explicitly, $\mathrm{false} \neq \mathrm{true}$.
background
The module closes the floor below the Recognition Science forcing chain (T-2 to T-1). Absolute nothing is encoded as the empty type: no inhabitants, unique map into every type. Naming that empty type already populates a higher universe, and comparing the initial object to the terminal object yields a first inequality of types.
From that first distinction the module derives type-level, propositional, and object-level distinctions with no extra premises. The Boolean case is the concrete two-valued instance: the type of truth values carries two canonical constructors that are definitionally unequal. The absolute-floor layer previously took meta-language distinguishability as given; this file discharges those preconditions from the empty type alone.
proof idea
Term-mode existence proof. The witnesses are the two Boolean constructors false and true. Inequality is closed by decide, which runs the decidable equality instance on Bool and confirms they differ. No lemmas from the forcing chain are required; the statement is pure type theory.
why it matters
Feeds nothingToDistinctionCert, which packages universe population, type distinction, propositional distinction, object distinction, and this Boolean distinction into a single theorem-backed certificate. The module doc states that the forced Boolean distinction is exactly the floor consumed by the public T-1 through T8 bridge. Closing this step means the absolute floor no longer assumes meta-language distinguishability; it is derived from Empty. The later spine (J-uniqueness, phi, eight-tick octave, D = 3) sits above this certificate and is not imported here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.