finite_logical_has_finite_closure
plain-language theorem explainer
Finite logical comparison on a comparison operator implies route independence via its counted-once composition property. Derivations linking Aristotelian constraints to the recognition composition law cite this algebraic bridge. The proof is a one-line wrapper applying the counted-once to finite-pairwise theorem directly to the algebra field of the hypothesis.
Claim. Let $C : ℝ → ℝ → ℝ$ be a comparison operator. If $C$ satisfies identity, non-contradiction, excluded middle, scale invariance, nontriviality, and counted-once composition, then $C$ satisfies route independence.
background
A comparison operator is a map from pairs of positive reals to a real-valued cost. Finite logical comparison is the structure that bundles the Aristotelian constraints (identity, non-contradiction, totality via excluded middle), scale invariance, nontriviality, and counted-once composition. Finite pairwise polynomial closure is defined as route independence, the polynomial route-independence condition imported from the level-1 logic-as-functional-equation module.
proof idea
The proof is a one-line wrapper that applies the upstream theorem counted_once_to_finite_pairwise_polynomial to the counted_once_algebra field extracted from the finite logical comparison hypothesis.
why it matters
This supplies the algebraic closure step required by the downstream theorem finite_logical_satisfies_laws. The module doc-comment positions it inside the sharpened result that finite logical comparison on positive ratios forces the RCL family. In the Recognition Science setting it connects logical axioms to the functional equation whose solutions produce J-uniqueness and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.