Rounding.lean`

190 declarations, 0 contain sorry, 0 declared as axioms

Continuation of Section09: finite top-down tree coupling. The sampled ancestors are retained as part of the joint state; no conditional means given those ancestors are assumed.

def OAI.KServer.Rounding.move line 15
lemma OAI.KServer.Rounding.move_nonneg line 19
lemma OAI.KServer.Rounding.move_sum line 33
lemma OAI.KServer.Rounding.move_coordinate line 45
abbrev OAI.KServer.Rounding.Outcome line 54
Source documentation
Each fiber records the actual observed total, not a conditional mean.
```
abbrev Outcome (r : S → ℕ) := {x : S × Finset I // x.2.card = r x.1}
```
def OAI.KServer.Rounding.subset line 56
def OAI.KServer.Rounding.state line 57
def OAI.KServer.Rounding.Marginal line 59
def OAI.KServer.Rounding.Mass line 62
def OAI.KServer.Rounding.Feasible line 65
lemma OAI.KServer.Rounding.mass_total line 69
lemma OAI.KServer.Rounding.marginal_total line 77
lemma OAI.KServer.Rounding.feasible_mass line 92
lemma OAI.KServer.Rounding.move_feasible line 97
lemma OAI.KServer.Rounding.continuous_mass line 106
lemma OAI.KServer.Rounding.continuous_marginal line 111
lemma OAI.KServer.Rounding.feasible_compact line 116
def OAI.KServer.Rounding.Objective line 134
lemma OAI.KServer.Rounding.objective_continuous line 139
lemma OAI.KServer.Rounding.exists_minimizer line 148
def OAI.KServer.Rounding.exchange line 154
lemma OAI.KServer.Rounding.exchange_card line 157
lemma OAI.KServer.Rounding.exchange_indicator line 164
def OAI.KServer.Rounding.afterExchange line 174
lemma OAI.KServer.Rounding.exchange_state line 179
lemma OAI.KServer.Rounding.move_exchange_marginal line 183
lemma OAI.KServer.Rounding.deviation_descent line 194
lemma OAI.KServer.Rounding.discrepancy_pair line 220
lemma OAI.KServer.Rounding.support_mem line 238
lemma OAI.KServer.Rounding.support_notMem line 251
lemma OAI.KServer.Rounding.exists_bridge line 265
def OAI.KServer.Rounding.ExchangeCost line 284
Source documentation
The local Lipschitz property needed by the repair objective. It will be instantiated by Hamming distance from the state's preliminary rounding.
```
def ExchangeCost {r : S → ℕ} (c : Outcome (I := I) r → ℝ) : Prop :=
…
```
Mentions: OAI.KServer.Rounding.Outcome
lemma OAI.KServer.Rounding.one_exchange_improves line 288
lemma OAI.KServer.Rounding.two_exchanges_improve line 315
lemma OAI.KServer.Rounding.minimizer_marginals line 361
Source documentation
A minimizer has the prescribed unconditional marginals, even when different fibers have different adjacent totals. This is the source's essential correlation-tolerant two-state exchange argument.
```
lemma minimizer_marginals {r : S → ℕ} {p₀ p c : Outcome (I := I) r → ℝ} {f : I → ℝ}
…
```
Mentions: OAI.KServer.Rounding.Outcome
theorem OAI.KServer.Rounding.finite_repair line 392
Source documentation
The compact finite-law repair step, including its quantitative cost bound.
```
theorem finite_repair {r : S → ℕ} (p₀ c : Outcome (I := I) r → ℝ) (f : I → ℝ)
…
```
Mentions: OAI.KServer.Rounding.Outcome
def OAI.KServer.Rounding.hamming line 404
lemma OAI.KServer.Rounding.hamming_self line 407
lemma OAI.KServer.Rounding.hamming_triangle line 409
lemma OAI.KServer.Rounding.hamming_exchange line 413
def OAI.KServer.Rounding.HammingCost line 428
lemma OAI.KServer.Rounding.hamming_exchangeCost line 432
def OAI.KServer.Rounding.seed line 441
lemma OAI.KServer.Rounding.seed_nonneg line 445
lemma OAI.KServer.Rounding.seed_sum line 450
lemma OAI.KServer.Rounding.seed_total line 459
lemma OAI.KServer.Rounding.seed_mass line 463
lemma OAI.KServer.Rounding.seed_marginal line 468

theorem OAI.KServer.Rounding.hamming_repair line 474

Source documentation

Joint-law repair in the exact Hamming metric of the manuscript. All correlation is retained by preserving every original state probability.

theorem hamming_repair (w : S → ℝ) (hw : ∀ ω, 0 ≤ w ω) (h₁ : ∑ ω, w ω = 1)
    (r : S → ℕ) (hr : ∀ ω ν, r ω ≤ r ν + 1) (A₀ : S → Finset I)
    (hA : ∀ ω, (A₀ ω).card = r ω) (f : I → ℝ) (hf : ∀ i, 0 ≤ f i ∧ f i ≤ 1)
    (hs : ∑ i, f i = ∑ ω, w ω * r ω) :
    ∃ p : Outcome (I := I) r → ℝ, (∀ x, 0 ≤ p x) ∧ (∀ ω, Mass p ω = w ω) ∧
…

Mentions: OAI.KServer.Rounding.Outcome, OAI.KServer.Rounding.Mass

lemma OAI.KServer.Rounding.hamming_comm line 495
lemma OAI.KServer.Rounding.hamming_subset line 500
lemma OAI.KServer.Rounding.adjust_subset line 512
Source documentation
Deterministic adjustment to any attainable integer total, with optimal Hamming cost. The permitted coordinates H may omit all integral targets.
```
lemma adjust_subset (H A : Finset I) (hAH : A ⊆ H) {r : ℕ} (hr : r ≤ H.card) :
    ∃ B : Finset I, B ⊆ H ∧ B.card = r ∧ hamming B A = |(r : ℝ) - A.card| := by
…
```
Mentions: OAI.KServer.Rounding.hamming
def OAI.KServer.Rounding.clip line 539
Source documentation
The literal scalar interval used by the source's preliminary clipping.
```
def clip (b : ℝ) (x : ℤ) : ℤ := max ⌊b⌋ (min ⌈b⌉ x)
```
def OAI.KServer.Rounding.Balanced line 541
lemma OAI.KServer.Rounding.balanced_iff_bounds line 543
lemma OAI.KServer.Rounding.clip_balanced line 550
lemma OAI.KServer.Rounding.balanced_bounds line 554
lemma OAI.KServer.Rounding.clip_up line 557
lemma OAI.KServer.Rounding.clip_down line 562

lemma OAI.KServer.Rounding.clipping_bound line 570

Source documentation

Exact source clipping estimate, with arbitrary finite weights and no independence assumptions.

lemma clipping_bound (w : S → ℝ) (_hw : ∀ ω, 0 ≤ w ω) (h₁ : ∑ ω, w ω = 1)
    {a b : ℝ} (X : S → ℤ) (hX : ∀ ω, Balanced a (X ω))
    (hmean : ∑ ω, w ω * (X ω : ℝ) = a) :
    (∑ ω, w ω * |(clip b (X ω) : ℝ) - X ω|) ≤ |a - b| := by
…

Mentions: OAI.KServer.Rounding.Balanced, OAI.KServer.Rounding.clip

def OAI.KServer.Rounding.fraction line 598
def OAI.KServer.Rounding.fractionalSet line 600
def OAI.KServer.Rounding.liftSet line 602
lemma OAI.KServer.Rounding.fraction_range line 605
lemma OAI.KServer.Rounding.ceil_formula line 609
lemma OAI.KServer.Rounding.not_fractional line 614
lemma OAI.KServer.Rounding.fraction_zero_iff line 620
lemma OAI.KServer.Rounding.liftSet_sum line 629
lemma OAI.KServer.Rounding.liftSet_balanced line 633
lemma OAI.KServer.Rounding.balanced_liftSet line 644
lemma OAI.KServer.Rounding.liftSet_distance line 665
lemma OAI.KServer.Rounding.total_endpoints line 675
def OAI.KServer.Rounding.residual line 694
lemma OAI.KServer.Rounding.residual_cast line 697
lemma OAI.KServer.Rounding.residual_bound line 704
lemma OAI.KServer.Rounding.residual_adjacent line 711
lemma OAI.KServer.Rounding.residual_cast_real line 722
lemma OAI.KServer.Rounding.residual_mean line 728

lemma OAI.KServer.Rounding.preliminary_state line 735

Source documentation

The statewise preliminary adjustment has exactly the source's cost.

lemma preliminary_state (b : I → ℝ) (X : I → ℤ) {N : ℤ}
    (hN : Balanced (∑ i, b i) N) :
    ∃ A : Finset I, A ⊆ fractionalSet b ∧ A.card = residual b N ∧
      (∑ i, |(liftSet b A i : ℝ) - clip (b i) (X i)|) =
        |(N : ℝ) - ∑ i, (clip (b i) (X i) : ℝ)| := by
…

Mentions: OAI.KServer.Rounding.Balanced, OAI.KServer.Rounding.fractionalSet, OAI.KServer.Rounding.residual, OAI.KServer.Rounding.liftSet, OAI.KServer.Rounding.clip

def OAI.KServer.Rounding.mean line 752
def OAI.KServer.Rounding.dist₁ line 754
lemma OAI.KServer.Rounding.dist₁_triangle line 757
lemma OAI.KServer.Rounding.abs_total_le line 763
lemma OAI.KServer.Rounding.mean_mono line 768
lemma OAI.KServer.Rounding.mean_add line 773
lemma OAI.KServer.Rounding.mean_abs_sub line 778
lemma OAI.KServer.Rounding.dist₁_mean line 787
lemma OAI.KServer.Rounding.preliminary_bounds line 796
lemma OAI.KServer.Rounding.weighted_state line 843
lemma OAI.KServer.Rounding.liftSet_mean line 853
lemma OAI.KServer.Rounding.marginal_support line 863
theorem OAI.KServer.Rounding.rounding_star_joint line 882
Source documentation
Full finite joint-law formulation of Section 09's star lemma. The first coordinate retains the original state and hence all its correlations. A kernel is obtained by finite disintegration below. Nonnegativity of a,b is needed only to deduce nonnegative integer output, not for this stronger signed statement.
```
theorem rounding_star_joint (w : S → ℝ) (hw : ∀ ω, 0 ≤ w ω) (h₁ : ∑ ω, w ω = 1)
    (a b : I → ℝ) (X : S → I → ℤ) (N : S → ℤ)
    (hX : ∀ ω i, Balanced (a i) (X ω i))
    (hmX : ∀ i, mean w (fun ω => (X ω i : ℝ)) = a i)
    (hN : ∀ ω, Balanced (∑ i, b i) (N ω))
    (hmN : mean w (fun ω => (N ω : ℝ)) = ∑ i, b i) :
    ∃ (p : Outcome (I := I) (fun ω => residual b (N ω)) → ℝ)
…
```
Mentions: OAI.KServer.Rounding.Balanced, OAI.KServer.Rounding.mean, OAI.KServer.Rounding.Outcome, OAI.KServer.Rounding.residual
def OAI.KServer.Rounding.conditionalKernel line 969
Source documentation
Finite disintegration, including genuinely zero-probability input states.
```
def conditionalKernel (w : S → ℝ) (p : J → ℝ) (st : J → S) (e : S → J)
    (ω : S) (j : J) : ℝ :=
…
```
lemma OAI.KServer.Rounding.conditionalKernel_nonneg line 975
lemma OAI.KServer.Rounding.conditionalKernel_sum line 986
lemma OAI.KServer.Rounding.conditionalKernel_identity line 994
lemma OAI.KServer.Rounding.conditionalKernel_average line 1010

theorem OAI.KServer.Rounding.rounding_star line 1024

Source documentation

The source's exact finite randomized kernel, with the constants 32 and 11, all correlations preserved, and valid outputs even at null input states.

theorem rounding_star (w : S → ℝ) (hw : ∀ ω, 0 ≤ w ω) (h₁ : ∑ ω, w ω = 1)
    (a b : I → ℝ) (_ha : ∀ i, 0 ≤ a i) (hb : ∀ i, 0 ≤ b i)
    (X : S → I → ℤ) (N : S → ℤ)
    (hX : ∀ ω i, Balanced (a i) (X ω i))
    (hmX : ∀ i, mean w (fun ω => (X ω i : ℝ)) = a i)
    (hN : ∀ ω, Balanced (∑ i, b i) (N ω))
    (hmN : mean w (fun ω => (N ω : ℝ)) = ∑ i, b i) :
    ∃ (κ : S → Outcome (I := I) (fun ω => residual b (N ω)) → ℝ)
…

Mentions: OAI.KServer.Rounding.Balanced, OAI.KServer.Rounding.mean, OAI.KServer.Rounding.Outcome, OAI.KServer.Rounding.residual

structure OAI.KServer.TreeRounding.Law line 1076
def OAI.KServer.TreeRounding.Law.avg line 1085
lemma OAI.KServer.TreeRounding.Law.avg_const line 1088
lemma OAI.KServer.TreeRounding.Law.avg_add line 1091
lemma OAI.KServer.TreeRounding.Law.avg_sub line 1095
lemma OAI.KServer.TreeRounding.Law.avg_sum line 1099
lemma OAI.KServer.TreeRounding.Law.avg_mono line 1103
lemma OAI.KServer.TreeRounding.Law.avg_nonneg line 1106
lemma OAI.KServer.TreeRounding.Law.avg_congr line 1109

def OAI.KServer.TreeRounding.Law.extend line 1114

Source documentation

A finite extension with a normalized kernel retains the entire old state.

def Law.extend {α β J : Type} [Fintype J] (L : Law α) (κ : L.Ω → J → ℝ)
    (hκ : ∀ ω j, 0 ≤ κ ω j) (hκ1 : ∀ ω, ∑ j, κ ω j=1)
    (z : L.Ω → J → β) : Law (α × β) where
…

Mentions: OAI.KServer.TreeRounding.Law

lemma OAI.KServer.TreeRounding.Law.extend_avg line 1124
lemma OAI.KServer.TreeRounding.Law.extend_old line 1133
def OAI.KServer.TreeRounding.Law.map line 1140
lemma OAI.KServer.TreeRounding.Law.map_avg line 1143
structure OAI.KServer.TreeRounding.Tree line 1146
abbrev OAI.KServer.TreeRounding.Tree.Child line 1153
instance OAI.KServer.TreeRounding.(instance at line 1154) line 1154
instance OAI.KServer.TreeRounding.(instance at line 1158) line 1158
lemma OAI.KServer.TreeRounding.Tree.child_gt line 1160
def OAI.KServer.TreeRounding.Tree.park line 1163
def OAI.KServer.TreeRounding.Tree.star line 1166
lemma OAI.KServer.TreeRounding.Tree.star_sum line 1170
structure OAI.KServer.TreeRounding.Counts line 1174
structure OAI.KServer.TreeRounding.PairState line 1178
def OAI.KServer.TreeRounding.Tree.intStar line 1182
def OAI.KServer.TreeRounding.Tree.Consistent line 1186
lemma OAI.KServer.TreeRounding.Tree.intStar_sum line 1189
def OAI.KServer.TreeRounding.Tree.Valid line 1193
def OAI.KServer.TreeRounding.Tree.Means line 1197
def OAI.KServer.TreeRounding.Tree.setStar line 1202
Source documentation
Set just the new children and the new park of one star.
```
def Tree.setStar (T : Tree n) (c : Counts n) (v : Fin n)
    (z : Option (T.Child v) → ℤ) : Counts n where
…
```
Mentions: OAI.KServer.TreeRounding.Tree, OAI.KServer.TreeRounding.Counts
lemma OAI.KServer.TreeRounding.Tree.setStar_old line 1207
lemma OAI.KServer.TreeRounding.Tree.setStar_child line 1211
lemma OAI.KServer.TreeRounding.Tree.setStar_root line 1216
lemma OAI.KServer.TreeRounding.Tree.setStar_self line 1220
lemma OAI.KServer.TreeRounding.Tree.setStar_intStar line 1228
lemma OAI.KServer.TreeRounding.Tree.setStar_other line 1236
lemma OAI.KServer.TreeRounding.Tree.setStar_before line 1247
def OAI.KServer.TreeRounding.Tree.Assigned line 1256
lemma OAI.KServer.TreeRounding.Tree.assigned_self line 1259
lemma OAI.KServer.TreeRounding.Tree.assigned_next line 1264
lemma OAI.KServer.TreeRounding.Tree.assigned_not_child line 1275
structure OAI.KServer.TreeRounding.Stage line 1284
Source documentation
The induction stores the original joint law and every already rounded ancestor, so all conditional correlations are retained.
```
structure Stage (T : Tree n) (a b : Fin n → ℝ) (k : ℤ)
    (L₀ : Law (Counts n)) (m : ℕ) where
…
```
Mentions: OAI.KServer.TreeRounding.Tree, OAI.KServer.TreeRounding.Law, OAI.KServer.TreeRounding.Counts

lemma OAI.KServer.TreeRounding.Stage.oldMean line 1306

Source documentation

The saved old law's means are valid at every intermediate refinement.

lemma Stage.oldMean {T : Tree n} {a b : Fin n → ℝ} {k : ℤ} {L₀ : Law (Counts n)}
    {m : ℕ} (S : Stage T a b k L₀ m) (hmean : T.Means a L₀) (v : Fin n)
    (i : Option (T.Child v)) :
    mean S.law.weight (fun ω => (T.intStar (S.law.point ω).old v i:ℝ))=T.star a v i := by
…

Mentions: OAI.KServer.TreeRounding.Tree, OAI.KServer.TreeRounding.Law, OAI.KServer.TreeRounding.Counts, OAI.KServer.TreeRounding.Stage

def OAI.KServer.TreeRounding.stepLaw line 1317

Source documentation

A finite kernel is extended and its output written into one star.

def stepLaw {T : Tree n} (L : Law (PairState n)) (v : Fin n) {J : Type} [Fintype J]
    (κ : L.Ω → J → ℝ) (hκ : ∀ ω j, 0 ≤ κ ω j) (hκ1 : ∀ ω, ∑ j, κ ω j=1)
    (z : L.Ω → J → Option (T.Child v) → ℤ) : Law (PairState n) :=
…

Mentions: OAI.KServer.TreeRounding.Tree, OAI.KServer.TreeRounding.Law, OAI.KServer.TreeRounding.PairState

lemma OAI.KServer.TreeRounding.stepLaw_avg line 1322
lemma OAI.KServer.TreeRounding.stepLaw_preserve line 1331

theorem OAI.KServer.TreeRounding.Stage.next line 1343

Source documentation

One complete top-down update. The only existence input is the proved finite star kernel, not a policy or a tree-rounding interface.

theorem Stage.next {T : Tree n} {a b : Fin n → ℝ} {k : ℤ} {L₀ : Law (Counts n)}
    (ha : ∀ v, 0 ≤ a v) (hpa : ∀ v, 0 ≤ T.park a v)
    (hb : ∀ v, 0 ≤ b v) (hpb : ∀ v, 0 ≤ T.park b v)
    (hmean : T.Means a L₀) (v : Fin n) (S : Stage T a b k L₀ v.val) :
    Nonempty (Stage T a b k L₀ (v.val+1)) := by
…

Mentions: OAI.KServer.TreeRounding.Tree, OAI.KServer.TreeRounding.Law, OAI.KServer.TreeRounding.Counts, OAI.KServer.TreeRounding.Stage

def OAI.KServer.TreeRounding.initialCounts line 1486
lemma OAI.KServer.TreeRounding.stage_zero line 1490

theorem OAI.KServer.TreeRounding.tree_coupling line 1524

Source documentation

All vertices are processed in increasing order; the parent order is the only tree-shape assumption used by the constructive correlated coupling.

theorem tree_coupling {T : Tree n} {a b : Fin n → ℝ} {k : ℤ}
    (ha : ∀ v, 0 ≤ a v) (hpa : ∀ v, 0 ≤ T.park a v)
    (hb : ∀ v, 0 ≤ b v) (hpb : ∀ v, 0 ≤ T.park b v)
    (hk : 0 ≤ k) (hb0 : b 0=(k:ℝ)) (L₀ : Law (Counts n))
    (hvalid : ∀ ω, T.Valid a (L₀.point ω)) (hmean : T.Means a L₀) :
    ∃ L : Law (PairState n),
      (∀ f : Counts n → ℝ, L.avg (fun s => f s.old)=L₀.avg f) ∧
      (∀ ω, T.Valid a (L.point ω).old ∧ T.Valid b (L.point ω).new ∧ (L.point ω).new.subtree 0=k) ∧
      (∀ v, L.avg (fun s => (s.new.subtree v:ℝ))=b v) ∧
      (∀ v, L.avg (fun s => (s.new.park v:ℝ))=T.park b v) ∧
      (∀ v, L.avg (fun s => dist₁ (fun i => (T.intStar s.new v i:ℝ))
                                  (fun i => (T.intStar s.old v i:ℝ))) ≤
…

Mentions: OAI.KServer.TreeRounding.Tree, OAI.KServer.TreeRounding.Law, OAI.KServer.TreeRounding.Counts, OAI.KServer.TreeRounding.PairState

lemma OAI.KServer.TreeRounding.Law.avg_mul line 1557
lemma OAI.KServer.TreeRounding.Law.avg_le_of_support line 1561
def OAI.KServer.TreeRounding.Tree.childEquiv line 1566
Source documentation
Every nonroot vertex occurs in exactly one child list.
```
def Tree.childEquiv (T : Tree n) : (Σ v : Fin n, T.Child v) ≃ {v : Fin n // v≠0} where
…
```
Mentions: OAI.KServer.TreeRounding.Tree
lemma OAI.KServer.TreeRounding.Tree.weighted_children line 1576
lemma OAI.KServer.TreeRounding.Tree.star_distance line 1596
lemma OAI.KServer.TreeRounding.Tree.children_distance_le line 1611

lemma OAI.KServer.TreeRounding.Tree.parent_weight line 1618

Source documentation

The radius at a nonroot node is one tau-th of its parent radius.

lemma Tree.parent_weight (T : Tree n) {τ : ℝ} (hτ : 0 < τ) (w f : Fin n → ℝ)
    (hscale : ∀ u, u≠0 → w (T.parent u)=τ*w u) (h0 : f 0=0) :
    (∑ u, w u*f u)=(1/τ)*(∑ u, w (T.parent u)*f u) := by
…

Mentions: OAI.KServer.TreeRounding.Tree

lemma OAI.KServer.TreeRounding.Tree.star_weight_bound line 1629

theorem OAI.KServer.TreeRounding.Tree.rounding_absorption line 1644

Source documentation

Finite, exact absorption of the local 32/11 bounds. No tree depth or initialization cost enters the coefficient.

theorem Tree.rounding_absorption (T : Tree n) {τ : ℝ} (hτ : 22 ≤ τ)
    (w a b : Fin n → ℝ) (hw : ∀ u, 0 ≤ w u)
    (hscale : ∀ u, u≠0 → w (T.parent u)=τ*w u) (h0 : a 0=b 0)
    (L : Law (PairState n)) (hroot : ∀ ω, (L.point ω).new.subtree 0=(L.point ω).old.subtree 0)
    (hcost : ∀ v, L.avg (fun s => dist₁ (fun i => (T.intStar s.new v i:ℝ))
                                  (fun i => (T.intStar s.old v i:ℝ))) ≤
      32*dist₁ (T.star a v) (T.star b v)+
        11*L.avg (fun s => |(s.new.subtree v:ℝ)-(s.old.subtree v:ℝ)|)) :
    L.avg (fun s => ∑ u, w (T.parent u)*|(s.new.subtree u:ℝ)-(s.old.subtree u:ℝ)|) ≤
      132*(∑ u, w (T.parent u)*|a u-b u|) := by
…

Mentions: OAI.KServer.TreeRounding.Tree, OAI.KServer.TreeRounding.Law, OAI.KServer.TreeRounding.PairState

def OAI.KServer.TreeRounding.Law.pure line 1697
lemma OAI.KServer.TreeRounding.Law.avg_pure line 1705
lemma OAI.KServer.TreeRounding.balanced_integer line 1709
def OAI.KServer.TreeRounding.stock line 1713
Source documentation
Deterministic park of all k units at the root, solely for initialization.
```
def stock (k : ℤ) : Counts n where
…
```
Mentions: OAI.KServer.TreeRounding.Counts
def OAI.KServer.TreeRounding.stockMass line 1717
lemma OAI.KServer.TreeRounding.stockMass_park line 1719
lemma OAI.KServer.TreeRounding.stock_valid line 1725
lemma OAI.KServer.TreeRounding.stock_means line 1741
theorem OAI.KServer.TreeRounding.tree_initialization line 1746
Source documentation
Actual balanced law at the initial fractional configuration. This is not an assumed rounding interface: it is obtained by the finite star construction.
```
theorem tree_initialization (T : Tree n) (b : Fin n → ℝ) {k : ℤ} (hk : 0 ≤ k)
    (hb : ∀ v, 0 ≤ b v) (hpb : ∀ v, 0 ≤ T.park b v) (hb0 : b 0=(k:ℝ)) :
    ∃ L : Law (Counts n), (∀ ω, T.Valid b (L.point ω) ∧ (L.point ω).subtree 0=k) ∧
      T.Means b L := by
…
```
Mentions: OAI.KServer.TreeRounding.Tree, OAI.KServer.TreeRounding.Law, OAI.KServer.TreeRounding.Counts

theorem OAI.KServer.TreeRounding.rounded_step line 1762

Source documentation

Section09's one-step top-down rounding, including the uniform constant132. The old marginal is kept exactly, and the new root and all parks are balanced.

theorem rounded_step (T : Tree n) {τ : ℝ} (hτ : 22 ≤ τ)
    (w a b : Fin n → ℝ) (hw : ∀ u, 0 ≤ w u)
    (hscale : ∀ u, u≠0 → w (T.parent u)=τ*w u) {k : ℤ} (hk : 0 ≤ k)
    (ha0 : a 0=(k:ℝ)) (hb0 : b 0=(k:ℝ))
    (ha : ∀ v, 0 ≤ a v) (hpa : ∀ v, 0 ≤ T.park a v)
    (hb : ∀ v, 0 ≤ b v) (hpb : ∀ v, 0 ≤ T.park b v)
    (L₀ : Law (Counts n)) (hvalid : ∀ ω, T.Valid a (L₀.point ω)) (hmean : T.Means a L₀) :
    ∃ L : Law (PairState n),
      (∀ f : Counts n → ℝ, L.avg (fun s => f s.old)=L₀.avg f) ∧
      (∀ ω, T.Valid a (L.point ω).old ∧ T.Valid b (L.point ω).new ∧ (L.point ω).new.subtree 0=k) ∧
      T.Means b (L.map PairState.new) ∧
      L.avg (fun s => ∑ u, w (T.parent u)*|(s.new.subtree u:ℝ)-(s.old.subtree u:ℝ)|) ≤
…

Mentions: OAI.KServer.TreeRounding.Tree, OAI.KServer.TreeRounding.Law, OAI.KServer.TreeRounding.Counts, OAI.KServer.TreeRounding.PairState

structure OAI.KServer.Rounding.Tree line 1793
abbrev OAI.KServer.Rounding.Tree.Child line 1800
instance OAI.KServer.Rounding.(instance at line 1801) line 1801
instance OAI.KServer.Rounding.(instance at line 1805) line 1805
def OAI.KServer.Rounding.Tree.park line 1807
def OAI.KServer.Rounding.Tree.childEquiv line 1810
lemma OAI.KServer.Rounding.Tree.weighted_children line 1820
def OAI.KServer.Rounding.Tree.under line 1841
Source documentation
True precisely on a vertex's descendants (including the vertex itself).
```
def Tree.under (T : Tree n) (v w : Fin n) : Bool :=
…
```
Mentions: OAI.KServer.Rounding.Tree
lemma OAI.KServer.Rounding.Tree.under_self line 1846
lemma OAI.KServer.Rounding.Tree.under_le line 1849
lemma OAI.KServer.Rounding.Tree.under_parent_self line 1862
lemma OAI.KServer.Rounding.Tree.under_zero line 1870
def OAI.KServer.Rounding.Tree.indicator line 1876
lemma OAI.KServer.Rounding.Tree.indicator_parent line 1878
theorem OAI.KServer.Rounding.Tree.park_subtree_total line 1888
Source documentation
Literal telescoping over one subtree of the concrete parent tree.
```
theorem Tree.park_subtree_total (T : Tree n) (q : Fin n → ℝ) (v : Fin n) :
    (∑ w, T.indicator v w*T.park q w)=q v := by
…
```
Mentions: OAI.KServer.Rounding.Tree
lemma OAI.KServer.Rounding.Tree.indicator_nonneg line 1915
lemma OAI.KServer.Rounding.Tree.park_nonneg line 1919
theorem OAI.KServer.Rounding.Tree.selected_park_capacity line 1925
Source documentation
The mass of any finite collection of descendant parks is bounded by its root allocation; overlapping depths do not introduce a height factor.
```
theorem Tree.selected_park_capacity (T : Tree n) (q : Fin n → ℝ) (v : Fin n)
    (hp : ∀ w, 0 ≤ T.park q w) (S : Finset (Fin n))
    (hS : ∀ w ∈ S, T.under v w=true) :
    (∑ w ∈ S, T.park q w) ≤ q v := by
…
```
Mentions: OAI.KServer.Rounding.Tree
theorem OAI.KServer.Rounding.Tree.cut_park_capacity line 1940
Source documentation
Several descendant collections may be charged simultaneously to a fixed cut. The hypotheses are explicit incidence data, not an assumed mass bound.
```
theorem Tree.cut_park_capacity (T : Tree n) (q : Fin n → ℝ)
    (hp : ∀ w, 0 ≤ T.park q w) (S F : Finset (Fin n))
    (hcover : ∀ w ∈ S, ∃ v ∈ F, T.under v w=true) :
    (∑ w ∈ S, T.park q w) ≤ ∑ v ∈ F, q v := by
…
```
Mentions: OAI.KServer.Rounding.Tree
def OAI.KServer.Rounding.countingMass line 1964
Source documentation
Finite posterior counting mass; repeated hidden locations contribute their full weight and do not require an injective posterior support.
```
def countingMass (μ : Y → ℝ) (R : Finset Y) : ℝ := ∑ y ∈ R, μ y
…
```

lemma OAI.KServer.Rounding.witness_ball_inclusion line 1968

Source documentation

A cell with a nearby validity witness lies in the source's 67r ball.

lemma witness_ball_inclusion {R : Finset Y} {y z : Y} {r : ℝ}
    (hz : z ∈ R) (hnear : dist y z ≤ 27*r)
    (hdiam : ∀ a ∈ R, ∀ b ∈ R, dist a b ≤ 40*r) :
    R ⊆ univ.filter (fun a => dist y a ≤ 67*r) := by
…

lemma OAI.KServer.Rounding.disjoint_counting_mass line 1980

theorem OAI.KServer.Rounding.Tree.geometric_park_capacity line 1996

Source documentation

Cumulative park capacity with the exact geometric radius 67. Grouping is by actual tree ancestors; posterior regions are those fixed-prefix cells. The cut F may contain unoccupied roots too, and can be the full depth-j cut.

theorem Tree.geometric_park_capacity (T : Tree n) (q : Fin n → ℝ)
    (hp : ∀ w, 0 ≤ T.park q w) (S F : Finset (Fin n))
    (hcover : ∀ w ∈ S, ∃ v ∈ F, T.under v w=true)
    (R : Fin n → Finset Y) (μ : Y → ℝ) (hμ : ∀ y, 0 ≤ μ y)
    {C r : ℝ} (hC : 0 ≤ C) (y : Y)
    (hq : ∀ v ∈ F, q v ≤ C*countingMass μ (R v))
    (hdisj : Set.PairwiseDisjoint (↑F) R)
    (hwitness : ∀ v ∈ F, ∃ z ∈ R v, dist y z ≤ 27*r)
    (hdiam : ∀ v ∈ F, ∀ a ∈ R v, ∀ b ∈ R v, dist a b ≤ 40*r) :
    (∑ w ∈ S, T.park q w) ≤
      C*countingMass μ (univ.filter (fun z => dist y z ≤ 67*r)) := by
…

Mentions: OAI.KServer.Rounding.Tree, OAI.KServer.Rounding.countingMass