ScheduledProtectedLabels.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.leaves_stem line 12
lemma OAI.DilutedSpinGlass.PrescribedTree.leaves_doubled line 18
lemma OAI.DilutedSpinGlass.PrescribedTree.leaves_splitFrame line 23
lemma OAI.DilutedSpinGlass.ReducedTopology.delayed_node_leaves line 35
Source documentation
The shifted children retain exactly their topology leaves. In particular one fixed dictionary arity works for every admissible depth assignment.
```
lemma delayed_node_leaves (H lo : ℕ) (k : ℕ+) (hk : 2≤(k:ℕ))
    (C : Fin k → ReducedTopology) (q : (j : Fin k) → (C j).Vertex → ℕ)
    (had : ∀ j, Admissible (C j) (q j) lo (lo+H)) :
    leaves (PrescribedTree.node k (fun j => realize H (lo+1) (C j)
      (fun v => q j v+1))) = Fintype.card (ReducedTopology.node k hk C).Leaf := by
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.ReducedTopology.realize, OAI.DilutedSpinGlass.ReducedTopology.Leaf
theorem OAI.DilutedSpinGlass.ReducedTopology.delayed_node_protected_labeling line 49
Source documentation
Actual assignment-dependent protected labeling for the genuinely delayed multileaf target. The dictionary size depends only on the reduced topology, not the grid horizon or any of its branching-coordinate assignments.
```
theorem delayed_node_protected_labeling (H lo r d : ℕ) (k : ℕ+)
    (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology)
    (q : (j : Fin k) → (C j).Vertex → ℕ)
    (had : ∀ j, Admissible (C j) (q j) lo (lo+H)) :
    let S := PrescribedTree.node k (fun j => realize H (lo+1) (C j)
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.ReducedTopology.Vertex, OAI.DilutedSpinGlass.ReducedTopology.Admissible, OAI.DilutedSpinGlass.ReducedTopology.realize

theorem OAI.DilutedSpinGlass.ReducedTopology.regular_node_labeled_frame line 77

Source documentation

Full regular-domain frame and protected-label extraction, with the exact old and delayed integer levels used by the physical multileaf inequality.

theorem regular_node_labeled_frame {L : ℕ} [NeZero L] {η : ℝ} (hη : 0<η)
    (hlarge : 1<η*(L:ℝ)) (k : ℕ+) (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology)
    (Q : Option (ReducedTopology.node k hk C).Vertex → Fin L)
    (hQ : regularShapeDomain (.node k hk C) L η Q) :
    ∃ H r d : ℕ, L=H+1+1+r+1+(d+1) ∧ (Q none).val=d+1 ∧
      (Q (some none)).val=r+1+(d+1) ∧
      (∀ j, Admissible (C j) (fun v => (Q (some (some ⟨j,v⟩))).val)
        (r+1+(d+1)+1) (r+1+(d+1)+1+H)) ∧
      let S := PrescribedTree.node k (fun j =>
…

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