Derived in part from Apache-2.0 openai/ten-proofs, ConnesRigidity.lean at 94bc0feb6a9ff12c7d31d6de640a725c9d43d2b6, lines 18-23. Modifications: renamed the elementary ZMod 2 helper and placed it in the local Boolean-polynomial namespace. The remaining finite-coordinate support and weight development is local. See the upstream PORT_MAP.md.

@[reducible, inline]

abbrev Connes.BooleanPolynomial.F : Type

Characteristic-two scalar field. Paper: §4.

Equations

• Connes.BooleanPolynomial.F = ZMod 2

theorem Connes.BooleanPolynomial.eq_one_of_ne_zero (a : F) (ha : a ≠ 0) : a = 1

Nonzero characteristic-two scalars are one. Paper: §2; see the pinned upstream provenance manifest.

@[reducible, inline]

abbrev Connes.BooleanPolynomial.PolynomialOn (ι : Type u_1) : Type u_1

Boolean functions on an arbitrary finite coordinate type. Paper: §4.

Equations

• Connes.BooleanPolynomial.PolynomialOn ι = ((ι → Connes.BooleanPolynomial.F) → Connes.BooleanPolynomial.F)

noncomputable def Connes.BooleanPolynomial.supportOn {ι : Type u_1} [Fintype ι] (P : PolynomialOn ι) : Finset (ι → F)

Support of a Boolean function on arbitrary finite coordinates. Paper: §4.

Equations

• Connes.BooleanPolynomial.supportOn P = {x : ι → Connes.BooleanPolynomial.F | P x ≠ 0}

noncomputable def Connes.BooleanPolynomial.weightOn {ι : Type u_1} [Fintype ι] (P : PolynomialOn ι) : ℕ

Support weight on arbitrary finite coordinates. Paper: §4.

Equations

• Connes.BooleanPolynomial.weightOn P = (Connes.BooleanPolynomial.supportOn P).card

structure Connes.BooleanPolynomial.QuadraticData (ι : Type u_1) [Fintype ι] : Type u_1

Degree-two coefficient data on arbitrary finite Boolean coordinates. Paper: §4.

• constantTerm : F

  The constantTerm component of QuadraticData.

• linear : ι → F

  The linear component of QuadraticData.

• quadratic : ι → ι → F

  The quadratic component of QuadraticData.

def Connes.BooleanPolynomial.QuadraticData.eval {ι : Type u_1} [Fintype ι] (q : QuadraticData ι) (x : ι → F) : F

Evaluation of degree-two coefficient data. Paper: §4.

Equations

• q.eval x = q.constantTerm + ∑ i : ι, q.linear i * x i + ∑ i : ι, ∑ j : ι, q.quadratic i j * x i * x j

def Connes.BooleanPolynomial.IsQuadratic {ι : Type u_1} [Fintype ι] (P : PolynomialOn ι) : Prop

Degree restriction on arbitrary finite Boolean coordinates. Paper: §4.

Equations

• Connes.BooleanPolynomial.IsQuadratic P = ∃ (q : Connes.BooleanPolynomial.QuadraticData ι), ∀ (x : ι → Connes.BooleanPolynomial.F), q.eval x = P x

theorem Connes.BooleanPolynomial.quadratic_support_quarter {W : Type u_1} [AddCommGroup W] [Module F W] [Fintype W] (f : W → F) (b : W → W → F) (hadd : ∀ (x y : W), f (x + y) = f x + f y + f 0 + b x y) (hbadd : ∀ (x y z : W), b (x + y) z = b x z + b y z) (hf : ∃ (x : W), f x ≠ 0) : Fintype.card W ≤ 4 * {x : W | f x ≠ 0}.card

Four-point support cover for quadratic functions. Paper: §4.

theorem Connes.BooleanPolynomial.quadratic_weight_lower_bound {ι : Type u_1} [Fintype ι] (P : PolynomialOn ι) (hdeg : IsQuadratic P) (hP : P ≠ 0) : weightOn P ≥ 2 ^ (Fintype.card ι - 2)

Low-degree support estimate on arbitrary finite Boolean coordinates. Paper: §4.