rcl_polynomial_closure_theorem
plain-language theorem explainer
Operative positive-ratio comparisons with finite pairwise polynomial closure yield a derived cost obeying the Recognition Composition Law in bi-affine form. Foundation researchers cite this when establishing the RCL family from comparison operators under polynomial regularity. The proof is a one-line term application of the uniqueness theorem for the functional form of logic after translating the operative hypotheses into laws of logic.
Claim. Let $C$ be a comparison operator that satisfies the operative positive-ratio comparison axioms (identity, non-contradiction, continuity, scale invariance, and non-triviality) together with finite pairwise polynomial closure. Then there exist a function $P : ℝ → ℝ → ℝ$ and a constant $c ∈ ℝ$ such that the derived cost of $C$ is multiplicatively consistent with $P$ and $P(u,v) = 2u + 2v + c·uv$ for all real $u,v$.
background
An operative positive-ratio comparison is a continuous, nontrivial comparison operator satisfying identity, symmetric single-valued comparison, and scale invariance on positive arguments. Finite pairwise polynomial closure is defined as route independence, the polynomial route-independence condition from the Level-1 logic-as-functional-equation module. The module supplies a paper-facing wrapper around the translation theorem, isolating finite pairwise polynomial closure as the precise regularity condition that forces the Recognition Composition Law family while also handling the strict bi-affine counted-once subcase directly.
proof idea
The proof is a one-line term wrapper. It applies RCL_is_unique_functional_form_of_logic to the result of operative_to_laws_of_logic C hOp hFinite, which converts the operative positive-ratio comparison and finite closure hypotheses into the laws of logic.
why it matters
This theorem places the RCL family on the finite pairwise polynomial algebra of positive-ratio comparison and feeds directly into the canonicality results rcl_from_canonical_mismatch_encoding and rcl_from_truth_evaluable_comparison. It fills the paper proposition on RCL as the finite pairwise polynomial algebra and supports the Recognition Composition Law as the core functional equation in the forcing chain from T5 J-uniqueness onward.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.