IdentityOn
plain-language theorem explainer
IdentityOn defines the identity property for a comparison operator C on an ordered field K by requiring C(x,x)=0 for every positive x. Researchers assembling the bootstrap of the Law of Logic cite it when stating the Aristotelian conditions on the comparison operator inside LogicSupported. The definition is a direct universal quantification with no auxiliary lemmas.
Claim. Let $K$ be a field with zero and strict order. For a comparison operator $C:K→K→K$, the identity property holds if and only if $∀x∈K$, $0<x$ implies $C(x,x)=0$.
background
DomainBootstrap moves from the Law of Logic (stated with a comparison operator $C:ℝ→ℝ→ℝ$ in LogicAsFunctionalEquation) to a generic ordered-field setting. ComparisonOperatorOn is the abbrev $K→K→K$ that supplies the operator type on any linearly ordered field $K$. The upstream Constants.K supplies the dimensionless bridge ratio $φ^{1/2}$, while the module doc notes that the ambient field must later be shown isomorphic to $ℝ$ under Archimedean and Dedekind-completeness hypotheses.
proof idea
Direct definition whose body is the single quantified statement $∀x:K, 0<x → C x x =0$. No tactics or upstream lemmas are applied; the declaration simply names this predicate.
why it matters
IdentityOn supplies the identity clause inside the LogicSupported structure, which packages the four Aristotelian conditions plus scale invariance and distinguishability. That structure is the immediate parent that feeds bootstrap_closure and the uniqueness theorem showing any such field is canonically $ℝ$. It therefore closes one of the four required conditions in the generic-field version of the comparison operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.