hasIdentityStep_of_nontrivial
plain-language theorem explainer
Any LogicRealization R equipped with a nontrivial field satisfies the identity-step condition: there exists a carrier element x such that its comparison cost to the zero element is nonzero. Workers on discrete boolean realizations and continuous positive-ratio realizations cite this to establish the starting point for arithmetic extraction. The proof is a one-line field projection.
Claim. Let $R$ be a LogicRealization. Then $R$ has an identity step: there exists $x$ in the carrier of $R$ such that the comparison cost of $x$ to the zero element of $R$ is nonzero.
background
The module supplies a setting-independent interface for the Universal Forcing program. Different Law-of-Logic settings map into the common LogicRealization object, which carries a carrier type, comparison cost with zero, zero element, step action, and orbit data. The hasIdentityStep predicate extracts the minimal data needed for arithmetic: the existence of a nonzero comparison from some element to zero. Upstream, the definition of hasIdentityStep itself states this existence condition directly.
proof idea
The proof is a one-line wrapper that applies the nontrivial field of the input LogicRealization R.
why it matters
This declaration is invoked by bool_hasIdentityStep to show the discrete realization has an identity step and by positiveRatio_hasIdentityStep for the continuous case. It fills the role of ensuring every realization supplies the identity-step shadow from which ArithmeticOf extracts arithmetic, supporting the common interface for the Universal Forcing program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.