`gate_forces_rcl`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.DAlembert.FactorizationForcing
domain: Foundation
line: 63 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.DAlembert.FactorizationForcing on GitHub at line 63.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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

papers checked against this theorem

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