prop_distinction_forced
plain-language theorem explainer
Propositional distinction is forced: there exist unequal propositions. Anyone building the absolute-floor witness or the nothing-to-distinction certificate cites this fact. The proof is a short term that exhibits True and False and shows that identifying them would transport a proof of True into False.
Claim. There exist propositions $P$ and $Q$ such that $P \neq Q$. Concretely $\mathrm{True} \neq \mathrm{False}$, since any equality would transport the canonical proof of $\mathrm{True}$ into a proof of $\mathrm{False}$.
background
This module closes the T-2 to T-1 floor of Recognition Science: it derives the meta-language preconditions that AbsoluteFloorClosure previously assumed. Absolute nothing is encoded as the empty type (the initial object): no inhabitants, and a unique map into every type.
Naming nothing writes that empty type, which itself has type Type, so the act of denoting nothing populates the universe. Once the universe is inhabited one also has the terminal type; empty and terminal cannot be identified, because transport would move the terminal inhabitant into the empty type. From that first distinction the module derives type-level, object-level, and propositional distinctions with no premises.
The propositional form—existence of unequal propositions—is exactly the meta-language fact that the absolute-floor witness took as a precondition. This declaration discharges that precondition from nothing rather than assuming it.
proof idea
Pure term-mode existence proof; no external lemmas. Witnesses are True and False. Inequality is shown by assuming an equality h and rewriting: transport along h sends the canonical proof of True (trivial) to an inhabitant of False, which is impossible. The argument is ordinary equality transport in Prop.
why it matters
Supplies the propositional half of the T-2/T-1 closure. It fills the meta_distinguishes field of absolute_floor_from_nothing, which builds an absolute-floor witness for Bool with the precondition now derived from nothing. It is also the prop_distinction component of nothingToDistinctionCert, the theorem-backed certificate for the whole module.
By discharging the meta-language distinguishability that AbsoluteFloorClosure previously took as given, the result closes the last open floor below the Recognition Science forcing chain (T0 through T8). The Boolean distinction that follows is the floor consumed by the public T-1–T8 bridge; this file itself stays at T-2/T-1 and does not import the later spine.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.