truth_eval_implies_identity
plain-language theorem explainer
Truth-evaluability of a comparison operator on positive reals yields the identity law that self-comparison costs zero. Workers on the Logic Functional Equation paper cite this result when deriving the first Aristotelian condition from reality structures. The proof is a direct field projection from the TruthEvaluableComparison hypothesis.
Claim. Let $C$ be a comparison operator on positive reals. If $C$ is truth-evaluable, then $C(x,x)=0$ for every $x>0$.
background
The module formalises the Reality ⇒ Logic leg of the Logic Functional Equation paper. A comparison operator maps pairs of positive reals to reals and encodes comparison cost. TruthEvaluableComparison requires four fields: self-comparison evaluates to zero, reordering is single-valued, the map is continuous on positive pairs, and composites admit finite pairwise polynomial closure.
Identity is the proposition that self-comparison always costs zero, the formal counterpart of the law of identity. Upstream definitions of ComparisonOperator and Identity supply the target property and the semantic starting point for the four lemmas that translate truth-evaluability into (L1)--(L4).
proof idea
One-line wrapper that applies the self_evaluable field of the TruthEvaluableComparison hypothesis.
why it matters
This supplies the identity component inside the OperativePositiveRatioComparison constructed by the downstream theorem truth_eval_to_operative. It advances the first step of the Reality ⇒ Logic direction in the Logic Functional Equation paper by converting one semantic field of TruthEvaluableComparison into a logical condition. The result grounds the comparison operator without reference to the forcing chain, J-uniqueness, or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.