truth_eval_implies_identity
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not address reorder symmetry or continuity of C.
- Does not apply when arguments are non-positive.
- Does not derive non-contradiction or composition laws.
- Does not invoke the phi-forcing or spectral-emergence structures.
Lean usage
theorem example (C : ComparisonOperator) (hT : TruthEvaluableComparison C) : Identity C := truth_eval_implies_identity C hTformal statement (Lean)
34theorem truth_eval_implies_identity
35 (C : ComparisonOperator)
36 (hT : TruthEvaluableComparison C) :
37 Identity C :=
proof body
Term-mode proof.
38 hT.self_evaluable
39
40/-- Truth-evaluability of reordered pair-statements gives non-contradiction. -/