counted_once_to_finite_pairwise_polynomial
plain-language theorem explainer
Counted-once composition on a comparison operator implies finite pairwise polynomial closure. Researchers formalizing the logic-as-functional-equation foundation cite this to connect the algebraic counted-once restriction to route independence. The proof extracts the polynomial combiner and its coefficients from the hypothesis, assembles the closure witness, and discharges the identity by direct substitution followed by ring normalization.
Claim. Let $C$ be a comparison operator. If there exists a polynomial $P(u,v)=a+bu+cv+duv$ such that $P$ is symmetric, the combiner satisfies the counted-once property, and the derived costs obey $C(x y)+C(x/y)=P(C(x),C(y))$ for positive $x,y$, then $C$ satisfies route independence.
background
ComparisonOperator is an abbreviation for a map from pairs of positive reals to reals that obeys the four Aristotelian constraints making comparison well-posed. CountedOnceComposition asserts the existence of a combiner polynomial $P$ that is symmetric, satisfies the counted-once algebraic form $a+bu+cv+duv$, and reproduces the derived-cost addition law for products and quotients. FinitePairwisePolynomialClosure is defined simply as route independence, the condition that composite-path cost depends only on the endpoints.
proof idea
The proof performs case analysis on the counted-once hypothesis to extract the polynomial $P$, coefficients $a,b,c,d$, symmetry, and consistency data. It then constructs the finite pairwise polynomial closure witness by supplying these data with zero defect terms. The route-independence identity is discharged by rewriting the left-hand side with the combiner definition and normalizing via ring arithmetic.
why it matters
This result is invoked directly by finite_logical_has_finite_closure to transfer finite pairwise polynomial closure to any finite logical comparison. It thereby advances the logic-as-functional-equation program by showing that the counted-once resource discipline forces the polynomial route independence needed for truth-evaluable comparisons. In the Recognition framework it isolates the affine combiner that identity and symmetry later specialize toward the RCL family and the J-cost form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.