hasIdentityStep_of_nontrivial
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not construct concrete realizations or verify their structural laws.
- Does not address periodic or modular carriers that may fail faithfulness.
- Does not compute explicit values for costs or orbits.
- Does not connect to the J-cost or phi-ladder directly.
Lean usage
theorem bool_hasIdentityStep : boolRealization.hasIdentityStep := LogicRealization.hasIdentityStep_of_nontrivial boolRealizationformal statement (Lean)
72theorem hasIdentityStep_of_nontrivial (R : LogicRealization) :
73 R.hasIdentityStep :=
proof body
Term-mode proof.
74 R.nontrivial
75
76/-- A realization whose internal forced arithmetic embeds faithfully into its
77ambient carrier. Periodic realizations, such as modular carriers, need not
78satisfy this; their internal orbit is still free while the carrier
79interpretation is periodic. -/