TruthEvaluableComparison
plain-language theorem explainer
Truth-evaluable comparison operators on positive reals bundle six properties ensuring self-comparison yields zero, reordering is symmetric, the map is continuous on positive pairs, composites admit finite pairwise polynomial closure, scale invariance holds, and the operator is non-trivial. Workers on the Logic Functional Equation paper cite this structure to ground the passage from physical comparison to the laws of logic. The definition itself supplies the semantic conditions that downstream lemmas convert into the four Aristotelian encodings.
Claim. An operator $C : (0,∞) × (0,∞) → ℝ$ is truth-evaluable when $C(x,x)=0$ for all $x>0$, $C(x,y)=C(y,x)$ for all $x,y>0$, the map $(x,y)↦C(x,y)$ is continuous on the positive quadrant, composite comparisons admit finite pairwise polynomial closure, $C(λx,λy)=C(x,y)$ for all $λ>0$, and there exists $x>0$ such that the derived cost of $C$ at $x$ is nonzero.
background
The module formalises the Reality ⇒ Logic leg of the Logic Functional Equation paper. A ComparisonOperator is an ℝ→ℝ→ℝ map assigning a real cost to pairs of positive quantities. ScaleInvariant requires the cost to depend only on the ratio of the arguments, while NonTrivial excludes the zero operator. FinitePairwisePolynomialClosure encodes determinate finite pairwise combiners for composites. Upstream, LedgerFactorization supplies the route-independence form of the cost, and the d'Alembert structure ensures the cost is well-defined on positive ratios.
proof idea
This declaration is a structure definition that directly bundles the six required properties; no proof body exists. Downstream lemmas extract each field verbatim as a separate implication theorem.
why it matters
This structure is the central hypothesis for the Reality ⇒ Logic leg. It is invoked by reality_satisfies_logic to obtain SatisfiesLawsOfLogic, by rcl_from_truth_evaluable_comparison to force the Recognition Composition Law family, and by the implication theorems recovering identity, non-contradiction, totality, and composition. In the framework it supplies the minimal conditions under which physical comparison yields logical consistency, feeding the derivation of the functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.