theorem
proved
tactic proof
gate_forces_bilinear_family
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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. -/