  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) :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.