structure
definition
def or abbrev
FactorizationAssociativityGate
show as:
view Lean formalization →
formal statement (Lean)
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. -/