pith. sign in
theorem

bilinear_family_forced

proved
show as:

The bilinear cost family is forced by the d'Alembert factorization.

module
IndisputableMonolith.Foundation.DAlembert.Inevitability
domain
Foundation
line
289 · github
papers citing
150 papers (below)

plain-language theorem explainer

Any cost functional normalized at unity and multiplicatively consistent with a symmetric quadratic polynomial combiner must have that combiner of bilinear form 2u + 2v + c uv. Recognition Science researchers cite the result to establish that the d'Alembert equation is the unique form forced by consistency. The proof extracts coefficients from the polynomial assumption via normalization at 1 and P-symmetry, then fixes the remaining terms using non-triviality of F.

Claim. Let $F : (0,∞) → ℝ$ satisfy $F(1) = 0$ and let $P : ℝ → ℝ → ℝ$ be a symmetric polynomial of degree at most 2 such that $F(xy) + F(x/y) = P(F(x), F(y))$ for all $x,y > 0$. Assume $F$ is non-trivial and continuous on $(0,∞)$. Then there exists $c ∈ ℝ$ such that $P(u,v) = 2u + 2v + c uv$ for all $u,v$, and if $c=2$ then $P(u,v) = 2u + 2v + 2uv$.

background

The module establishes that the d'Alembert equation is the unique form compatible with multiplicative consistency for cost functionals. IsNormalized encodes the condition $F(1) = 0$, the normalization that treats $F$ as a cost of deviation from unity. HasMultiplicativeConsistency encodes the relation $F(xy) + F(x/y) = P(F(x), F(y))$ where $P$ is required to be symmetric and quadratic. The local theoretical setting is that symmetry, normalization, and polynomial consistency together force the bilinear family, closing the transcendental argument for the axiom bundle without presupposing the specific RCL coefficients.

proof idea

The proof first obtains symmetry of $F$ from symmetry of $P$ via the consistency relation. It applies the normalization lemma to constrain $P(0, F(y)) = 2 F(y)$. Expanding the given polynomial form and substituting the consistency equation at $(1,1)$ forces the constant term to vanish. Symmetry of $P$ then equates the linear coefficients and the quadratic coefficients. Non-triviality supplies a point where $F(y) ≠ 0$, which forces the remaining coefficients to the bilinear values $c=2$ and zero quadratic term.

why it matters

This theorem supplies the central step showing that the RCL form is inevitable once consistency is required to hold with a symmetric quadratic polynomial. It feeds directly into axiom_bundle_necessary, which concludes that the full axiom bundle (normalization, RCL, calibration) is transcendentally necessary, and into consistency_forces_RCL_form_is_theorem, which fixes the canonical scale $c=2$. In the framework it completes the argument that A2 is not an arbitrary choice but the unique polynomial solution compatible with the cost axioms.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.

papers checked against this theorem (showing 30 of 150)

The full set is indexed internally; the public theorem page shows a capped sample so high-use declarations do not become many-thousand-row pages.