TreeParticles.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Deterministic causal recursion on a rooted finite tree. The depth certificate is constructed from graph distance below; it is not an embedding hypothesis.

structure OAI.BoundedTreewidthL1.RootedForest line 11
def OAI.BoundedTreewidthL1.RootedForest.run line 19
lemma OAI.BoundedTreewidthL1.RootedForest.run_eq line 28
lemma OAI.BoundedTreewidthL1.RootedForest.run_invariant line 33
lemma OAI.BoundedTreewidthL1.RootedForest.run_measurable line 46
def OAI.BoundedTreewidthL1.TreeParticles.interface line 68
def OAI.BoundedTreewidthL1.TreeParticles.retained line 70
def OAI.BoundedTreewidthL1.TreeParticles.fresh line 72
def OAI.BoundedTreewidthL1.TreeParticles.seed line 74
def OAI.BoundedTreewidthL1.TreeParticles.step line 76
def OAI.BoundedTreewidthL1.TreeParticles.state line 79
lemma OAI.BoundedTreewidthL1.TreeParticles.retained_subset line 83
lemma OAI.BoundedTreewidthL1.TreeParticles.batch_data line 90
lemma OAI.BoundedTreewidthL1.TreeParticles.interface_card line 102
lemma OAI.BoundedTreewidthL1.TreeParticles.state_eq line 111

theorem OAI.BoundedTreewidthL1.TreeParticles.forest_particle_realization line 120

Source documentation

Actual branching preparation for active-scale keys. Children use their own copies of the parent's list; no consistency assumption on sampled bag laws.

theorem forest_particle_realization (R : RootedForest I) (bag : I → Finset V)
    (A : I → Finset J) (k q : ℕ) (hbag : ∀ i, (bag i).card ≤ k)
    (hA : ∀ i, (A i).card ≤ q) (hN : Fintype.card ι = 2*q + k.factorial + 2)
    (d : V → V → ℝ) (L H Δ : ℝ) (hH : 0 < H) (hΔ : 0 < Δ)
    (g : I → J → V → ℝ)
    (hLip : ∀ i a, ∀ u v, |g i a u - g i a v| ≤ L*d u v)
    (hHeight : ∀ i a v, |g i a v| ≤ H)
    (hzero : ∀ i a, ∀ v ∈ interface R bag i, g i a v = 0) :
    let M := H*((Fintype.card ι : ℝ)-1)+2*Δ
…

Mentions: OAI.BoundedTreewidthL1.RootedForest, OAI.BoundedTreewidthL1.TreeParticles.interface

theorem OAI.BoundedTreewidthL1.TreeParticles.measurable_state line 204
Source documentation
Measurability of the actual branching preparation, with all randomness sampled beforehand. No measurable-choice assumption about the particle lists.
```
theorem measurable_state (R : RootedForest I) (bag : I → Finset V) (A : I → Finset J)
    (g : Ω → I → J → V → ℝ)
    (hg : ∀ i a v, Measurable (fun ω => g ω i a v)) (i : I) :
    Measurable (fun ω => state (ι := ι) R bag A (g ω) i) := by
…
```
Mentions: OAI.BoundedTreewidthL1.RootedForest, OAI.BoundedTreewidthL1.TreeParticles.state