meta_language_distinguishes_props
plain-language theorem explainer
The formal language already distinguishes at least two propositions. Researchers closing the absolute-floor argument cite this result to separate meta-level facts from object-level claims. The proof exhibits the pair True and False and derives a contradiction from their equality by substitution into True.intro followed by falsehood elimination.
Claim. There exist propositions $P$ and $Q$ such that $P ≠ Q$.
background
The declaration belongs to the SelfBootstrapDistinguishability module, which records the Lean-checkable meta-level facts for Route A of the absolute-floor program. The module establishes that the formal language distinguishes propositions and that the object-level distinguishability claim differs from its negation. Upstream results supply supporting definitions such as IntegrationGap.A (active edge count per fundamental tick, equal to 1) and Masses.Anchor.A (coherence energy unit), though the present theorem uses only the underlying Prop type.
proof idea
A tactic proof constructs the witness pair True and False. It assumes their equality, substitutes to obtain False from True.intro, and eliminates the resulting falsehood.
why it matters
The theorem supplies the meta_distinguishes field for absolute_floor_of_bare_distinguishability (which states that bare distinguishability supplies the nontrivial specification part of the absolute-floor witness) and for selfBootstrapCert. It anchors the meta-language half of Route A in the Recognition Science self-bootstrap argument, ensuring the formal system already provides non-trivial distinctions before object-level non-singleton conditions are imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.