truth_eval_implies_totality
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish identity or non-contradiction for comparisons.
- Does not derive scale invariance or the full Recognition Composition Law.
- Applies only to positive-ratio comparisons on the reals.
- Does not address discrete phi-ladder mass assignments or Berry thresholds.
formal statement (Lean)
49theorem truth_eval_implies_totality
50 (C : ComparisonOperator)
51 (hT : TruthEvaluableComparison C) :
52 ExcludedMiddle C :=
proof body
Term-mode proof.
53 hT.determinate_continuous
54
55/-- Truth-evaluability of composite comparison-statements gives finite pairwise
56composition. -/