ScheduledFrameGeometry.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.branchingCount_heightCast line 12
lemma OAI.DilutedSpinGlass.PrescribedTree.branchRegular_heightCast line 15
lemma OAI.DilutedSpinGlass.PrescribedTree.branchingCount_splitFrame_bottom line 19

theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_frame_old_count line 34

Source documentation

The scheduled old frame has no charged internal branching vertex. No regularity of a union of old and target trees is postulated.

theorem scheduled_frame_old_count (H r d : ℕ) (k : ℕ+) (a : α)
    (C : Fin k → ReducedTopology) (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
    (Q : α → Fin (H+1+1+r+1+d))
    (had : ∀ j, Admissible (C j) (fun v => (Q (e j v)).val) (r+1+d+1) (r+1+d+1+H))
    (hno : NoAdjacentBranchDepths
      (stem (PrescribedTree.node k (fun j => realize H (r+1+d+1) (C j) (fun v => (Q (e j v)).val))) r)) :
    let Base := PrescribedTree.node k (fun j => realize H (r+1+d+1) (C j) (fun v => (Q (e j v)).val))
…

Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.ReducedTopology.realize

theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_frame_target_count line 58
Source documentation
The delayed scheduled target contains exactly two occurrences of each branching vertex of the base, even if both copies have equal assigned depths.
```
theorem scheduled_frame_target_count (H r d : ℕ) (k : ℕ+) (a : α)
    (C : Fin k → ReducedTopology) (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
    (Q : α → Fin (H+1+1+r+1+d)) :
    let Base := PrescribedTree.node k (fun j => realize H (r+1+d+1) (C j) (fun v => (Q (e j v)).val))
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.realize

theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_frame_target_total line 80

Source documentation

All target branches except the protected separation vertex are charged.

theorem scheduled_frame_target_total (H r d : ℕ) (k : ℕ+) (a : α)
    (C : Fin k → ReducedTopology) (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
    (Q : α → Fin (H+1+1+r+1+d)) :
    let Base := PrescribedTree.node k (fun j => realize H (r+1+d+1) (C j) (fun v => (Q (e j v)).val))
…

Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.realize

theorem OAI.DilutedSpinGlass.ReducedTopology.scheduled_frame_target_regular line 103

Source documentation

Higher-degree target factors are uniformly interior at every regular first split. No premise is imposed on an overlay of the two shapes.

theorem scheduled_frame_target_regular (H r d : ℕ) (k : ℕ+) (a : α)
    (C : Fin k → ReducedTopology) (e : (j : Fin k) → (C j).Vertex → {j : α // j≠a})
    (Q : α → Fin (H+1+1+r+1+d)) (η : ℝ)
    (heval : η≤((d+r+2:ℕ):ℝ)/((H+1+1+r+1+d:ℕ):ℝ)) :
    let New := PrescribedTree.node k (fun j => realize H (r+1+1+d+1) (C j) (fun v => (Q (e j v)).val+1))
…

Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.realize

def OAI.DilutedSpinGlass.PrescribedTree.canonicalMatrixTail line 126
Source documentation
The literal tail of the universal dictionary's reversed insertion list.
```
def canonicalMatrixTail (t : ℕ) : List (Option (Fin (t+1))) :=
…
```
lemma OAI.DilutedSpinGlass.PrescribedTree.canonicalMatrixHistory line 129
lemma OAI.DilutedSpinGlass.PrescribedTree.canonicalMatrixTail_nodup line 135
lemma OAI.DilutedSpinGlass.PrescribedTree.canonicalMatrixTail_not_mem line 139
lemma OAI.DilutedSpinGlass.PrescribedTree.canonicalMatrixTail_full line 148