SignParity.lean`

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Removing threshold zeros and turning sensitive edges into constant-sign edges

All graph pairs are ordered. The cube coordinates are the real signs encoded by Bool in the public statement.

def OAI.LeanBlast.GotsmanLinial.fullParity line 20
Source documentation
Full parity, with values in the reals.
```
noncomputable def fullParity {n : ℕ} (x : Cube n) : ℝ :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.CubeAdjacent line 24
Source documentation
Two cube vertices differ by a single coordinate flip.
```
def CubeAdjacent {n : ℕ} (x y : Cube n) : Prop :=
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.orderedNeighborPairs line 28
Source documentation
All ordered pairs of neighboring vertices.
```
noncomputable def orderedNeighborPairs (n : ℕ) : Finset (Cube n × Cube n) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
def OAI.LeanBlast.GotsmanLinial.orderedConstantEdges line 33
Source documentation
Ordered neighboring pairs at which a real function has equal values.
```
noncomputable def orderedConstantEdges {n : ℕ} (h : Cube n → ℝ) :
    Finset (Cube n × Cube n) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.exists_pos_lt_finset line 38
theorem OAI.LeanBlast.GotsmanLinial.exists_pos_shift_nonzero_preserves_sign line 58
Source documentation
A positive constant removes all zeros of a real function on a finite set without changing its threshold signs, including the convention sign(0)=1.
```
theorem exists_pos_shift_nonzero_preserves_sign {α : Type*} [Fintype α]
    (v : α → ℝ) : ∃ ε : ℝ, 0 < ε ∧ (∀ x, v x + ε ≠ 0) ∧
      (∀ x, thresholdSign (v x + ε) = thresholdSign (v x)) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.thresholdSign
theorem OAI.LeanBlast.GotsmanLinial.fullParity_sq line 84
theorem OAI.LeanBlast.GotsmanLinial.fullParity_cases line 88
theorem OAI.LeanBlast.GotsmanLinial.fullParity_flip line 93
Source documentation
Reversing one coordinate reverses full parity.
```
@[simp] theorem fullParity_flip {n : ℕ} (i : Fin n) (x : Cube n) :
    fullParity (flip i x) = -fullParity x := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fullParity, OAI.LeanBlast.GotsmanLinial.flip
theorem OAI.LeanBlast.GotsmanLinial.hammingDist_flip line 106
theorem OAI.LeanBlast.GotsmanLinial.adjacent_iff_hammingDist_eq_one line 119
Source documentation
The flip definition of adjacency agrees with Hamming distance one.
```
theorem adjacent_iff_hammingDist_eq_one {n : ℕ} (x y : Cube n) :
    CubeAdjacent x y ↔ hammingDist x y = 1 := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.CubeAdjacent
def OAI.LeanBlast.GotsmanLinial.directedEdgeEmbedding line 144
Source documentation
A vertex and a direction identify a unique ordered cube edge.
```
def directedEdgeEmbedding (n : ℕ) : (Fin n × Cube n) ↪ (Cube n × Cube n) where
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube
theorem OAI.LeanBlast.GotsmanLinial.orderedNeighborPairs_eq_map line 154
theorem OAI.LeanBlast.GotsmanLinial.card_orderedNeighborPairs line 168
Source documentation
The n * 2^n count includes both orientations of every cube edge.
```
theorem card_orderedNeighborPairs (n : ℕ) :
    (orderedNeighborPairs n).card = n * 2 ^ n := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.orderedNeighborPairs
theorem OAI.LeanBlast.GotsmanLinial.card_orderedConstantEdges line 173
theorem OAI.LeanBlast.GotsmanLinial.parity_twist_eq_iff line 185
Source documentation
Twisting a sign-valued function by parity changes sensitivity into equality across a coordinate flip.
```
theorem parity_twist_eq_iff {n : ℕ} {f : Cube n → ℝ}
    (hf : ∀ x, f x = 1 ∨ f x = -1) (i : Fin n) (x : Cube n) :
    fullParity x * f x = fullParity (flip i x) * f (flip i x) ↔
      f x ≠ f (flip i x) := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fullParity, OAI.LeanBlast.GotsmanLinial.flip
theorem OAI.LeanBlast.GotsmanLinial.parity_twist_cases line 194
theorem OAI.LeanBlast.GotsmanLinial.card_orderedConstantEdges_parity line 200
theorem OAI.LeanBlast.GotsmanLinial.averageSensitivity_eq_parity_edges line 216
Source documentation
Exact uniform normalization: both sides count each sensitive undirected edge twice, once in each direction.
```
theorem averageSensitivity_eq_parity_edges {n : ℕ} {f : Cube n → ℝ}
    (hf : ∀ x, f x = 1 ∨ f x = -1) :
    averageSensitivity f =
      ((orderedConstantEdges (fun x => fullParity x * f x)).card : ℝ) / (2 : ℝ) ^ n := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.averageSensitivity, OAI.LeanBlast.GotsmanLinial.orderedConstantEdges, OAI.LeanBlast.GotsmanLinial.fullParity
theorem OAI.LeanBlast.GotsmanLinial.polynomialThreshold_sensitivity_eq_parity_edges line 222
theorem OAI.LeanBlast.GotsmanLinial.ofReal_fullParity line 231
Source documentation
The real parity used for threshold signs is exactly the full complex Walsh character under the standard real embedding.
```
@[simp] theorem ofReal_fullParity {n : ℕ} (x : Cube n) :
    (fullParity x : ℂ) = walshChar Finset.univ x := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.fullParity, OAI.LeanBlast.GotsmanLinial.walshChar
theorem OAI.LeanBlast.GotsmanLinial.polynomialValue_add_C line 235
theorem OAI.LeanBlast.GotsmanLinial.exists_nonzero_polynomial_same_threshold line 242
Source documentation
The zero-removal reduction preserves multilinearity, the degree bound, and the entire threshold function.
```
theorem exists_nonzero_polynomial_same_threshold {n d : ℕ}
    {p : MvPolynomial (Fin n) ℝ} (hp : IsMultilinear p) (hd : p.totalDegree ≤ d) :
    ∃ q : MvPolynomial (Fin n) ℝ,
      IsMultilinear q ∧ q.totalDegree ≤ d ∧
        (∀ x : Cube n, polynomialValue q x ≠ 0) ∧
        polynomialThreshold q = polynomialThreshold p := by
…
```
Mentions: OAI.LeanBlast.GotsmanLinial.IsMultilinear, OAI.LeanBlast.GotsmanLinial.Cube, OAI.LeanBlast.GotsmanLinial.polynomialValue, OAI.LeanBlast.GotsmanLinial.polynomialThreshold