finite_logical_satisfies_laws
plain-language theorem explainer
Finite logical comparison on positive ratios satisfies the encoded laws of logic, including identity, non-contradiction, excluded middle, scale invariance, and route independence. Researchers deriving logic from functional equations in Recognition Science cite this when bridging finite algebraic comparisons to the full Aristotelian constraints. The proof is a one-line wrapper that composes the conversion to operative comparison with the finite closure property to invoke the packaging theorem.
Claim. Let $C : (0,∞) × (0,∞) → ℝ$ be a comparison operator. If $C$ is a finite logical comparison, then $C$ satisfies the laws of logic: it obeys identity, non-contradiction, excluded middle, scale invariance, and route independence.
background
A comparison operator is a map from pairs of positive reals to a real-valued cost. The FiniteLogicalComparison structure requires identity, non-contradiction, totality (excluded middle), scale invariance, nontriviality, and counted-once algebra, so that composite values are fixed by a finite pairwise polynomial algebra. SatisfiesLawsOfLogic augments these with route independence. The module states that finite logical comparison on positive ratios forces the Recognition Composition Law family. Upstream, operative_to_laws_of_logic packages an operative positive-ratio comparison together with finite pairwise polynomial closure into the laws structure.
proof idea
The proof is a one-line wrapper that applies operative_to_laws_of_logic to the operative positive-ratio comparison obtained via finite_logical_to_operative and the finite pairwise polynomial closure obtained via finite_logical_has_finite_closure.
why it matters
This result feeds operative_domain_satisfies_logic, which shows operative-domain structures satisfy the laws of logic. It fills the sharpened theorem that finite logical comparison forces the RCL family, a step in the forcing chain from T0 to T8 toward the Recognition Composition Law. The module's counterexamples address why the finite algebraic condition cannot be dropped.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.