bool_absolute_floor
plain-language theorem explainer
Bool serves as the minimal concrete carrier realizing the absolute-floor witness. A researcher closing the base case of the forcing chain would cite this result when instantiating the general witness on the Boolean type. The proof is a one-line term application of absolute_floor_of_bare_distinguishability to the explicit distinction between false and true together with meta-language distinguishability of propositions.
Claim. The Boolean type satisfies the absolute-floor witness: there exist propositions $P$ and $Q$ with $P ≠ Q$, and the type of non-trivial specifications over Bool is inhabited.
background
The absolute-floor witness for a type K is the structure requiring meta_distinguishes (existence of distinct propositions P, Q) and nontrivial_specifiable (Nonempty (NontrivialSpecification K)). The module states that distinguishability is equivalent to non-trivial specifiability on an inhabited carrier, while the meta-language already distinguishes propositions; the remaining floor is therefore the precondition of a non-singleton universe of discourse. The upstream lemma absolute_floor_of_bare_distinguishability states that bare distinguishability supplies the non-trivial specification part of the witness while the meta-language part is theorem-backed.
proof idea
The proof is a one-line term wrapper that applies absolute_floor_of_bare_distinguishability to the concrete distinction ⟨false, true, bool_distinguishable⟩ on Bool.
why it matters
This declaration closes the absolute-floor program by exhibiting the minimal carrier Bool. It feeds absoluteFloorClosureCert (which assembles the joint certificate with selfBootstrapCert and distinguishability_iff_nontrivial_specifiability) and reality_from_one_distinction (the master forcing chain). Within the framework it anchors the T0 base, confirming the absolute floor is the precondition of a non-singleton universe rather than an RS-specific postulate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 3 of 3)
-
Mathematics builds from zero and one as absence and presence
"Axioms of the Binary Principle... unit composition... Arithmetic and Logic as One System"
-
Discrete memories unify federated time-series models
"align cross-domain memories to promise the unified discrete latent space... domain-specific memory update"
-
Linear cellular automata controllable exactly when matrix is invertible
"The Jacobian Jij = ∂s′i/∂sj … in case of linear rules ∂si(T)/∂sj(0)=(J^T)ij"