IndisputableMonolith.Foundation.DAlembert.FactorizationForcing

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Foundation
   5namespace DAlembert
   6namespace FactorizationForcing
   7
   8/-!
   9# Factorization and Associativity Gate
  10
  11This module formalizes the algebraic core used by the B2 closure program.
  12
  13The hard analytic step in the paper is the passage from factorization plus
  14three-way compatibility to the statement that the combiner is affine in its
  15second argument. Once that affine response is available, the remaining forcing
  16is pure algebra:
  17
  18- symmetry,
  19- the boundary law `P(u,0) = 2u`,
  20- and the canonical normalization `P(1,1) = 6`
  21
  22together force the RCL polynomial exactly.
  23-/
  24
  25/-- Packaged combiner gate used by the factorization/associativity bridge. -/
  26structure FactorizationAssociativityGate (P : ℝ → ℝ → ℝ) : Prop where
  27  symmetric : ∀ u v, P u v = P v u
  28  rightAffine : ∀ u, ∃ α β, ∀ v, P u v = α * v + β
  29  zeroBoundary : ∀ u, P u 0 = 2 * u
  30  unitDiagonal : P 1 1 = 6
  31
  32/-- Once the affine-response step is known, symmetry and the boundary law force
  33    the entire bilinear family. -/
  34theorem gate_forces_bilinear_family (P : ℝ → ℝ → ℝ)
  35    (hGate : FactorizationAssociativityGate P) :
  36    ∃ c : ℝ, ∀ u v, P u v = c * u * v + 2 * u + 2 * v := by
  37  classical
  38  choose α β hAffine using hGate.rightAffine
  39  have hβ : ∀ u, β u = 2 * u := by
  40    intro u
  41    have h0 : P u 0 = α u * 0 + β u := hAffine u 0
  42    rw [hGate.zeroBoundary u] at h0
  43    linarith
  44  let c : ℝ := α 1 - 2
  45  refine ⟨c, ?_⟩
  46  intro u v
  47  have hsym1 : P u 1 = P 1 u := hGate.symmetric u 1
  48  have hαu : α u = c * u + 2 := by
  49    dsimp [c]
  50    have hcalc : α u * 1 + β u = α 1 * u + β 1 := by
  51      calc
  52        α u * 1 + β u = P u 1 := by symm; exact hAffine u 1
  53        _ = P 1 u := hGate.symmetric u 1
  54        _ = α 1 * u + β 1 := hAffine 1 u
  55    rw [hβ u, hβ 1] at hcalc
  56    linarith
  57  calc
  58    P u v = α u * v + β u := hAffine u v
  59    _ = (c * u + 2) * v + 2 * u := by rw [hαu, hβ u]
  60    _ = c * u * v + 2 * u + 2 * v := by ring
  61
  62/-- Canonical normalization selects the RCL member of the bilinear family. -/
  63theorem gate_forces_rcl (P : ℝ → ℝ → ℝ)
  64    (hGate : FactorizationAssociativityGate P) :
  65    ∀ u v, P u v = 2 * u * v + 2 * u + 2 * v := by
  66  obtain ⟨c, hc⟩ := gate_forces_bilinear_family P hGate
  67  have hc_two : c = 2 := by
  68    have h11 : P 1 1 = c * 1 * 1 + 2 * 1 + 2 * 1 := by
  69      simpa using hc 1 1
  70    linarith [hGate.unitDiagonal, h11]
  71  intro u v
  72  calc
  73    P u v = c * u * v + 2 * u + 2 * v := hc u v
  74    _ = 2 * u * v + 2 * u + 2 * v := by rw [hc_two]
  75
  76end FactorizationForcing
  77end DAlembert
  78end Foundation
  79end IndisputableMonolith
  80