FinitePairwisePolynomialClosure
plain-language theorem explainer
Finite pairwise polynomial closure packages the route-independence condition on a comparison operator as the existence of a quadratic polynomial expressing the symmetric composite cost of forward and backward ratios. Researchers formalizing the Level-1 translation from recognition events to logical structure cite this definition when packaging the regularity hypothesis for deriving the Recognition Composition Law family. The definition is realized as a direct one-line alias to the RouteIndependence predicate.
Claim. A comparison operator $C : ℝ → ℝ → ℝ$ satisfies finite pairwise polynomial closure when its route independence holds: there exists a polynomial $P(u,v)$ of total degree at most two such that the composite cost of comparing ratios $xy$ and $x/y$ equals $P$ applied to the individual ratio costs, with $P$ symmetric in its arguments and satisfying the consistency condition.
background
ComparisonOperator is the abbreviation for maps from positive reals to reals that assign a real-valued cost to comparing two quantities, subject to the four Aristotelian structural constraints of identity, non-contradiction, and consistency. RouteIndependence is the upstream predicate requiring that the symmetric forward-and-backward composite comparison on positive ratios yields a cost that is a quadratic polynomial in the two constituent ratio costs, together with symmetry and consistency axioms. The DirectProof module isolates this finite pairwise polynomial closure as the precise regularity condition needed to force the Recognition Composition Law family from an operative positive-ratio comparison.
proof idea
The definition is a one-line wrapper that directly invokes the RouteIndependence predicate on the supplied comparison operator C.
why it matters
This definition supplies the exact hypothesis used by canonicality_of_encoding and rcl_from_canonical_mismatch_encoding to conclude that a magnitude-of-mismatch comparison satisfies SatisfiesLawsOfLogic and yields the RCL family. It is invoked by operative_to_laws_of_logic and rcl_polynomial_closure_theorem, which package the Level-1 translation from recognition to logical structure. In the framework it encodes the polynomial restriction at Level 1, the step that precedes the continuity upgrade and enables the forcing chain from J-uniqueness through the phi fixed point to the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.