FieldGraphSeparation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Actual contraction labels obstruct short walks

One label is chosen for each edge of a hypothetical short walk. These labels are padded to the full degree using one fixed member of the same set of directions. Symmetry moves each edge's direction to the contracted slot, so evaluation on this single tuple is constant along the walk. This contradicts robust nonvanishing of the difference of its endpoints.

theorem OAI.MetricEntropyDuality.SymmetricForm.eval_eq_of_contract_eq line 29
Source documentation
Equal contractions imply equal evaluations whenever the contracted vector occurs in any slot. Repeated arguments are allowed.
```
theorem eval_eq_of_contract_eq (v : Fin r → K)
    (F G : SymmetricForm K r (j + 1))
    (hFG : contract v F = contract v G)
    (args : Fin (j + 1) → (Fin r → K)) (a : Fin (j + 1)) (ha : args a = v) :
    F.eval args = G.eval args := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.SymmetricForm.contract
def OAI.MetricEntropyDuality.FieldGraphSeparation.labels line 54
Source documentation
The partition labels are the actual symmetric coefficient contractions.
```
def labels (t : ι → (Fin r → K)) (i : ι)
    (F : SymmetricForm K r (j + 1)) : SymmetricForm K r j :=
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm
def OAI.MetricEntropyDuality.FieldGraphSeparation.padTuple line 58
theorem OAI.MetricEntropyDuality.FieldGraphSeparation.padTuple_mem line 61
theorem OAI.MetricEntropyDuality.FieldGraphSeparation.padTuple_cast line 69
theorem OAI.MetricEntropyDuality.FieldGraphSeparation.eval_eq_of_walk_steps line 76
Source documentation
A finite walk along which a function agrees at each consecutive pair has equal values at its endpoints. This includes the empty walk.
```
private theorem eval_eq_of_walk_steps {V : Type uV} {A : Type uA} {G : SimpleGraph V} {x y : V}
    (w : G.Walk x y) (f : V → A)
    (hf : ∀ n, n < w.length → f (w.getVert n) = f (w.getVert (n + 1))) :
    f x = f y := by
…
```
theorem OAI.MetricEntropyDuality.FieldGraphSeparation.no_short_walk line 92
Source documentation
A robustly nonzero form difference rules out every short walk in the actual contraction partition graph. No separation certificate is assumed.
```
theorem no_short_walk (t : ι → (Fin r → K)) (T : Finset ι) (hT : T.Nonempty)
    (x y : SymmetricForm K r (j + 1))
    (hrobust : ∀ a : Fin (j + 1) → ι, (∀ l, a l ∈ T) →
      (y - x).eval (fun l => t (a l)) ≠ 0)
    (w : (PartitionGraph.graph (labels t) T).Walk x y) : j + 1 < w.length := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.PartitionGraph.graph, OAI.MetricEntropyDuality.FieldGraphSeparation.labels
theorem OAI.MetricEntropyDuality.FieldGraphSeparation.distance_gt line 121
Source documentation
Separation in the extended graph metric, including disconnected endpoints.
```
theorem distance_gt (t : ι → (Fin r → K)) (T : Finset ι) (hT : T.Nonempty)
    (x y : SymmetricForm K r (j + 1))
    (hrobust : ∀ a : Fin (j + 1) → ι, (∀ l, a l ∈ T) →
      (y - x).eval (fun l => t (a l)) ≠ 0) :
    ((j + 1 : ℕ) : ℕ∞) < PartitionGraph.distance (labels t) T x y := by
…
```
Mentions: OAI.MetricEntropyDuality.SymmetricForm, OAI.MetricEntropyDuality.PartitionGraph.distance, OAI.MetricEntropyDuality.FieldGraphSeparation.labels