hasIdentityStep
plain-language theorem explainer
A definition that isolates the non-triviality condition on a LogicRealization by requiring an element x whose comparison cost to the zero element is nonzero. Workers on discrete or continuous realizations cite this predicate when confirming that their carrier supplies the minimal data for arithmetic extraction. The definition is a direct existential statement over the carrier and the compare operation supplied by the structure.
Claim. For a logic realization $R$, the predicate holds precisely when there exists $x$ in the carrier of $R$ such that the comparison cost of $x$ to the zero element of $R$ is nonzero.
background
A LogicRealization is a structure consisting of a carrier type, a cost type equipped with zero, a compare map from pairs of carrier elements to costs, a distinguished zero element, a step map on the carrier, and orbit data. The structure supplies a setting-independent interface that lets different realizations of the law of logic (continuous positive ratios, discrete propositions, categorical settings) map into a common object whose arithmetic content can be extracted uniformly.
proof idea
One-line definition that states the existence predicate directly from the fields of the LogicRealization structure.
why it matters
The predicate supplies the non-triviality condition used by downstream results to verify that the boolean realization and the positive-ratio realization both possess the identity-step shadow. It therefore feeds the extraction of arithmetic from any realization and sits in the foundation layer that supports the Universal Forcing program. The module doc-comment states that the invariant target is the arithmetic object extracted from the identity/step data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.