IdentityOn
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not enforce non-contradiction or scale invariance.
- Does not assume Archimedean or Dedekind completeness.
- Does not construct the comparison operator from the functional equation.
- Does not derive any field isomorphism.
formal statement (Lean)
65def IdentityOn [Zero K] [LT K] (C : ComparisonOperatorOn K) : Prop :=
proof body
Definition body.
66 ∀ x : K, 0 < x → C x x = 0
67
68/-- Non-contradiction, generic field version. -/