Scales.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Work on the genuinely missing main statements of the pinned manuscript. All definitions are finite and use the source's ordinary probability and trace normalizations. No result of the manuscript is assumed.

lemma OAI.CoordinateSweeps.Grid.exists_concat_of_length line 20
Source comment
Any cut retains exactly the ordered bit list; no coordinate permutation is introduced into the sweep law.
```
lemma exists_concat_of_length (G : Grid) (n m : ℕ) (hn : 0 < n) (hm : 0 < m)
    (hb : G.b=n+m) : ∃ A B : Grid, A.b=n ∧ B.b=m ∧ concat A B=G := by
…
```
Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat
lemma OAI.CoordinateSweeps.Grid.exists_half_concat line 38
Source comment
Cutting the coordinate list in half is balanced because every bit count is between r and 2r. This avoids choosing a cut by logarithmic rounding.
```
lemma exists_half_concat (G : Grid) (hb : 2 ≤ G.b) :
    ∃ A B : Grid, concat A B=G ∧ A.b<G.b ∧ B.b<G.b ∧ A.b≤B.b ∧ B.b≤2*A.b := by
…
```
Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat
lemma OAI.CoordinateSweeps.Grid.balanced_logs line 51
lemma OAI.CoordinateSweeps.Grid.balanced_sizes line 75
lemma OAI.CoordinateSweeps.ScalarInduction.eventually_log_power_bound line 105
Source comment
A fixed polynomial logarithmic loss is uniformly negligible compared with any strictly larger power, the quantitative choice needed in06.
```
lemma eventually_log_power_bound (u v r C : ℝ) (huv : u < v) (hC : 0 < C) :
    ∀ᶠ s : ℝ in atTop, 0 < s ∧ s^u*(Real.log s)^r ≤ C*s^v := by
…
```
lemma OAI.CoordinateSweeps.ScalarInduction.eventually_constant_le_power line 119
lemma OAI.CoordinateSweeps.ScalarInduction.eventually_absorb_hook line 123
lemma OAI.CoordinateSweeps.ScalarInduction.eventually_absorb_removed line 148

theorem OAI.CoordinateSweeps.ScalarInduction.removed_endgame line 175

Source comment

Scalar endgame after the *actual* induced placement-cycle estimate. All representation/path data enter only through their already derived entropies, multiplicity and cost inequalities.

theorem removed_endgame (L F Fg Fd k h b C : ℝ) (_ : ℝ) (err : ℝ)
    (hL : 0 < L) (_ : 0 ≤ F) (hh : 0 ≤ h) (_ : 0 ≤ k)
    (hD : F ≤ Fg+k*L) (hroot : 0 < Real.sqrt L)
    (hcost : (c0+e0)*k*L+Real.log 4*k*b-Fd+err ≤ F/(20*Real.sqrt L)) :
    -(c0+1/Real.sqrt L+1/(20*Real.sqrt L))*Fg+
      (e0-1/Real.sqrt L-1/(20*Real.sqrt L))*(h+k)*L+err-C+Real.log 4*k*b-Fd ≤
      -(c0+1/Real.sqrt L)*F+(e0-1/Real.sqrt L)*h*L-C := by
…

Mentions: OAI.CoordinateSweeps.c0, OAI.CoordinateSweeps.e0

lemma OAI.CoordinateSweeps.ScalarInduction.reciprocal_sqrt_gap line 192
Source comment
Child coefficient improvement from a balanced nontrivial split.
```
lemma reciprocal_sqrt_gap {L t : ℝ} (hL : 0 < L) (ht : 0 < t) (htL : t ≤ (4/5)*L) :
    (11/10 : ℝ)/Real.sqrt L ≤ 1/Real.sqrt t := by
…
```
lemma OAI.CoordinateSweeps.ScalarInduction.hook_comparison line 201
lemma OAI.CoordinateSweeps.ScalarInduction.hook_error_bound line 220
structure OAI.CoordinateSweeps.ScalarInduction.MainSizeReady line 244
Also declared: ComparatorChallenges/CoordinateSweeps.lean:250 (same declaration text).
lemma OAI.CoordinateSweeps.ScalarInduction.eventually_mainSizeReady line 249
lemma OAI.CoordinateSweeps.ScalarInduction.improved_coefficients line 258
lemma OAI.CoordinateSweeps.ScalarInduction.hook_strengthening line 263
lemma OAI.CoordinateSweeps.ScalarInduction.removed_cost_bound line 288