Foundation Dalembert Right Affine From Factorization Polynomial Consistency Forc

The combiner's forced form

In the Recognition Science framework, a recognition event, a discrete record of a comparison, carries a cost, a real number measuring the price of that record. The framework studies a function P that combines two such costs into a third, the way addition combines two numbers into a sum. The declaration polynomial_consistency_forces_rcl proves a constraint on that combiner: if P is a symmetric quadratic polynomial, and the cost function F it serves obeys a consistency relation F(xy) + F(x/y) = P(F(x), F(y)), then P must equal the polynomial 2uv + 2u + 2v.

The theorem's hypotheses are plain. The combiner P is symmetric, meaning P(u,v) = P(v,u). It is a quadratic polynomial, meaning it has the form a + bu + cv + duv + eu² + fv² for some real coefficients. The cost function F is normalized, non-trivial, and continuous on the positive reals. Under those conditions, the machine-checked library of formal theorems proves the conclusion: for every u and v, P(u,v) = 2uv + 2u + 2v. The proof runs through an intermediate result that a symmetric quadratic polynomial consistent with F must be bilinear, and a bilinear form is automatically right-affine, meaning for each fixed u the function v ↦ P(u,v) is a straight line.

The historical context matters. Earlier work in the framework had assumed right-affineness as a hypothesis in a gate structure, a set of conditions that force the combiner's shape. This declaration closes a gap: it shows that under the stronger assumption that P is polynomial, right-affineness is a consequence, not a separate assumption. The theorem is one of two routes to the same conclusion. The other, in a companion module, proves the identical combiner form from the surjectivity of the cost function J alone, with no polynomial hypothesis at all. Both routes mean the core forcing claim does not rest on an unproved right-affine assumption.

The theorem does not claim that P must be a polynomial. That is the genuinely open step: deriving polynomial shape from mere continuity or smoothness of P, a problem in classical functional equation theory that remains unformalized. The theorem also does not claim that the cost function must be J; it takes J's properties as input through the consistency relation. What the declaration establishes is narrower and precise: given the polynomial and functional hypotheses, the combiner's form is forced, and the machine-checked proof certifies it.

/-- **Main Theorem of this Module**: RCL follows from polynomial consistency
without separately assuming right-affine.

This closes Gap 4 in the direction of: if we're willing to assume P is
polynomial, then right-affine is a theorem, not a hypothesis. -/
theorem polynomial_consistency_forces_rcl
    (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hNorm : Inevitability.IsNormalized F)
    (hCons : Inevitability.HasMultiplicativeConsistency F P)
    (hPoly : ∃ (a b c d e f : ℝ), ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2)
    (hSymP : ∀ u v, P u v = P v u)
    (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
    (hCont : ContinuousOn F (Set.Ioi 0))
    (hP11 : P 1 1 = 6)
    (hP0 : ∀ u, P u 0 = 2 * u) :
    ∀ u v, P u v = 2 * u * v + 2 * u + 2 * v :=
  gate_forces_rcl P
    (gate_from_polynomial_consistency F P hNorm hCons hPoly hSymP hNonTriv hCont hP11 hP0)

/-- Right-affine follows from polynomial consistency with a cost functional `F`.

This theorem takes the Inevitability hypotheses (F normalized, consistent with
a symmetric quadratic polynomial P, non-trivial, continuous) and concludes
that P is right-affine. -/
theorem polynomial_consistency_implies_right_affine
    (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
    (hNorm : Inevitability.IsNormalized F)
    (hCons : Inevitability.HasMultiplicativeConsistency F P)
    (hPoly : ∃ (a b c d e f : ℝ), ∀ u v, P u v = a + b*u + c*v + d*u*v + e*u^2 + f*v^2)
    (hSymP : ∀ u v, P u v = P v u)
    (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
    (hCont : ContinuousOn F (Set.Ioi 0)) :
    ∀ u, ∃ α β, ∀ v, P u v = α * v + β := by
  obtain ⟨c, hc, _⟩ := Inevitability.bilinear_family_forced F P hNorm hCons hPoly hSymP hNonTriv hCont
  exact bilinear_implies_right_affine P c hc

/-- Bilinear form implies right-affine. -/
theorem bilinear_implies_right_affine
    (P : ℝ → ℝ → ℝ) (c : ℝ)
    (h_bilinear : ∀ u v, P u v = 2*u + 2*v + c*u*v) :
    ∀ u, ∃ α β, ∀ v, P u v = α * v + β := by
  intro u
  refine ⟨2 + c*u, 2*u, ?_⟩
  intro v
  rw [h_bilinear u v]
  ring

/-- **Gate-free RCL theorem (from Unconditional.lean, re-exposed here).**

If F = J and F has any consistency relation F(xy) + F(x/y) = P(F(x), F(y))
with some function P, then P equals the RCL polynomial on [0, ∞)². This holds
without any assumption on P's form (polynomial, right-affine, smooth, etc.).
-/
theorem rcl_without_gate
    (P : ℝ → ℝ → ℝ)
    (hCons : ∀ x y : ℝ, 0 < x → 0 < y →
      Cost.Jcost (x * y) + Cost.Jcost (x / y) = P (Cost.Jcost x) (Cost.Jcost y)) :
    ∀ u v : ℝ, 0 ≤ u → 0 ≤ v → P u v = 2*u*v + 2*u + 2*v :=
  Unconditional.rcl_unconditional P hCons

What this page does not claim

The theorem does not prove that P must be a polynomial from continuity or smoothness alone. The theorem does not establish that the cost function F must equal J; it assumes J's properties through the consistency relation. The theorem does not show that the combiner form holds for functions P that are not symmetric quadratic polynomials.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/DAlembert/RightAffineFromFactorization.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: