bool_hasIdentityStep
plain-language theorem explainer
The Boolean realization of the Law-of-Logic satisfies the identity-step condition required to extract arithmetic. Researchers testing discrete models against Universal Forcing cite this to confirm propositional carriers meet the same minimal nontriviality requirement as continuous ones. The proof is a direct one-line application of the general hasIdentityStep_of_nontrivial lemma to boolRealization.
Claim. Let $R$ be the Boolean realization with carrier type Bool. Then there exists an element $x$ in the carrier such that the comparison cost $R.compare(x, R.zero)$ is nonzero.
background
The module DiscreteLogicRealization supplies the second Law-of-Logic realization: a discrete Boolean/propositional carrier serving as the first non-continuous test case for Universal Forcing. A LogicRealization is the structure carrying a Carrier type, a Cost type with Zero instance, a compare function Carrier → Carrier → Cost, and a distinguished zero element; the structure supplies the data from which arithmetic is later extracted. The predicate hasIdentityStep(R) asserts ∃ x : R.Carrier, R.compare x R.zero ≠ 0; this is the data used by ArithmeticOf.
proof idea
One-line wrapper that applies the upstream theorem hasIdentityStep_of_nontrivial directly to boolRealization.
why it matters
This result verifies that the discrete propositional carrier satisfies the minimal identity-step shadow needed for arithmetic extraction inside the Recognition framework. It supports the Universal Forcing program by furnishing a propositional test case parallel to continuous realizations. The declaration sits in the foundation layer that feeds later extraction of forced arithmetic invariants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.