IndisputableMonolith.Foundation.SelfBootstrapDistinguishability
The module shows that the two-element type carries a definitional distinction, which bootstraps distinguishability for the Recognition Science foundation without external postulates. It is cited by AbsoluteFloorClosure as the base for the absolute-floor certificate. The module assembles lemmas that start from Bool and lift the distinction to propositions and inhabited carriers.
claimThe two-element type $\mathbf{2}$ admits a definitional distinction between its elements, which lifts to propositions via the meta-language and to non-trivial specifiability on inhabited carriers.
background
The module lies in the Foundation domain and imports only Mathlib. It introduces lemmas around distinguishability that begin with the two-element type Bool. Key supporting results include bool_distinguishable, which records the definitional inequality of the two constructors, and distinguishability_lifted_from_bool, which extends the fact to other types.
The theoretical setting treats distinguishability as equivalent to non-trivial specifiability on an inhabited carrier. The meta-language already distinguishes propositions, so the construction requires no additional RS-specific assumption. This matches the modest closure described in the downstream AbsoluteFloorClosure documentation.
proof idea
The module is a collection of short lemmas rather than a single theorem. bool_distinguishable supplies the base case by direct appeal to the constructors of Bool. Subsequent results such as distinguishability_lifted_from_bool, prop_ne_not, and dist_claim_self_distinguishes apply simple lifting and self-reference arguments to reach the meta-language level. No complex tactics appear.
why it matters in Recognition Science
This module supplies the self-bootstrap mechanism required by AbsoluteFloorClosure. The downstream documentation states that the closure is deliberately modest because distinguishability is equivalent to non-trivial specifiability on an inhabited carrier and the meta-language already distinguishes propositions. The remaining floor is therefore not an RS-specific physical postulate but a precondition of the meta-language.
scope and limits
- Does not introduce any RS-specific physical postulates.
- Does not claim distinguishability for empty or uninhabited types.
- Does not connect to the phi-ladder, mass formulas, or forcing chain T0-T8.
- Does not address spatial dimensions or constants such as alpha.