reality_satisfies_logic
plain-language theorem explainer
A truth-evaluable comparison operator on positive reals satisfies the laws of logic. Workers on the Logic Functional Equation paper cite this to close the Reality implies Logic direction. The proof is a term-mode application of operative_to_laws_of_logic using the operative property and finite pairwise closure extracted from truth-evaluability.
Claim. Let $C: (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ is truth-evaluable (self-comparisons evaluate to zero, reorderings are single-valued, the map is continuous on positive pairs, and composites admit finite pairwise polynomial closure, plus scale invariance and non-triviality), then $C$ satisfies the laws of logic: identity, non-contradiction, excluded middle, scale invariance, and route independence.
background
This module encodes the Reality to Logic implication for the Logic Functional Equation paper. A ComparisonOperator is a function assigning a real cost to pairs of positive reals. TruthEvaluableComparison is the minimal structure whose fields are self-evaluations to zero, single-valued reorderings, continuity on the positive quadrant, and finite pairwise polynomial closure for composites, together with scale invariance and non-triviality.
proof idea
The proof is a direct term application of operative_to_laws_of_logic. It supplies the operative positive-ratio comparison obtained from truth_eval_to_operative C hT and the finite pairwise closure given by truth_eval_implies_composition C hT.
why it matters
This theorem completes the Reality implies Logic leg of the Logic Functional Equation paper by translating truth-evaluability into the SatisfiesLawsOfLogic structure. It supports the forcing chain toward the Recognition Composition Law. The result is fully proved with no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.