BlockPropagation.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Label projection along connected substring links. A link determines a specified subset of one block from positions in its partner word, via a letter equivalence such as identity or inversion. No embedding of inactive graph vertices is requested or assumed.

structure OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton line 11
theorem OAI.TorsionFreeZeroDivisors.BlockPropagation.exists_skeleton line 19
Source documentation
A connected comparison graph supplies a decreasing parent system, with any chosen block as root (in particular the minimizer of its weight bin).
```
theorem exists_skeleton {I : Type*} (G : SimpleGraph I) (hc : G.Connected) (r : I) :
    ∃ S : Skeleton I, S.root = r ∧ ∀ i, i ≠ r → G.Adj i (S.parent i) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton
abbrev OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton.Assignment line 49
def OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton.Consistent line 51
abbrev OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton.FreePosition line 54
theorem OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton.assignment_ext line 57
Source documentation
The omitted coordinates plus the root word determine every full word.
```
theorem assignment_ext {w v : Assignment h (T := T)}
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton.Assignment
theorem OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton.card_freePositions line 80
Source documentation
Exact number of unrecorded letters after the tree comparisons.
```
theorem card_freePositions :
    Nat.card (S.FreePosition h known) =
      ∑ i : {i : I // i ≠ S.root}, (h i.val - (known i.val).card) := by
…
```
theorem OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton.card_assignments line 97
Source documentation
Choose actual root words from R, then at most |T| choices per omitted coordinate. The remaining coordinates are forced by the comparisons.
```
theorem card_assignments (R : Finset (Fin (h S.root) → T)) :
    Nat.card {w : Assignment h (T := T) //
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BlockPropagation.Skeleton.Assignment
structure OAI.TorsionFreeZeroDivisors.StageLabels.Links line 139
Source documentation
A finite directed presentation of substring links. Both directions of an actual interval-isometry link may be included; extra constraints only reduce the set of feasible strings.
```
structure Links (h : I → ℕ) where
…
```
abbrev OAI.TorsionFreeZeroDivisors.StageLabels.Links.Word line 148
def OAI.TorsionFreeZeroDivisors.StageLabels.Links.Consistent line 150
abbrev OAI.TorsionFreeZeroDivisors.StageLabels.Links.RootedWords line 154

theorem OAI.TorsionFreeZeroDivisors.StageLabels.Links.connected_count line 159

Source documentation

Full strings on a connected link component, with a chosen root, are bounded by the root choices times one alphabet choice per missing position.

theorem connected_count (hc : L.graph.Connected) (r : I)
    (R : Finset (Fin (h r) → T)) (e : ℕ)
    (he : ∀ i j, L.graph.Adj i j → h i - (L.known i j).card ≤ e) :
    Fintype.card (L.RootedWords r R) ≤
      R.card * (Fintype.card T)^(e*(Fintype.card I-1)) := by
…

abbrev OAI.TorsionFreeZeroDivisors.StageLabels.Fiber line 207
abbrev OAI.TorsionFreeZeroDivisors.StageLabels.PieceWord line 208
def OAI.TorsionFreeZeroDivisors.StageLabels.restrictWord line 210
def OAI.TorsionFreeZeroDivisors.StageLabels.activeComponents line 213
def OAI.TorsionFreeZeroDivisors.StageLabels.stageWords line 216
theorem OAI.TorsionFreeZeroDivisors.StageLabels.projection_count line 224
Source documentation
Restriction to active blocks is bounded by complete strings only on the components they meet. The representative root of a component need not be active: the witness is a string, not an embedding in a sampled graph.
```
theorem projection_count (A : Finset I) (P : ((i : I) → Fin (h i) → T) → Prop)
    (Q : (c : C) → PieceWord (T := T) color h c → Prop)
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageLabels.PieceWord
def OAI.TorsionFreeZeroDivisors.StageLabels.Links.component line 259
theorem OAI.TorsionFreeZeroDivisors.StageLabels.Links.restrict_consistent line 266

theorem OAI.TorsionFreeZeroDivisors.StageLabels.Links.component_count line 273

Source documentation

Exact local bound on one actual connected component; its root is arbitrary.

theorem component_count (c : L.graph.ConnectedComponent) (r : c)
    (R : Finset (Fin (h r.val) → T)) (e : ℕ)
    (he : ∀ i j, L.graph.Adj i j → h i - (L.known i j).card ≤ e) :
    Fintype.card ((L.component c).RootedWords r R) ≤
      R.card * (Fintype.card T)^(e*(Fintype.card c-1)) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.StageLabels.Links.RootedWords

theorem OAI.TorsionFreeZeroDivisors.StageLabels.Links.active_component_size line 285
Source documentation
Sum of sizes only over components met by the stage.
```
theorem active_component_size (A : Finset I) :
    (∑ c : activeComponents L.graph.connectedComponentMk A, Fintype.card c.val) ≤
      Fintype.card I := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.StageLabels.activeComponents

theorem OAI.TorsionFreeZeroDivisors.StageLabels.Links.stage_exp line 302

Source documentation

Completing strings on each active link component before projection gives an exponential stage bound. No vertices of an inactive chain are embedded.

theorem stage_exp (A : Finset I)
    (r : (c : L.graph.ConnectedComponent) → c)
    (R : (c : L.graph.ConnectedComponent) → Finset (Fin (h (r c).val) → T))
    (P : ((i : I) → Fin (h i) → T) → Prop)
    (hP : ∀ w, P w → L.Consistent w)
    (hroot : ∀ w, P w → ∀ c, w (r c).val ∈ R c)
    (e : ℕ) (he : ∀ i j, L.graph.Adj i j → h i - (L.known i j).card ≤ e)
    (cost : L.graph.ConnectedComponent → ℝ)
    (hcost : ∀ c, ((R c).card : ℝ) ≤ Real.exp (cost c)) :
    ((stageWords h A P).card : ℝ) ≤
      Real.exp ((∑ c : activeComponents L.graph.connectedComponentMk A, cost c.val) +
        (e : ℝ) * Fintype.card I * Real.log (Fintype.card T)) := by
…

Mentions: OAI.TorsionFreeZeroDivisors.StageLabels.stageWords, OAI.TorsionFreeZeroDivisors.StageLabels.activeComponents