IdentityOn
plain-language theorem explainer
IdentityOn encodes the identity axiom for a comparison operator on an ordered field, requiring that the operator returns zero when applied to any positive element with itself. Researchers deriving the real line from the Law of Logic would cite this predicate when assembling the minimal conditions on the comparison operator. The definition consists of a direct universal quantification with no lemmas or reductions.
Claim. Let $K$ be a linearly ordered field and let $C$ be a comparison operator on $K$. The identity condition holds when $C(x,x)=0$ for every positive element $x$ of $K$.
background
The DomainBootstrap module supplies the comparison-operator domain for the Law of Logic stated in LogicAsFunctionalEquation. ComparisonOperatorOn is the type of binary maps $K→K→K$ on a linearly ordered field. The module recovers that any ordered field supporting the full set of conditions is canonically isomorphic to the reals via the classical uniqueness of the Archimedean Dedekind-complete ordered field.
proof idea
The declaration is a definition whose body is the predicate itself: universal quantification over positive elements of $K$ with the requirement that the comparison operator returns zero on the diagonal. No lemmas are invoked and no tactics are applied.
why it matters
IdentityOn supplies the identity field of the LogicSupported structure, which packages the four Aristotelian conditions together with scale invariance and distinguishability. This structure is the immediate parent that feeds the bootstrap theorem identifying the ambient field with the reals. The definition therefore closes one link in the chain from the functional equation to the uniqueness of the ordered field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.