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/-- The canonical RCL combiner. -/
  33def rclCombiner (u v : ℝ) : ℝ :=
  34  2 * u * v + 2 * u + 2 * v
  35
  36/-- The canonical RCL polynomial satisfies the full factorization gate. -/
  37theorem rclCombiner_satisfies_gate :
  38    FactorizationAssociativityGate rclCombiner where
  39  symmetric := by
  40    intro u v
  41    unfold rclCombiner
  42    ring
  43  rightAffine := by
  44    intro u
  45    refine ⟨2 * u + 2, 2 * u, ?_⟩
  46    intro v
  47    unfold rclCombiner
  48    ring
  49  zeroBoundary := by
  50    intro u
  51    unfold rclCombiner
  52    ring
  53  unitDiagonal := by
  54    unfold rclCombiner
  55    norm_num
  56
  57/-- Once the affine-response step is known, symmetry and the boundary law force
  58    the entire bilinear family. -/
  59theorem gate_forces_bilinear_family (P : ℝ → ℝ → ℝ)
  60    (hGate : FactorizationAssociativityGate P) :
  61    ∃ c : ℝ, ∀ u v, P u v = c * u * v + 2 * u + 2 * v := by
  62  classical
  63  choose α β hAffine using hGate.rightAffine
  64  have hβ : ∀ u, β u = 2 * u := by
  65    intro u
  66    have h0 : P u 0 = α u * 0 + β u := hAffine u 0
  67    rw [hGate.zeroBoundary u] at h0
  68    linarith
  69  let c : ℝ := α 1 - 2
  70  refine ⟨c, ?_⟩
  71  intro u v
  72  have hsym1 : P u 1 = P 1 u := hGate.symmetric u 1
  73  have hαu : α u = c * u + 2 := by
  74    dsimp [c]
  75    have hcalc : α u * 1 + β u = α 1 * u + β 1 := by
  76      calc
  77        α u * 1 + β u = P u 1 := by symm; exact hAffine u 1
  78        _ = P 1 u := hGate.symmetric u 1
  79        _ = α 1 * u + β 1 := hAffine 1 u
  80    rw [hβ u, hβ 1] at hcalc
  81    linarith
  82  calc
  83    P u v = α u * v + β u := hAffine u v
  84    _ = (c * u + 2) * v + 2 * u := by rw [hαu, hβ u]
  85    _ = c * u * v + 2 * u + 2 * v := by ring
  86
  87/-- Canonical normalization selects the RCL member of the bilinear family. -/
  88theorem gate_forces_rcl (P : ℝ → ℝ → ℝ)
  89    (hGate : FactorizationAssociativityGate P) :
  90    ∀ u v, P u v = 2 * u * v + 2 * u + 2 * v := by
  91  obtain ⟨c, hc⟩ := gate_forces_bilinear_family P hGate
  92  have hc_two : c = 2 := by
  93    have h11 : P 1 1 = c * 1 * 1 + 2 * 1 + 2 * 1 := by
  94      simpa using hc 1 1
  95    linarith [hGate.unitDiagonal, h11]
  96  intro u v
  97  calc
  98    P u v = c * u * v + 2 * u + 2 * v := hc u v
  99    _ = 2 * u * v + 2 * u + 2 * v := by rw [hc_two]
 100
 101/-- Exact gate characterization: the factorization gate is equivalent to being
 102the canonical RCL combiner. -/
 103theorem factorization_gate_iff_rcl (P : ℝ → ℝ → ℝ) :
 104    FactorizationAssociativityGate P ↔ ∀ u v, P u v = rclCombiner u v := by
 105  constructor
 106  · intro hGate u v
 107    rw [gate_forces_rcl P hGate u v]
 108    rfl
 109  · intro hP
 110    refine {
 111      symmetric := ?_
 112      rightAffine := ?_
 113      zeroBoundary := ?_
 114      unitDiagonal := ?_
 115    }
 116    · intro u v
 117      rw [hP u v, hP v u]
 118      unfold rclCombiner
 119      ring
 120    · intro u
 121      refine ⟨2 * u + 2, 2 * u, ?_⟩
 122      intro v
 123      rw [hP u v]
 124      unfold rclCombiner
 125      ring
 126    · intro u
 127      rw [hP u 0]
 128      unfold rclCombiner
 129      ring
 130    · rw [hP 1 1]
 131      unfold rclCombiner
 132      norm_num
 133
 134end FactorizationForcing
 135end DAlembert
 136end Foundation
 137end IndisputableMonolith
 138