FactorizationAssociativityGate

formal source

  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