RegularNodeGeometry.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.PrescribedTree.leaves_heightCast line 8
lemma OAI.DilutedSpinGlass.PrescribedTree.canonicalMatrixTail_length line 11
def OAI.DilutedSpinGlass.ReducedTopology.nodeHistoryBudget line 22
Source documentation
A grid-independent budget for all leaves and history colors used in the aligned two-copy experiment of a fixed topology.
```
def nodeHistoryBudget (k : ℕ+) (hk : 2≤(k:ℕ)) (C : Fin k → ReducedTopology) : ℕ :=
…
```
Mentions: OAI.DilutedSpinGlass.ReducedTopology
def OAI.DilutedSpinGlass.ReducedTopology.nodeChargeConstant line 25
lemma OAI.DilutedSpinGlass.ReducedTopology.nodeChargeConstant_nonneg line 31
lemma OAI.DilutedSpinGlass.ReducedTopology.node_realize_leaves line 37
lemma OAI.DilutedSpinGlass.ReducedTopology.node_old_realize_leaves line 46

theorem OAI.DilutedSpinGlass.ReducedTopology.node_frame_charge_uniform line 64

Source documentation

The actual frame charging cost is bounded only by the reduced topology and the separation parameter. The canonical ratio and vertex multiplicities are retained; no maximization over a grid-dependent majorant is used.

theorem node_frame_charge_uniform (H r d : ℕ) (k : ℕ+) (hk : 2≤(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))
    {η : ℝ} (hη : 0<η)
    (heval : η≤((d+r+2:ℕ):ℝ)/((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.Admissible, OAI.DilutedSpinGlass.ReducedTopology.realize