bool_hasIdentityStep
The Boolean realization of the Law-of-Logic structure satisfies the identity-step condition required to extract arithmetic. Discrete-model researchers cite this as the first non-continuous test case for Universal Forcing. The proof is a direct one-line application of the general nontriviality lemma to the Boolean carrier.
claimThe Boolean realization with carrier $B = $ {true, false} and zero element false satisfies $R.hasIdentityStep$, i.e., there exists $x : B$ such that the comparison cost of $x$ to false is nonzero.
background
The module introduces the second Law-of-Logic realization as a discrete Boolean carrier, serving as the first non-continuous test case for Universal Forcing. A LogicRealization consists of a carrier type, a cost type with zero, a comparison function, and a distinguished zero element; the structure supplies the data from which arithmetic is later extracted. The predicate hasIdentityStep on a realization R is the proposition that there exists an element x in the carrier with R.compare x R.zero nonzero. The concrete boolRealization sets the carrier to Bool, the cost to Nat, the zero to false, and the comparison to the sibling boolCost function.
proof idea
One-line wrapper that applies the theorem hasIdentityStep_of_nontrivial directly to boolRealization, which itself reduces to the nontrivial field carried by every LogicRealization instance.
why it matters in Recognition Science
This theorem confirms that the discrete Boolean carrier meets the minimal identity-step requirement for arithmetic extraction inside the Recognition framework. It supplies the first non-continuous example in the Universal Forcing program and supports the transition from continuous to discrete realizations along the forcing chain. No downstream uses are recorded yet, leaving open how the extracted arithmetic will be compared with the continuous case.
scope and limits
- Does not compute the explicit nonzero cost value for the identity step.
- Does not address periodic or modular carriers that may lack the step.
- Does not derive the full arithmetic invariants or the Recognition Composition Law.
- Does not compare the Boolean case with the continuous realization.
formal statement (Lean)
67theorem bool_hasIdentityStep : boolRealization.hasIdentityStep :=
proof body
Term-mode proof.
68 LogicRealization.hasIdentityStep_of_nontrivial boolRealization
69
70/-- Boolean realization has the same forced arithmetic as every realization. -/