pith. machine review for the scientific record. sign in
theorem

bilinear_family_forced

proved
show as:
view math explainer →

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

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.DAlembert.Inevitability on GitHub at line 289.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 286
 287This means F satisfies the generalized d'Alembert equation.
 288If we choose the canonical cost normalization c = 2, we recover the RCL. -/
 289theorem bilinear_family_forced (F : ℝ → ℝ) (P : ℝ → ℝ → ℝ)
 290    (hNorm : IsNormalized F)
 291    (hCons : HasMultiplicativeConsistency F P)
 292    (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)
 293    (hSymP : ∀ u v, P u v = P v u) -- Explicit symmetry of P
 294    (hNonTriv : ∃ x : ℝ, 0 < x ∧ F x ≠ 0)
 295    (hCont : ContinuousOn F (Set.Ioi 0)) -- Regularity: F is continuous on (0, ∞)
 296    : ∃ c : ℝ, (∀ u v, P u v = 2*u + 2*v + c*u*v) ∧
 297               (c = 2 → ∀ u v, P u v = 2*u + 2*v + 2*u*v) := by
 298  -- Derived reciprocity from symmetry of P
 299  have hSym : IsSymmetric F := F_symmetric_of_P_symmetric F P hCons hSymP
 300  -- Step 1: Normalization forces P(0, v) = 2v
 301  have hP0 : ∀ y : ℝ, 0 < y → P 0 (F y) = 2 * F y :=
 302    symmetry_and_normalization_constrain_P F P hSym hNorm hCons
 303
 304  -- Use the polynomial form lemma
 305  -- We need to satisfy the hypotheses of `polynomial_form_forced`.
 306  -- `hNorm0`: ∀ v, P 0 v = 2 * v.
 307  -- We only have `P 0 (F y) = 2 F y`.
 308  -- However, since P is a polynomial and F is non-trivial (has range with at least 0 and some non-zero value),
 309  -- we can determine the coefficients.
 310  -- P(0, v) = a + c*v + f*v^2.
 311  -- P(0, 0) = a = 2*0 = 0 (from F(1)=0).
 312  -- P(0, F y) = c*(F y) + f*(F y)^2 = 2*(F y).
 313  -- This holds for y=1 (0=0) and some y where F y ≠ 0.
 314  -- If we only have two points, we can't uniquely determine a quadratic.
 315  -- But wait, `polynomial_form_forced` derived `a=0, c=2, f=0`.
 316  -- Let's reproduce that logic but being careful about the domain.
 317
 318  obtain ⟨a, b, c, d, e, f, hP⟩ := hPoly
 319