PolynomialCombiner
plain-language theorem explainer
The PolynomialCombiner structure packages the assumption that the combiner relating F(xy) + F(x/y) to F(x) and F(y) is at most quadratic. Researchers deriving the uniqueness of the recognition composition law from symmetry and normalization cite it when closing the transcendental argument for cost functionals. The definition directly encodes the degree bound that later algebraic constraints reduce to the bilinear family.
Claim. A map $P : ℝ × ℝ → ℝ$ is a polynomial combiner when there exist real numbers $a,b,c,d,e,f$ such that $P(u,v) = a + b u + c v + d u v + e u^2 + f v^2$ for all real $u,v$.
background
The module proves that any cost functional F : ℝ₊ → ℝ obeying symmetry F(x) = F(1/x), normalization F(1) = 0, and multiplicative consistency F(xy) + F(x/y) = P(F(x), F(y)) for a symmetric quadratic polynomial P must recover the d'Alembert form. A polynomial combiner is the packaging of that quadratic assumption on P, with the explicit coefficient existence condition given in the structure fields.
proof idea
This declaration is a structure definition that introduces the type by specifying the field P together with the explicit existential witness for its quadratic coefficients. No lemmas are applied and no tactics are used; it serves as a direct packaging of the degree-at-most-two hypothesis required by the module's core argument.
why it matters
The definition supplies the polynomial assumption that downstream siblings such as polynomial_form_forced and bilinear_family_forced constrain to the specific bilinear family 2u + 2v + c u v. It thereby completes the inevitability proof for the recognition composition law inside the D'Alembert module, closing the final gap in the A1-A3 axiom bundle and aligning with the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.