hasIdentityStep
The predicate asserts that a realization of the law of logic has at least one carrier element whose comparison cost to the zero element is nonzero. Workers extracting arithmetic from logical structures cite this predicate as the starting point for deriving addition and multiplication. The definition is the direct existential statement over the carrier and comparison operation.
claimFor a realization $R$ with carrier set $C$, zero element $0$, and comparison cost function $d$, the identity-step condition holds if there exists $x$ in $C$ such that $d(x, 0) ≠ 0$.
background
A LogicRealization consists of a carrier type, a cost type equipped with zero, a comparison function from pairs of carriers to costs, a distinguished zero carrier, a step function on the carrier, an orbit type, and orbit zero and step operations. This structure supplies a setting-independent interface for the Universal Forcing program, allowing distinct Law-of-Logic settings (continuous positive ratios, discrete propositions, categorical structures) to map into one common object. The invariant target is the arithmetic object extracted from the identity and step data rather than the ambient carrier itself.
proof idea
The declaration is a direct definition of the predicate as the existence of a carrier element x satisfying compare x zero ≠ 0.
why it matters in Recognition Science
This predicate supplies the minimal non-triviality data from which ArithmeticOf extracts arithmetic in the Universal Forcing program. It is invoked to establish the property for the boolean realization and the positive-ratio realization. It fills the role of the identity-step shadow required before arithmetic can be realized from any Law-of-Logic setting.
scope and limits
- Does not assert that every realization satisfies the condition.
- Does not specify the algebraic structure of the carrier or cost.
- Does not derive addition or multiplication from the predicate.
- Does not address continuity or discreteness of the carrier.
formal statement (Lean)
69def hasIdentityStep (R : LogicRealization) : Prop :=
proof body
Definition body.
70 ∃ x : R.Carrier, R.compare x R.zero ≠ 0
71