operative_to_laws_of_logic
plain-language theorem explainer
Operative positive-ratio comparisons with finite pairwise polynomial closure satisfy the laws of logic structure. Foundation researchers cite this to connect operative comparisons to the SatisfiesLawsOfLogic interface used in Level-1 theorems. The proof is a term-mode structure constructor that assembles fields directly from the operative hypothesis and the closure condition.
Claim. Let $C$ be a comparison operator on positive reals. If $C$ is an operative positive-ratio comparison (continuous and nontrivial, satisfying identity, non-contradiction, scale invariance) and obeys finite pairwise polynomial closure (route independence), then $C$ satisfies the laws of logic.
background
ComparisonOperator is an abbreviation for maps from pairs of positive reals to reals that assign comparison cost. OperativePositiveRatioComparison requires continuity, nontriviality, identity, non-contradiction, and scale invariance on positive arguments. FinitePairwisePolynomialClosure is defined as route independence, the polynomial closure condition drawn from the Level-1 logic-as-functional-equation module.
proof idea
The proof is a term-mode structure constructor. It populates the SatisfiesLawsOfLogic fields by direct projection: identity, non-contradiction, excluded middle (from continuous), scale invariance, and non-trivial from the operative hypothesis, with route independence supplied by the finite closure hypothesis.
why it matters
This packages the operative comparison for use in canonicality_of_encoding and rcl_polynomial_closure_theorem. It supplies the direct proof step that feeds the Level-1 theorem, linking to the Recognition Composition Law family through the d'Alembert inevitability theorem. It touches the question of whether the functional equation alone forces all downstream structure without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.