ActualCharging.lean`

58 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DilutedSpinGlass.MarkSelector.rademacher line 11
Source documentation
Each mark coordinate is a genuine independent fair Rademacher variable.
```
noncomputable def rademacher : FiniteLaw Bool where
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw
def OAI.DilutedSpinGlass.MarkSelector.sign line 16
theorem OAI.DilutedSpinGlass.MarkSelector.sign_sq line 18
theorem OAI.DilutedSpinGlass.MarkSelector.abs_sign line 19
theorem OAI.DilutedSpinGlass.MarkSelector.mean_sign line 20
theorem OAI.DilutedSpinGlass.MarkSelector.pair_selector line 25
Source documentation
Independent vertex marks select sharing of the vertex, not equality of spins.
```
theorem pair_selector {V : Type*} [Fintype V] [DecidableEq V] (a b : V) :
    (FiniteLaw.pi (fun _ : V => rademacher)).expect
      (fun x => sign (x a) * sign (x b)) = if a = b then 1 else 0 := by
…
```
Mentions: OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.MarkSelector.rademacher, OAI.DilutedSpinGlass.MarkSelector.sign

theorem OAI.DilutedSpinGlass.MarkSelector.requirements_selector line 42

Source documentation

Different requested color pairs use separate independent coordinates.

theorem requirements_selector {R V : Type*} [Fintype R] [DecidableEq R]
    [Fintype V] [DecidableEq V] (a b : R → V) :
    (FiniteLaw.pi (fun _ : R => FiniteLaw.pi (fun _ : V => rademacher))).expect
      (fun x => ∏ r, sign (x r (a r)) * sign (x r (b r))) =
      ∏ r, if a r = b r then (1 : ℝ) else 0 := by
…

Mentions: OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.MarkSelector.rademacher, OAI.DilutedSpinGlass.MarkSelector.sign

def OAI.DilutedSpinGlass.MarkSelector.colorMark line 57
Source documentation
Factor assigned to one color from a pair requirement. Pair endpoints are assumed distinct colors, as stipulated in the canceled-anchor expansion.
```
noncomputable def colorMark {C R V : Type*} [Fintype R] [DecidableEq C]
    (a b : R → C) (pos : C → V) (x : R → V → Bool) (c : C) : ℝ :=
…
```
theorem OAI.DilutedSpinGlass.MarkSelector.colorMark_abs line 62

theorem OAI.DilutedSpinGlass.MarkSelector.colored_selector line 73

Source documentation

Regrouping the factors assigned to colors gives precisely the selector.

theorem colored_selector {C R V : Type*} [Fintype C] [DecidableEq C]
    [Fintype R] [DecidableEq R] [Fintype V] [DecidableEq V]
    (a b : R → C) (pos : C → V) :
    (FiniteLaw.pi (fun _ : R => FiniteLaw.pi (fun _ : V => rademacher))).expect
      (fun x => ∏ c, colorMark a b pos x c) =
      ∏ r, if pos (a r) = pos (b r) then (1 : ℝ) else 0 := by
…

Mentions: OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.MarkSelector.rademacher, OAI.DilutedSpinGlass.MarkSelector.colorMark

def OAI.DilutedSpinGlass.PrescribedTree.cluster line 98
Source documentation
The actual depth-d vertex is represented by its set of descendant leaf positions. Depths range from the root through the terminal leaf positions.
```
noncomputable def cluster {n : ℕ} (S : PrescribedTree n) (d : ℕ) (a : Leaf S) :
    Finset (Leaf S) := Finset.univ.filter (fun b => d ≤ splitDepth S a b)
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth
theorem OAI.DilutedSpinGlass.PrescribedTree.mem_cluster line 101
theorem OAI.DilutedSpinGlass.PrescribedTree.cluster_eq_iff line 105
Source documentation
Equality of depth vertices is exactly sharing of the prefix.
```
theorem cluster_eq_iff {n : ℕ} (S : PrescribedTree n) {d : ℕ} (hd : d ≤ n)
    (a b : Leaf S) : cluster S d a = cluster S d b ↔ d ≤ splitDepth S a b := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.cluster, OAI.DilutedSpinGlass.PrescribedTree.splitDepth

theorem OAI.DilutedSpinGlass.PrescribedTree.tree_mark_selector line 124

Source documentation

The marker projector in pert:mark-selector on actual tree positions.

theorem tree_mark_selector {n : ℕ} (S : PrescribedTree n) {C R : Type*}
    [Fintype C] [DecidableEq C] [Fintype R] [DecidableEq R]
    (a b : R → C) (pos : C → Leaf S) (d : R → ℕ) (hd : ∀ r, d r ≤ n) :
    (FiniteLaw.pi (fun _ : R => FiniteLaw.pi
      (fun _ : Finset (Leaf S) => MarkSelector.rademacher))).expect
      (fun x => ∏ r, MarkSelector.sign (x r (cluster S (d r) (pos (a r)))) *
        MarkSelector.sign (x r (cluster S (d r) (pos (b r))))) =
      ∏ r, if d r ≤ splitDepth S (pos (a r)) (pos (b r)) then (1 : ℝ) else 0 := by
…

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.FiniteLaw.pi, OAI.DilutedSpinGlass.MarkSelector.rademacher, OAI.DilutedSpinGlass.MarkSelector.sign, OAI.DilutedSpinGlass.PrescribedTree.cluster, OAI.DilutedSpinGlass.PrescribedTree.splitDepth

theorem OAI.DilutedSpinGlass.PrescribedTree.exact_split_selector line 138
Source documentation
Exact splitting is the difference of consecutive sharing projectors.
```
theorem exact_split_selector {n : ℕ} (S : PrescribedTree n) (a b : Leaf S) (d : ℕ) :
    (if d ≤ splitDepth S a b then (1 : ℝ) else 0) -
      (if d+1 ≤ splitDepth S a b then 1 else 0) =
      if splitDepth S a b = d then 1 else 0 := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.splitDepth
def OAI.DilutedSpinGlass.PrescribedTree.branchProduct line 158
Source documentation
The local product of reference factors for k represented children. The empty and unary induced vertices contribute no factor.
```
noncomputable def branchProduct (x y : ℝ) (k : ℕ) : ℝ :=
…
```
theorem OAI.DilutedSpinGlass.PrescribedTree.branchProduct_zero line 161
theorem OAI.DilutedSpinGlass.PrescribedTree.branchProduct_one line 164
theorem OAI.DilutedSpinGlass.PrescribedTree.branchProduct_succ line 168
def OAI.DilutedSpinGlass.PrescribedTree.partialKappa line 175
theorem OAI.DilutedSpinGlass.PrescribedTree.childRefs_empty line 182
theorem OAI.DilutedSpinGlass.PrescribedTree.childRefs_insert_same line 189
theorem OAI.DilutedSpinGlass.PrescribedTree.childRefs_insert_other line 207
theorem OAI.DilutedSpinGlass.PrescribedTree.childRefs_singleton_same line 222
theorem OAI.DilutedSpinGlass.PrescribedTree.childRefs_singleton_other line 236
theorem OAI.DilutedSpinGlass.PrescribedTree.partialKappa_empty line 245
theorem OAI.DilutedSpinGlass.PrescribedTree.partialKappa_singleton line 252
theorem OAI.DilutedSpinGlass.PrescribedTree.prod_local_factor line 276
theorem OAI.DilutedSpinGlass.PrescribedTree.childRefs_eq_empty_of_unoccupied line 286
theorem OAI.DilutedSpinGlass.PrescribedTree.partialKappa_insert line 294
def OAI.DilutedSpinGlass.PrescribedTree.referencePlanRefs line 384
Source documentation
The actual final set of leaf positions in a finite reference prescription.
```
noncomputable def referencePlanRefs {n : ℕ} (T : PrescribedTree n) :
    {p : ℕ} → {s : Fin (p+1) → Leaf T} → ReferencePlan T s → Finset (Leaf T)
  | _, s, .nil => Finset.univ.image s
  | _, _, .cons _ _ _ _ next => referencePlanRefs T next
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan
theorem OAI.DilutedSpinGlass.PrescribedTree.image_cons_refs line 389
theorem OAI.DilutedSpinGlass.PrescribedTree.partialKappa_referencePlan line 408
Source documentation
The history's reference normalization is the unordered branching-vertex product, independently of the order in which the colors were added.
```
theorem partialKappa_referencePlan {n p : ℕ} (T : PrescribedTree n)
    (m : Fin (n+1) → ℝ) {s : Fin (p+1) → Leaf T} (P : ReferencePlan T s) :
    partialKappa T m (referencePlanRefs T P) =
      referencePlanNormalizer T m P * partialKappa T m (Finset.univ.image s) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Leaf, OAI.DilutedSpinGlass.PrescribedTree.ReferencePlan, OAI.DilutedSpinGlass.PrescribedTree.partialKappa, OAI.DilutedSpinGlass.PrescribedTree.referencePlanRefs, OAI.DilutedSpinGlass.PrescribedTree.referencePlanNormalizer
theorem OAI.DilutedSpinGlass.PrescribedTree.reference_history_kappa line 431

def OAI.DilutedSpinGlass.PrescribedTree.vertexDepth line 462

Source documentation

Depth and arity refer to the genuine internal vertices, not their sampled values.

def vertexDepth : {n : ℕ} → (S : PrescribedTree n) → Internal S → ℕ
  | 0, .leaf, v => nomatch v
  | _+1, .node _ C, v =>
    match (v : Option ((i : _) × Internal (C i))) with
    | none => 0
    | some ⟨i,v⟩ => vertexDepth (C i) v + 1

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal

def OAI.DilutedSpinGlass.PrescribedTree.vertexArity line 469
def OAI.DilutedSpinGlass.PrescribedTree.branchingCount line 476
theorem OAI.DilutedSpinGlass.PrescribedTree.leaves_single line 485
theorem OAI.DilutedSpinGlass.PrescribedTree.leaves_pos line 493
theorem OAI.DilutedSpinGlass.PrescribedTree.branchingCount_single line 499
theorem OAI.DilutedSpinGlass.PrescribedTree.branchingCount_grow line 511
Source documentation
One fresh growth creates at most one branching vertex; new continuations are unary. This holds even at coincident depths elsewhere in the tree.
```
theorem branchingCount_grow {n : ℕ} (S : PrescribedTree n) (v : Internal S)
    (P : ℕ → Prop) :
    branchingCount (grow S v) P = branchingCount S P +
      (if P (vertexDepth S v) ∧ vertexArity S v = 1 then 1 else 0) := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.vertexDepth, OAI.DilutedSpinGlass.PrescribedTree.vertexArity

def OAI.DilutedSpinGlass.PrescribedTree.depthCount line 555

Source documentation

Count of vertices at one depth, including unary vertices.

noncomputable def depthCount : {n : ℕ} → PrescribedTree n → ℕ → ℕ
  | 0, .leaf, _ => 0
  | _+1, .node _ _, 0 => 1
  | _+1, .node _ C, d+1 => ∑ i, depthCount (C i) d

Mentions: OAI.DilutedSpinGlass.PrescribedTree

theorem OAI.DilutedSpinGlass.PrescribedTree.depthCount_le_leaves line 560
theorem OAI.DilutedSpinGlass.PrescribedTree.depthCount_eq_sum line 570
Source documentation
Identification with the actual finite internal-vertex index type.
```
theorem depthCount_eq_sum {n : ℕ} (S : PrescribedTree n) (d : ℕ) :
    (∑ v : Internal S, if vertexDepth S v = d then (1:ℕ) else 0) = depthCount S d := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.vertexDepth, OAI.DilutedSpinGlass.PrescribedTree.depthCount
def OAI.DilutedSpinGlass.PrescribedTree.grid line 583
Source documentation
Equally spaced exponents, with an arbitrary incoming depth.
```
noncomputable def grid (n d L : ℕ) : Fin (n+1) → ℝ := fun i => (d+i.val:ℕ) / (L:ℝ)
```
theorem OAI.DilutedSpinGlass.PrescribedTree.gamma_grid_unary line 585
theorem OAI.DilutedSpinGlass.PrescribedTree.unary_depth_budget line 607
Source documentation
The sum of coefficients of unary splits at a specified depth is at most leaves/L, uniformly in the total number of levels.
```
theorem unary_depth_budget {n : ℕ} (S : PrescribedTree n) (d L q : ℕ) :
    (∑ v : Internal S, if vertexDepth S v = q ∧ vertexArity S v = 1 then
      |gamma S (grid n d L) v| else 0) ≤ (leaves S:ℝ) * (L:ℝ)⁻¹ := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.q, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.vertexDepth, OAI.DilutedSpinGlass.PrescribedTree.vertexArity, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.leaves
def OAI.DilutedSpinGlass.PrescribedTree.charged line 634
Source documentation
A charged step is precisely the first branching at a designated depth.
```
def charged {n : ℕ} (S : PrescribedTree n) (Q : Finset ℕ) (v : Internal S) : Prop :=
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal
theorem OAI.DilutedSpinGlass.PrescribedTree.unary_set_budget line 637
theorem OAI.DilutedSpinGlass.PrescribedTree.sum_abs_gamma_grid line 655
def OAI.DilutedSpinGlass.PrescribedTree.historyMass line 669
Source documentation
The absolute history sum with a terminal test. The old-leaf multiplier is exactly the number of eligible leaves (each contributes coefficient one). Fresh histories keep the genuine grow operation and coefficient at every step.
```
noncomputable def historyMass {L : ℕ} (F : PrescribedTree L → ℝ) :
    ℕ → (S : PrescribedTree L) → ℕ → ℝ
  | 0, S, _ => F S
  | k+1, S, a => (a:ℝ) * historyMass F k S (a-1) +
      ∑ v : Internal S, |gamma S (grid L 0 L) v| * historyMass F k (grow S v) a

/-- Histories having at least b charged steps, preserving their multiplicities. -/
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.charged

def OAI.DilutedSpinGlass.PrescribedTree.chargeMass line 676

Source documentation

Histories having at least b charged steps, preserving their multiplicities.

noncomputable def chargeMass {L : ℕ} (Q : Finset ℕ) :
    ℕ → (S : PrescribedTree L) → ℕ → ℕ → ℝ
  | 0, _, _, b => if b = 0 then 1 else 0
  | k+1, S, a, b => (a:ℝ) * chargeMass Q k S (a-1) b +
      ∑ v : Internal S, |gamma S (grid L 0 L) v| *
        chargeMass Q k (grow S v) a (b - if charged S Q v then 1 else 0)

/-- Exact correspondence between charging steps and actual terminal branching
vertices. Distinct vertices at the same depth are counted separately. -/

Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.Internal, OAI.DilutedSpinGlass.PrescribedTree.gamma, OAI.DilutedSpinGlass.PrescribedTree.grid, OAI.DilutedSpinGlass.PrescribedTree.grow, OAI.DilutedSpinGlass.PrescribedTree.charged

theorem OAI.DilutedSpinGlass.PrescribedTree.chargeMass_eq_historyMass line 685
Source documentation
Exact correspondence between charging steps and actual terminal branching vertices. Distinct vertices at the same depth are counted separately.
```
theorem chargeMass_eq_historyMass {L : ℕ} (Q : Finset ℕ) (B k a : ℕ)
    (S : PrescribedTree L) :
    chargeMass Q k S a (B - branchingCount S (· ∈ Q)) =
      historyMass (fun T => if B ≤ branchingCount T (· ∈ Q) then 1 else 0) k S a := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.chargeMass, OAI.DilutedSpinGlass.PrescribedTree.branchingCount, OAI.DilutedSpinGlass.PrescribedTree.historyMass
def OAI.DilutedSpinGlass.PrescribedTree.chargeBound line 709
theorem OAI.DilutedSpinGlass.PrescribedTree.chargeBound_nonneg line 714
theorem OAI.DilutedSpinGlass.PrescribedTree.chargeBound_scale line 725
Source documentation
Every specified split contributes one factor delta; constants are independent of the grid denominator. This also handles arbitrarily repeated target depths.
```
theorem chargeBound_scale (C D δ : ℝ) (k b : ℕ) :
    chargeBound C (D*δ) k b = chargeBound C D k b * δ^b := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree.chargeBound
theorem OAI.DilutedSpinGlass.PrescribedTree.chargeMass_bound line 737
Source documentation
A genuine history estimate, not a distribution postulated from the desired identity. R bounds the leaves during all the remaining growth steps.
```
theorem chargeMass_bound {L : ℕ} (hL : 0 < L) (Q : Finset ℕ) (R k b a : ℕ)
    (S : PrescribedTree L) (ha : a ≤ leaves S) (hR : leaves S + k ≤ R) :
    chargeMass Q k S a b ≤
      chargeBound (2*(R:ℝ)) ((Q.card:ℝ)*(R:ℝ)*(L:ℝ)⁻¹) k b := by
…
```
Mentions: OAI.DilutedSpinGlass.PrescribedTree, OAI.DilutedSpinGlass.PrescribedTree.leaves, OAI.DilutedSpinGlass.PrescribedTree.chargeMass, OAI.DilutedSpinGlass.PrescribedTree.chargeBound
theorem OAI.DilutedSpinGlass.PrescribedTree.charging_final_shape line 814