truth_eval_implies_totality
plain-language theorem explainer
A truth-evaluable comparison operator on positive reals yields continuity of its cost function over the open positive quadrant. Researchers deriving the logic-functional equation from physical comparison structures cite this when converting semantic truth conditions into the excluded-middle axiom. The proof is a direct field extraction from the determinate-continuous component of the hypothesis.
Claim. Let $C$ be a comparison operator on positive reals. If $C$ satisfies truth-evaluability (self-comparisons evaluate to zero, reordering is single-valued, the uncurried map is continuous on the positive quadrant, and composites admit finite pairwise closure), then $C$ is continuous on $(0,∞)×(0,∞)$.
background
A ComparisonOperator maps pairs of positive reals to a real cost. TruthEvaluableComparison packages the minimal semantic requirements: self-evaluations return zero, reordering yields the same value, the map is continuous on the open positive quadrant, and composite statements close under finite pairwise polynomials. The module formalizes the Reality-to-Logic direction of the functional-equation paper, translating these semantic fields into the four Aristotelian conditions (L1)–(L4). ExcludedMiddle is defined precisely as the continuity statement on the positive quadrant.
proof idea
The proof is a one-line term wrapper that returns the determinate_continuous field of the TruthEvaluableComparison hypothesis; that field is definitionally identical to ExcludedMiddle.
why it matters
The result supplies the continuity leg required to construct an OperativePositiveRatioComparison in the downstream theorem truth_eval_to_operative. It completes one of the four translations from truth-evaluability to the logical axioms used in the Logic Functional Equation paper. Within Recognition Science this step anchors the passage from physical J-cost comparisons to the self-similar fixed-point structure and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.