truth_eval_implies_identity
plain-language theorem explainer
A truth-evaluable comparison operator C on positive reals satisfies the identity property that C(x,x) equals zero for every x > 0. Researchers formalizing the Reality-to-Logic leg of the functional-equation paper cite this to obtain the base Aristotelian law (L1) directly from the structure axioms. The proof is a one-line term projection of the self_evaluable field.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ is truth-evaluable, then $C(x,x) = 0$ for all $x > 0$.
background
The module formalizes the Reality ⇒ Logic direction by introducing truth-evaluable comparison operators whose self-comparisons, reorderings, continuity, and finite compositeness translate into the four logical conditions (L1)–(L4). A ComparisonOperator is simply a map ℝ → ℝ → ℝ on positive arguments. TruthEvaluableComparison packages six fields, the first of which is self_evaluable : ∀ x > 0, C x x = 0. Identity is the standalone proposition that extracts precisely this self-comparison law.
proof idea
The declaration is a term-mode one-liner that returns the self_evaluable field of the hypothesis hT : TruthEvaluableComparison C. No tactics or auxiliary lemmas are invoked; the field already matches the body of Identity C by definition.
why it matters
The result supplies the identity component required by the downstream theorem truth_eval_to_operative, which assembles the full OperativePositiveRatioComparison structure. It therefore closes the first step of the (L1)–(L4) translation chain in the Logic Functional Equation paper. Within Recognition Science this corresponds to the zero-cost self-comparison that initiates the J-uniqueness and phi-ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.