Cycles (A5)

Statements split from the original Statements.lean skeleton (one file per proving task). See AUDIT-NOTES A5 and the packet sources B4-cycles-and-stronger-hierarchies.md (§3-6) and B5-pair-source-classification.md (§4) for the mathematics.

The Walsh section is general Boolean-cube Fourier analysis (orthogonality, inversion, uniqueness) and is reusable by the other pair-source files.

Walsh characters on a finite Boolean cube

theorem TriangleInflation.Graph.sgn_mul_self (b : Bool) : sgn b * sgn b = 1

theorem TriangleInflation.Graph.prod_sgn_mul_self {ι : Type u_1} (F : Finset ι) (w : ι → Bool) : (∏ v ∈ F, sgn (w v)) * ∏ v ∈ F, sgn (w v) = 1

theorem TriangleInflation.Graph.prod_sgn_eq_prod_univ {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Finset ι) (w : ι → Bool) : ∏ v ∈ F, sgn (w v) = ∏ v : ι, if v ∈ F then sgn (w v) else 1

A Walsh character as a product over the whole index type.

theorem TriangleInflation.Graph.prod_sgn_mul_prod_sgn {ι : Type u_1} [DecidableEq ι] [Finite ι] (F F' : Finset ι) (w : ι → Bool) : (∏ v ∈ F', sgn (w v)) * ∏ v ∈ F, sgn (w v) = ∏ v ∈ symmDiff F' F, sgn (w v)

The product of two Walsh characters is the character of their symmetric difference.

theorem TriangleInflation.Graph.sum_prod_sgn {ι : Type u_1} [Fintype ι] [DecidableEq ι] (F : Finset ι) : ∑ w : ι → Bool, ∏ v ∈ F, sgn (w v) = if F = ∅ then 2 ^ Fintype.card ι else 0

Orthogonality of the Walsh characters on ι → Bool.

theorem TriangleInflation.Graph.sum_prod_sgn_mul {ι : Type u_1} [Fintype ι] (u w : ι → Bool) : ∑ F : Finset ι, ∏ v ∈ F, sgn (u v) * sgn (w v) = if u = w then 2 ^ Fintype.card ι else 0

The Walsh characters are their own dual basis.

theorem TriangleInflation.Graph.eq_of_walsh_moments_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P Q : (ι → Bool) → ℝ) (h : ∀ (F : Finset ι), ∑ w : ι → Bool, P w * ∏ v ∈ F, sgn (w v) = ∑ w : ι → Bool, Q w * ∏ v ∈ F, sgn (w v)) : P = Q

Walsh uniqueness. Two weight functions on a finite Boolean cube with the same Walsh moments are equal.

The boundary map of the cycle

def TriangleInflation.Graph.cycleNext {m : ℕ} (v : Fin m) : Fin m

The successor vertex on the cycle C_m. The edge recorded by v joins v and cycleNext v.

Equations

• TriangleInflation.Graph.cycleNext v = ⟨(↑v + 1) % m, ⋯⟩

theorem TriangleInflation.Graph.mem_cycleBoundary {m : ℕ} (F : Finset (Fin m)) (v : Fin m) : v ∈ cycleBoundary m F ↔ ¬(v ∈ F ↔ cycleNext v ∈ F)

theorem TriangleInflation.Graph.cycleNext_injective {m : ℕ} : Function.Injective cycleNext

theorem TriangleInflation.Graph.prod_cycleNext {m : ℕ} (f : Fin m → ℝ) : ∏ v : Fin m, f (cycleNext v) = ∏ v : Fin m, f v

theorem TriangleInflation.Graph.cycleBoundary_empty {m : ℕ} : cycleBoundary m ∅ = ∅

theorem TriangleInflation.Graph.cycleBoundary_univ {m : ℕ} : cycleBoundary m Finset.univ = ∅

theorem TriangleInflation.Graph.cycleBoundary_compl {m : ℕ} (F : Finset (Fin m)) : cycleBoundary m Fᶜ = cycleBoundary m F

theorem TriangleInflation.Graph.cycleBoundary_card_even {m : ℕ} (F : Finset (Fin m)) : Even (cycleBoundary m F).card

The source boundary of a vertex set of the cycle has even size.

theorem TriangleInflation.Graph.cycle_eq_of_boundary_eq {m : ℕ} (hm : 0 < m) {F F' : Finset (Fin m)} (hb : cycleBoundary m F = cycleBoundary m F') (h0 : ⟨0, hm⟩ ∈ F ↔ ⟨0, hm⟩ ∈ F') : F = F'

A vertex set of the cycle is determined by its source boundary together with the membership of the vertex 0.

theorem TriangleInflation.Graph.cycleBoundary_eq_empty_iff {m : ℕ} (hm : 0 < m) (F : Finset (Fin m)) : cycleBoundary m F = ∅ ↔ F = ∅ ∨ F = Finset.univ

A5: the cycle target is a law

theorem TriangleInflation.Graph.cycleTarget_sum (m : ℕ) (q : ℝ) : ∑ w : Fin m → Bool, cycleTarget m q w = 1

theorem TriangleInflation.Graph.cycleTarget_nonneg (m : ℕ) (hm : 0 < m) (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑m ^ 2 * q ≤ 1 / 4) (w : Fin m → Bool) : 0 ≤ cycleTarget m q w

The cycle target vanishes on the odd-parity outcomes and is bounded below by (1/2)^m (2 - 2((1+√q)^m - 1)) on the even-parity ones.

theorem TriangleInflation.Graph.cycleTarget_moment (m : ℕ) (q : ℝ) (F : Finset (Fin m)) : ∑ w : Fin m → Bool, cycleTarget m q w * ∏ v ∈ F, sgn (w v) = (-q) ^ ((cycleBoundary m F).card / 2)

The Walsh moments of the cycle target: the character of a vertex set F has moment (−q)^{|∂F|/2} (AUDIT-NOTES A5; packet B5 §4, equation (12)).

A5: every cycle

theorem TriangleInflation.Graph.cycleTarget_isLaw (m : ℕ) (hm : 3 ≤ m) (q : ℝ) (hq0 : 0 ≤ q) (hq : ↑m ^ 2 * q ≤ 1 / 4) : IsLaw (cycleTarget m q)

The cycle target is a law when m² q ≤ 1/4: the nonconstant Fourier terms sum to at most ∑_{j≥1} 4^{-j} = 1/3 of the uniform weight (AUDIT-NOTES A5).

A5: exact parity rigidity for the triangle

theorem TriangleInflation.Graph.exists_pos_of_isLaw {α : Type u_1} [Fintype α] (μ : α → ℝ) (h : IsLaw μ) : ∃ (a : α), 0 < μ a

theorem TriangleInflation.Graph.neg_one_le_mul_le_one {u v : ℝ} (hu1 : -1 ≤ u) (hu2 : u ≤ 1) (hv1 : -1 ≤ v) (hv2 : v ≤ 1) : -1 ≤ u * v ∧ u * v ≤ 1

Products of numbers in [-1,1] stay in [-1,1].

theorem TriangleInflation.Graph.sq_eq_one_of_prod_eq_one {u v w : ℝ} (hu1 : -1 ≤ u) (hu2 : u ≤ 1) (hv1 : -1 ≤ v) (hv2 : v ≤ 1) (hw1 : -1 ≤ w) (hw2 : w ≤ 1) (h : u * v * w = 1) : u * u = 1 ∧ v * v = 1 ∧ w * w = 1

A product of three numbers of [-1,1] equal to 1 forces all three to be signs.

theorem TriangleInflation.Graph.parity_rigidity (P : ThreeBit → ℝ) (hP : IsLaw P) (hpar : ∀ (w : ThreeBit), (w.1 ^^ w.2.1 ^^ w.2.2) = true → P w = 0) (hC : TriangleCompatible P) : 0 ≤ triMeanA P * triMeanB P * triMeanC P

AUDIT-NOTES A5, exact parity rigidity for the triangle. A compatible three-bit law supported on the even-parity outcomes has E[A] E[B] E[C] ≥ 0. (Absorb the seeds, fix y₀, put S = B(·,y₀), T = C(·,y₀); then A = ST, B = SU, C = TU for a sign U of the third source, so the three means are st, su, tu.)