BaseCase.lean`

55 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.UnitaryIrrep.orbit_span_top line 22
theorem OAI.CoordinateSweeps.UnitaryIrrep.dimension_le_card line 44
Source comment
Elementary irreducible dimension bound needed for the finite base case; no partition classification has been assumed.
```
theorem dimension_le_card [Fintype Γ] : ρ.dimension ≤ Fintype.card Γ := by
…
```
def OAI.CoordinateSweeps.UnitaryIrrep.fixed line 50
lemma OAI.CoordinateSweeps.UnitaryIrrep.fixed_eq_bot_or_trivial line 56
theorem OAI.CoordinateSweeps.UnitaryIrrep.uniform_average_eq_zero line 74
Source comment
The exact zero of a uniform group average in every nontrivial irreducible. This is the strict moment bound at z=0 used in06's b=1 base case.
```
theorem uniform_average_eq_zero [Fintype Γ]
    (hρ : ¬ ∀ g, ρ.matrix g=1) :
    (∑ g, (FiniteLaw.uniform Γ g : ℂ) • ρ.matrix g) = 0 := by
…
```
Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform
lemma OAI.CoordinateSweeps.UnitaryIrrep.sum_matrix_eq_zero line 95
theorem OAI.CoordinateSweeps.UnitaryIrrep.affine_average_norm_le line 105
Source comment
Uniform-in-the-irrep quantitative form of the finite one-block base perturbation in06. A conditional coset has precisely these affine weights, with u=1/m! and 0≤w≤1. No classification, finiteness of a chosen list of representations, or continuity assumption is needed.
```
theorem affine_average_norm_le (hρ : ¬ ∀ g, ρ.matrix g=1)
    (u : ℝ) (hu : 0 < u) (w : Γ → ℝ)
    (hw : ∀ g, 0 ≤ w g) (hw1 : ∀ g, w g ≤ 1)
    {z : ℝ} (hz : 0 ≤ z) (hz1 : z ≤ 1/2) :
    ‖((∑ g, ((1-z)*u+z*w g) : ℝ) : ℂ)⁻¹ •
       ∑ g, (((1-z)*u+z*w g : ℝ) : ℂ) • ρ.matrix g‖ ≤ 2*z/u := by
…
```
abbrev OAI.CoordinateSweeps.Grid.single line 156
Source comment
A one-coordinate grid, the base of06's induction.
```
abbrev single (d : ℕ) : Grid := ⟨1,by decide,fun _ => d⟩
```
Mentions: OAI.CoordinateSweeps.Grid
instance OAI.CoordinateSweeps.Grid.single_line_unique line 158
def OAI.CoordinateSweeps.Grid.singleSlot line 165
Source comment
The single coordinate slot identification is explicit.
```
def singleSlot (d : ℕ) : (single d).Slot ≃ Cube d :=
…
```
Mentions: OAI.CoordinateSweeps.Grid.single, OAI.CoordinateSweeps.Grid.Slot, OAI.CoordinateSweeps.Cube
theorem OAI.CoordinateSweeps.Grid.singleSlot_apply line 168
theorem OAI.CoordinateSweeps.Grid.singleSlot_symm_apply line 171
def OAI.CoordinateSweeps.Grid.singleChoice line 175
Source comment
Every line-choice array in a one-coordinate grid is one permutation.
```
def singleChoice (d : ℕ) : (single d).Choices ≃ Equiv.Perm (Cube d) where
…
```
Mentions: OAI.CoordinateSweeps.Grid.single, OAI.CoordinateSweeps.Grid.Choices, OAI.CoordinateSweeps.Cube
lemma OAI.CoordinateSweeps.Grid.single_stage_apply line 185
lemma OAI.CoordinateSweeps.Grid.single_sweep line 193
def OAI.CoordinateSweeps.Grid.singleSweepEquiv line 207
Source comment
No hidden fibers in the one-block base: all permutations are possible, and each one determines the unique line-choice array.
```
def singleSweepEquiv (d : ℕ) : (single d).Choices ≃ Equiv.Perm (single d).Slot :=
…
```
Mentions: OAI.CoordinateSweeps.Grid.single, OAI.CoordinateSweeps.Grid.Choices, OAI.CoordinateSweeps.Grid.Slot
lemma OAI.CoordinateSweeps.Grid.singleSweepEquiv_apply line 210
lemma OAI.CoordinateSweeps.Grid.single_choiceWeight line 213
lemma OAI.CoordinateSweeps.Grid.Holes.single_compatible_iff line 227
def OAI.CoordinateSweeps.Grid.Holes.singleResidualEquiv line 239
Source comment
Exact bijection of conditioned one-block choices with the remaining symmetric group, not an assumption of uniformity of that residual law.
```
def singleResidualEquiv (hf : H.Feasible) :
    {ω : (Grid.single d).Choices // H.Compatible ω} ≃ H.stabilizer where
…
```
Mentions: OAI.CoordinateSweeps.Grid.single, OAI.CoordinateSweeps.Grid.Choices
lemma OAI.CoordinateSweeps.Grid.Holes.single_probability line 264
lemma OAI.CoordinateSweeps.Grid.Holes.single_conditionalAverage line 269
theorem OAI.CoordinateSweeps.Grid.Holes.single_conditional_norm_le line 292
Source comment
Actual conditioned single-coordinate operator, uniform in the hole family, reference bijection, irrep, and representation realization.
```
theorem single_conditional_norm_le (hf : H.Feasible)
    (ρ : UnitaryIrrep H.stabilizer) (hρ : ¬ ∀ g, ρ.matrix g=1)
    {z : ℝ} (hz : 0 ≤ z) (hz1 : z ≤ 1/2) :
    ‖H.conditionalAverage hf z ρ‖ ≤
      2*z*(Fintype.card (Equiv.Perm (Cube d)) : ℝ) := by
…
```
Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.Cube
lemma OAI.CoordinateSweeps.Grid.Holes.single_dimension_le line 306

theorem OAI.CoordinateSweeps.Grid.Holes.single_conditional_moment_le line 314

Source comment

Exact one-block moment bound before choosing the absolute real interval.

theorem single_conditional_moment_le (hf : H.Feasible)
    (ρ : UnitaryIrrep H.stabilizer) (hρ : ¬ ∀ g, ρ.matrix g=1)
    {z : ℝ} (hz : 0 ≤ z) (hz1 : z ≤ 1/2) (q : ℕ) :
    schattenMoment q (H.conditionalAverage hf z ρ) ≤
      (Fintype.card (Equiv.Perm (Cube d)) : ℝ) *
        (2*z*(Fintype.card (Equiv.Perm (Cube d)) : ℝ))^(2*q) := by
…

Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.schattenMoment, OAI.CoordinateSweeps.Cube

lemma OAI.CoordinateSweeps.e0_pos line 330
lemma OAI.CoordinateSweeps.c0_eq_e0 line 331
lemma OAI.CoordinateSweeps.c0_small line 332
lemma OAI.CoordinateSweeps.Grid.log_size_lower_one line 336
def OAI.CoordinateSweeps.ScaleLarge line 346
Source comment
Exactly the two largeness requirements stated at the start of06, converted from log R to bit exponent r. Both constants remain the source constants.
Also declared: ComparatorChallenges/CoordinateSweeps.lean:242 (same declaration text).
```
def ScaleLarge (r : ℕ) : Prop :=
…
```
lemma OAI.CoordinateSweeps.exists_scaleLarge line 349
lemma OAI.CoordinateSweeps.scale_coefficients line 362
theorem OAI.CoordinateSweeps.Grid.Holes.allowance_lower line 392
Source comment
Exact source nonnegative allowance, including h=0 and the empty type.
```
theorem allowance_lower {r : ℕ} (hr : ScaleLarge r) (hG : G.Allowed r) :
    (e0/4) * h * Real.log G.size ≤ e G.size * h * Real.log G.size - H.cost := by
…
```
Mentions: OAI.CoordinateSweeps.ScaleLarge, OAI.CoordinateSweeps.e0, OAI.CoordinateSweeps.e
lemma OAI.CoordinateSweeps.Grid.Holes.allowance_nonneg line 399
lemma OAI.CoordinateSweeps.logMoment_le_of_le line 406

theorem OAI.CoordinateSweeps.Grid.Holes.conditional_automatic line 417

Source comment

Entire automatic branch06 eq16, with no representation type omitted.

theorem conditional_automatic (hf : H.Feasible) {z : ℝ} (hz : 0 ≤ z) (hz1 : z < 1)
    (ρ : UnitaryIrrep H.stabilizer) (q : ℕ)
    (ha : (1+c G.size)*Real.log ρ.dimension ≤
      e G.size*h*Real.log G.size-H.cost) :
    logMoment (schattenMoment q (H.conditionalAverage hf z ρ)) ≤
      ((-c G.size*Real.log ρ.dimension+e G.size*h*Real.log G.size-H.cost : ℝ) : EReal) := by
…

Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.logMoment, OAI.CoordinateSweeps.schattenMoment

theorem OAI.CoordinateSweeps.Grid.Holes.conditional_dimension_one line 430
Source comment
All one-dimensional types (trivial, sign, empty, and M=1), as required explicitly in the statement and the first branch of the main induction.
```
theorem conditional_dimension_one {r : ℕ} (hr : ScaleLarge r) (hG : G.Allowed r)
    (hf : H.Feasible) {z : ℝ} (hz : 0 ≤ z) (hz1 : z < 1)
    (ρ : UnitaryIrrep H.stabilizer) (hρ : ρ.dimension=1) (q : ℕ) :
    logMoment (schattenMoment q (H.conditionalAverage hf z ρ)) ≤
      ((-c G.size*Real.log ρ.dimension+e G.size*h*Real.log G.size-H.cost : ℝ) : EReal) := by
…
```
Mentions: OAI.CoordinateSweeps.ScaleLarge, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.logMoment, OAI.CoordinateSweeps.schattenMoment, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.e
lemma OAI.CoordinateSweeps.UnitaryIrrep.dimension_one_of_trivial line 445
def OAI.CoordinateSweeps.baseWidth line 458
Source comment
An explicit uniform base interval, so06's finiteness perturbation requires no choice of a finite list of representation realizations.
Also declared: ComparatorChallenges/CoordinateSweeps.lean:245 (same declaration text).
```
def baseWidth (r : ℕ) : ℝ := ((2^(2*r)).factorial : ℕ)
```
def OAI.CoordinateSweeps.baseZeta line 459
Also declared: ComparatorChallenges/CoordinateSweeps.lean:246 (same declaration text).
lemma OAI.CoordinateSweeps.baseWidth_one_le line 461
lemma OAI.CoordinateSweeps.baseZeta_pos line 465
lemma OAI.CoordinateSweeps.baseZeta_le_half line 470
lemma OAI.CoordinateSweeps.single_card_le_baseWidth line 476
theorem OAI.CoordinateSweeps.Grid.Holes.single_base_norm line 485

theorem OAI.CoordinateSweeps.Grid.Holes.single_base_moment line 505

Source comment

A quantitative strict base estimate for all nontrivial irreducibles.

theorem single_base_moment {r : ℕ} (hd : d ≤ 2*r) (hf : H.Feasible)
    (ρ : UnitaryIrrep H.stabilizer) (hρ : ρ.dimension ≠ 1)
    {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ baseZeta r)
    {q : ℕ} (hq : 1 ≤ q) :
    schattenMoment q (H.conditionalAverage hf z ρ) ≤ (ρ.dimension : ℝ)⁻¹ := by
…

Mentions: OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.baseZeta, OAI.CoordinateSweeps.schattenMoment

theorem OAI.CoordinateSweeps.Grid.Holes.single_conditional_main line 529
Source comment
The full06 one-coordinate base with the manuscript's precise c,e and cost.
```
theorem single_conditional_main {r : ℕ} (hr : ScaleLarge r)
    (hG : (Grid.single d).Allowed r) (hf : H.Feasible)
    {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ baseZeta r)
    (ρ : UnitaryIrrep H.stabilizer) {q : ℕ} (hq : 1 ≤ q) :
    logMoment (schattenMoment q (H.conditionalAverage hf z ρ)) ≤
      ((-c (Grid.single d).size*Real.log ρ.dimension+
        e (Grid.single d).size*h*Real.log (Grid.single d).size-H.cost : ℝ) : EReal) := by
…
```
Mentions: OAI.CoordinateSweeps.ScaleLarge, OAI.CoordinateSweeps.Grid.single, OAI.CoordinateSweeps.Grid.Allowed, OAI.CoordinateSweeps.baseZeta, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.logMoment, OAI.CoordinateSweeps.schattenMoment, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.Grid.size, OAI.CoordinateSweeps.e
lemma OAI.CoordinateSweeps.Grid.eq_single_of_b_one line 557

theorem OAI.CoordinateSweeps.Grid.conditional_main_b_one line 568

Source comment

Full base branch for every allowed one-coordinate grid, not only a chosen canonical coordinate presentation.

theorem conditional_main_b_one {r : ℕ} (hr : ScaleLarge r)
    (G : Grid) (hb : G.b=1) (hG : G.Allowed r)
    {h : ℕ} (H : G.Holes h) (hf : H.Feasible)
    {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ baseZeta r)
    (ρ : UnitaryIrrep H.stabilizer) {q : ℕ} (hq : 1 ≤ q) :
    logMoment (schattenMoment q (H.conditionalAverage hf z ρ)) ≤
      ((-c G.size*Real.log ρ.dimension+e G.size*h*Real.log G.size-H.cost : ℝ) : EReal) := by
…

Mentions: OAI.CoordinateSweeps.ScaleLarge, OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.baseZeta, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.logMoment, OAI.CoordinateSweeps.schattenMoment, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.e

def OAI.CoordinateSweeps.Grid.Holes.initialJunctionFree line 585
Source comment
The unswept free sites and the literal occupied junction board are identified by the actual reference first-half sweep.
```
noncomputable def initialJunctionFree (hf : H.Feasible) : H.FreeAt 0 ≃ H.JunctionFree :=
…
```
lemma OAI.CoordinateSweeps.Grid.Holes.initialJunction_conj line 588
lemma OAI.CoordinateSweeps.Grid.Holes.junctionChart_symm_boxes line 595
lemma OAI.CoordinateSweeps.Grid.Holes.junction_hasShape line 613
lemma OAI.CoordinateSweeps.Grid.Holes.conditionalAverage_cancelChart line 631

theorem OAI.CoordinateSweeps.Grid.Holes.actual_hook_bound line 643

Source comment

Exact hooked-main estimate for the actual stabilizer representation and its literal initial-site Young labeling, with arbitrary feasible holes.

theorem actual_hook_bound (p : ℕ) (hp : 0<p) (hf : H.Feasible)
    (z : ℝ) (q : ℕ) (hq : 0<q) (c e : ℝ) (hc : 0≤c) (hcq : c≤q)
    (s : ℕ) (hpS : p≤ s) (hAS : A.size≤ s) (hBS : B.size≤ s)
    (σ : UnitaryIrrep H.stabilizer)
    (hR : ∀ y : B.Slot, ∀ τ : UnitaryIrrep (H.rowHoles y).stabilizer,
      schattenMoment q ((H.rowHoles y).conditionalAverage (H.rowHoles y).feasible_of_disjoint z τ) ≤
        Real.exp (-c*Real.log τ.dimension+e*H.rowCount y*Real.log A.size-(H.rowHoles y).cost))
    (hC : ∀ x : A.Slot, ∀ τ : UnitaryIrrep (H.columnHoles x).stabilizer,
      schattenMoment q ((H.columnHoles x).conditionalAverage (H.columnHoles x).feasible_of_disjoint z τ) ≤
        Real.exp (-c*Real.log τ.dimension+e*H.columnCount x*Real.log B.size-(H.columnHoles x).cost))
    (μ : YoungDiagram) (eB : H.FreeAt 0 ≃ Boxes μ)
    (hσ : hasShape μ (Equiv.refl _) (σ.pullback (H.boxesChart μ eB)).asRepresentation) (hhook : Hook μ p) :
…

Mentions: OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.Grid.Holes.stabilizer, OAI.CoordinateSweeps.schattenMoment, OAI.CoordinateSweeps.Grid.Holes.conditionalAverage, OAI.CoordinateSweeps.Grid.Holes.feasible_of_disjoint, OAI.CoordinateSweeps.Grid.Holes.cost