WeightRounding.lean`

72 declarations, 0 contain sorry, 0 declared as axioms

Largest-remainder rounding for the occurrence game

The input is an indexed list of nonnegative rational weights, represented exactly by natural numerators with a common positive denominator. The order uses decreasing fractional remainders, with the original occurrence index as a deterministic tie-break. No constraint, endpoint or occurrence identity is changed by rounding.

def OAI.MaxCutGames.Reduction.WeightRounding.floorMass line 8

def OAI.MaxCutGames.Reduction.WeightRounding.roundCounts line 12

Source documentation

Increment the first r floors, in the original occurrence order.

def roundCounts (D q : Nat) : Nat → List Nat → List Nat
  | _, [] => []
  | 0, p :: ps => (D * p / q) :: roundCounts D q 0 ps
  | r + 1, p :: ps => (D * p / q + 1) :: roundCounts D q r ps

def OAI.MaxCutGames.Reduction.WeightRounding.deficit line 17
def OAI.MaxCutGames.Reduction.WeightRounding.rounded line 19
theorem OAI.MaxCutGames.Reduction.WeightRounding.length_roundCounts line 22
theorem OAI.MaxCutGames.Reduction.WeightRounding.sum_roundCounts line 28
theorem OAI.MaxCutGames.Reduction.WeightRounding.floorMass_mul_le line 44
theorem OAI.MaxCutGames.Reduction.WeightRounding.scaled_sum_lt line 54
theorem OAI.MaxCutGames.Reduction.WeightRounding.floorMass_le_target line 70
theorem OAI.MaxCutGames.Reduction.WeightRounding.deficit_lt_length line 75
theorem OAI.MaxCutGames.Reduction.WeightRounding.sum_rounded line 86
Source documentation
Equation (4.7), total mass: the output has exactly the chosen denominator.
```
theorem sum_rounded (D q : Nat) (ps : List Nat) (hq : 0 < q)
    (hmass : ps.sum = q) : (rounded D q ps).sum = D := by
…
```
Mentions: OAI.MaxCutGames.Reduction.WeightRounding.rounded

def OAI.MaxCutGames.Reduction.WeightRounding.selectedSum line 95

Source documentation

Sum only the positions selected by an arbitrary predicate.

def selectedSum : List Nat → (Nat → Bool) → Nat
  | [], _ => 0
  | p :: ps, keep => (if keep 0 then p else 0) +
      selectedSum ps (fun i => keep (i + 1))

/-- The two inequalities encode `|nᵢ − D pᵢ/q| ≤ 1`. -/

theorem OAI.MaxCutGames.Reduction.WeightRounding.floor_entry_bounds line 101
Source documentation
The two inequalities encode |nᵢ − D pᵢ/q| ≤ 1.
```
theorem floor_entry_bounds (D q p : Nat) (hq : 0 < q) (b : Bool) :
    let n := D * p / q + if b then 1 else 0
…
```
theorem OAI.MaxCutGames.Reduction.WeightRounding.selected_roundCounts_error line 112
Source documentation
Equation (4.8) for every selection of occurrences, before dividing by Dq. The selection can be the equations satisfied by any particular assignment.
```
theorem selected_roundCounts_error (D q r : Nat) (ps : List Nat)
    (keep : Nat → Bool) (hq : 0 < q) :
    selectedSum (roundCounts D q r ps) keep * q ≤
        D * selectedSum ps keep + ps.length * q ∧
    D * selectedSum ps keep ≤
        selectedSum (roundCounts D q r ps) keep * q + ps.length * q := by
…
```
Mentions: OAI.MaxCutGames.Reduction.WeightRounding.selectedSum, OAI.MaxCutGames.Reduction.WeightRounding.roundCounts
theorem OAI.MaxCutGames.Reduction.WeightRounding.selected_rounded_error line 137
def OAI.MaxCutGames.Reduction.WeightRounding.replicateOccurrences line 145
theorem OAI.MaxCutGames.Reduction.WeightRounding.length_replicateOccurrences line 149
def OAI.MaxCutGames.Reduction.WeightRounding.copyIndices line 158
Source documentation
Output occurrence indices; each integer count gives that many separate copies.
```
def copyIndices : List Nat → List Nat
  | [] => []
  | n :: ns => List.replicate n 0 ++ (copyIndices ns).map Nat.succ
```
theorem OAI.MaxCutGames.Reduction.WeightRounding.length_copyIndices line 162
theorem OAI.MaxCutGames.Reduction.WeightRounding.mem_copyIndices_lt line 167
theorem OAI.MaxCutGames.Reduction.WeightRounding.count_copyIndices line 183
Source documentation
Copying occurrences preserves the satisfaction test for every assignment.
```
theorem count_copyIndices (ns : List Nat) (keep : Nat → Bool) :
    ((copyIndices ns).filter keep).length = selectedSum ns keep := by
…
```
Mentions: OAI.MaxCutGames.Reduction.WeightRounding.copyIndices, OAI.MaxCutGames.Reduction.WeightRounding.selectedSum
def OAI.MaxCutGames.Reduction.WeightRounding.uniformSource line 192
theorem OAI.MaxCutGames.Reduction.WeightRounding.uniformSource_indices_lt line 194
theorem OAI.MaxCutGames.Reduction.WeightRounding.length_uniformSource line 199
theorem OAI.MaxCutGames.Reduction.WeightRounding.uniformSource_nonempty line 203

theorem OAI.MaxCutGames.Reduction.WeightRounding.uniformSource_error line 212

Source documentation

Full occurrence-list form of (4.8), quantified over all satisfaction tests.

theorem uniformSource_error (D q : Nat) (ps : List Nat)
    (keep : Nat → Bool) (hq : 0 < q) :
    ((uniformSource D q ps).filter keep).length * q ≤
        D * selectedSum ps keep + ps.length * q ∧
    D * selectedSum ps keep ≤
        ((uniformSource D q ps).filter keep).length * q + ps.length * q := by
…

Mentions: OAI.MaxCutGames.Reduction.WeightRounding.uniformSource, OAI.MaxCutGames.Reduction.WeightRounding.selectedSum

def OAI.MaxCutGames.Reduction.WeightRounding.ceilQuotient line 221
Source documentation
Integer ceiling; valid for positive a.
```
def ceilQuotient (n a : Nat) : Nat := (n + a - 1) / a
```
theorem OAI.MaxCutGames.Reduction.WeightRounding.le_ceilQuotient_mul line 223
theorem OAI.MaxCutGames.Reduction.WeightRounding.ceilQuotient_le line 231
def OAI.MaxCutGames.Reduction.WeightRounding.targetDenominator line 238
theorem OAI.MaxCutGames.Reduction.WeightRounding.targetDenominator_error_budget line 241
Source documentation
Cross-multiplied statement m / D ≤ γ₀ / 4.
```
theorem targetDenominator_error_budget (m a b : Nat) (ha : 0 < a) :
    4 * m * b ≤ targetDenominator m a b * a :=
…
```
Mentions: OAI.MaxCutGames.Reduction.WeightRounding.targetDenominator
theorem OAI.MaxCutGames.Reduction.WeightRounding.targetDenominator_size line 247
Source documentation
At fixed rational γ₀, the number of output occurrences is linear in m. This is an output-size bound, not a machine-model complexity theorem.
```
theorem targetDenominator_size (m a b : Nat) (ha : 0 < a) :
    targetDenominator m a b ≤ 4 * b * m := by
…
```
Mentions: OAI.MaxCutGames.Reduction.WeightRounding.targetDenominator
theorem OAI.MaxCutGames.Reduction.WeightRounding.targetDenominator_positive line 252
abbrev OAI.MaxCutGames.Explicit.Rounding.IntegerRounding line 278
def OAI.MaxCutGames.Explicit.Rounding.denominator line 281
Source documentation
Exact integer implementation of ceil(h / (a/b)).
```
def denominator (h a b : Nat) : Nat := IntegerRounding (h * b) a
```
Mentions: OAI.MaxCutGames.Explicit.Rounding.IntegerRounding
theorem OAI.MaxCutGames.Explicit.Rounding.denominator_budget line 283
theorem OAI.MaxCutGames.Explicit.Rounding.denominator_size line 287
theorem OAI.MaxCutGames.Explicit.Rounding.denominator_positive line 292
def OAI.MaxCutGames.Explicit.Rounding.remainder line 305
Source documentation
The fractional part of Q * (p i / q), with denominator q.
```
def remainder (Q q : Nat) (p : Fin h → Nat) (i : Fin h) : Nat :=
…
```
def OAI.MaxCutGames.Explicit.Rounding.priority line 308
instance OAI.MaxCutGames.Explicit.Rounding.priorityDecidable line 312
instance OAI.MaxCutGames.Explicit.Rounding.priorityTrans line 316
instance OAI.MaxCutGames.Explicit.Rounding.priorityAntisymm line 323
instance OAI.MaxCutGames.Explicit.Rounding.priorityTotal line 331
def OAI.MaxCutGames.Explicit.Rounding.remainderOrder line 339
Source documentation
Executable merge-sort of occurrence indices, rather than their records.
```
def remainderOrder (Q q : Nat) (p : Fin h → Nat) : List (Fin h) :=
…
```
theorem OAI.MaxCutGames.Explicit.Rounding.remainderOrder_sorted line 342
theorem OAI.MaxCutGames.Explicit.Rounding.remainderOrder_length line 346
theorem OAI.MaxCutGames.Explicit.Rounding.remainderOrder_nodup line 350
def OAI.MaxCutGames.Explicit.Rounding.floorCount line 353
def OAI.MaxCutGames.Explicit.Rounding.deficit line 356
theorem OAI.MaxCutGames.Explicit.Rounding.floor_sum_le line 359
theorem OAI.MaxCutGames.Explicit.Rounding.deficit_lt line 366
def OAI.MaxCutGames.Explicit.Rounding.incremented line 375
Source documentation
Precisely the first deficit indices in decreasing remainder order.
```
def incremented (Q q : Nat) (p : Fin h → Nat) : Finset (Fin h) :=
…
```
def OAI.MaxCutGames.Explicit.Rounding.count line 378
theorem OAI.MaxCutGames.Explicit.Rounding.incremented_card line 381
theorem OAI.MaxCutGames.Explicit.Rounding.sum_count line 388
Source documentation
Largest-remainder rounding preserves total mass exactly.
```
theorem sum_count (Q q : Nat) (p : Fin h → Nat) (hq : 0 < q)
    (hmass : ∑ i, p i = q) : ∑ i, count Q q p i = Q := by
…
```
Mentions: OAI.MaxCutGames.Explicit.Rounding.count
theorem OAI.MaxCutGames.Explicit.Rounding.count_error line 398
Source documentation
Cross-multiplied pointwise error, independent of the rounding order.
```
theorem count_error (Q q : Nat) (p : Fin h → Nat) (hq : 0 < q) (i : Fin h) :
    count Q q p i * q ≤ Q * p i + q ∧
      Q * p i ≤ count Q q p i * q + q := by
…
```
Mentions: OAI.MaxCutGames.Explicit.Rounding.count
theorem OAI.MaxCutGames.Explicit.Rounding.incremented_priority line 409
Source documentation
Every incremented entry precedes every entry that is not incremented. This records the largest-remainder requirement, including deterministic ties.
```
theorem incremented_priority (Q q : Nat) (p : Fin h → Nat) (i j : Fin h)
    (hi : i ∈ incremented Q q p) (hj : j ∉ incremented Q q p) :
    priority Q q p i j := by
…
```
Mentions: OAI.MaxCutGames.Explicit.Rounding.incremented, OAI.MaxCutGames.Explicit.Rounding.priority

theorem OAI.MaxCutGames.Explicit.Rounding.selected_count_error line 427

Source documentation

Error on any selected set of occurrences, before division.

theorem selected_count_error (Q q : Nat) (p : Fin h → Nat) (hq : 0 < q)
    (s : Finset (Fin h)) :
    (∑ i ∈ s, count Q q p i) * q ≤ Q * (∑ i ∈ s, p i) + s.card * q ∧
    Q * (∑ i ∈ s, p i) ≤ (∑ i ∈ s, count Q q p i) * q + s.card * q := by
…

Mentions: OAI.MaxCutGames.Explicit.Rounding.count

theorem OAI.MaxCutGames.Explicit.Rounding.ratio_error line 438

Source documentation

Convert the integer error certificate to its normalized rational form.

theorem ratio_error (n p m Q q : Nat) (hQ : 0 < Q) (hq : 0 < q)
    (hu : n * q ≤ Q * p + m * q) (hl : Q * p ≤ n * q + m * q) :
    |(n : ℚ) / Q - (p : ℚ) / q| ≤ (m : ℚ) / Q := by
…

theorem OAI.MaxCutGames.Explicit.Rounding.count_ratio_error line 452
theorem OAI.MaxCutGames.Explicit.Rounding.selected_ratio_error line 459
theorem OAI.MaxCutGames.Explicit.Rounding.denominator_ratio_budget line 470
theorem OAI.MaxCutGames.Explicit.Rounding.denominator_eq_ceil line 482
Source documentation
The algorithm's natural-number division is exactly the claimed ceiling.
```
theorem denominator_eq_ceil (h a b : Nat) (ha : 0 < a) (hb : 0 < b) :
    denominator h a b = Nat.ceil ((h : ℚ) / ((a : ℚ) / b)) := by
…
```
Mentions: OAI.MaxCutGames.Explicit.Rounding.denominator

theorem OAI.MaxCutGames.Explicit.Rounding.selected_tolerance line 502

Source documentation

Every satisfied-occurrence set has error at most the prescribed tolerance.

theorem selected_tolerance (a b q : Nat) (p : Fin h → Nat)
    (hh : 0 < h) (ha : 0 < a) (hb : 0 < b) (hq : 0 < q)
    (s : Finset (Fin h)) :
    |((∑ i ∈ s, count (denominator h a b) q p i : Nat) : ℚ) /
          denominator h a b - ((∑ i ∈ s, p i : Nat) : ℚ) / q| ≤
      (a : ℚ) / b :=
…

Mentions: OAI.MaxCutGames.Explicit.Rounding.count, OAI.MaxCutGames.Explicit.Rounding.denominator

theorem OAI.MaxCutGames.Explicit.Rounding.selected_weight_error line 512

Source documentation

Satisfaction-predicate form, with individually normalized rational weights.

theorem selected_weight_error (Q q : Nat) (p : Fin h → Nat)
    (hQ : 0 < Q) (hq : 0 < q) (keep : Fin h → Bool) :
    |(∑ i, if keep i then (count Q q p i : ℚ) / Q else 0) -
      (∑ i, if keep i then (p i : ℚ) / q else 0)| ≤ (h : ℚ) / Q := by
…

Mentions: OAI.MaxCutGames.Explicit.Rounding.count

theorem OAI.MaxCutGames.Explicit.Rounding.selected_weight_tolerance line 519
def OAI.MaxCutGames.Explicit.Rounding.copies line 528
theorem OAI.MaxCutGames.Explicit.Rounding.copies_length line 531
theorem OAI.MaxCutGames.Explicit.Rounding.copies_nonempty line 535
theorem OAI.MaxCutGames.Explicit.Rounding.copies_filter_length line 543
theorem OAI.MaxCutGames.Explicit.Rounding.count_le line 550
Source documentation
An individual multiplicity is bounded by the chosen output size.
```
theorem count_le (Q q : Nat) (p : Fin h → Nat) (hq : 0 < q)
    (hmass : ∑ i, p i = q) (i : Fin h) : count Q q p i ≤ Q := by
…
```
Mentions: OAI.MaxCutGames.Explicit.Rounding.count