Main.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.CoordinateSweeps.moment_le_exp_of_logMoment_le line 8
lemma OAI.CoordinateSweeps.logMoment_le_of_moment_le_exp line 15
lemma OAI.CoordinateSweeps.Grid.Holes.conditionalAverage_free_cancel line 22

theorem OAI.CoordinateSweeps.Grid.Holes.conditional_sparse_main line 32

Source documentation

Entire nonautomatic sparse-dimension branch of the conditional main, with the actual stabilizer irrep, actual feasible paths and a common real z interval.

theorem conditional_sparse_main (hr : ScaleLarge r) (hrS : ScaleReady r)
    (hG : G.Allowed r) (hS : MainSizeReady SparseScalar.q G.size)
    (hf : H.Feasible) {zStar : ℝ} (hζ : SparsePerturb r zStar) {z : ℝ} (hz : z∈Set.Icc 0 zStar)
    (σ : UnitaryIrrep H.stabilizer) (hσ : σ.dimension≠1)
    (ha : ¬ (1+c G.size)*Real.log σ.dimension ≤ e G.size*h*Real.log G.size-H.cost)
    (hF : Real.log σ.dimension < (G.size:ℝ)^(1-a/4)) :
    schattenMoment SparseScalar.q (H.conditionalAverage hf z σ) ≤
      Real.exp (-c G.size*Real.log σ.dimension+e G.size*h*Real.log G.size-H.cost) := by
…

Mentions: OAI.CoordinateSweeps.ScaleLarge, OAI.CoordinateSweeps.SparseScalar.q, OAI.CoordinateSweeps.SparsePerturb, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.e, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.schattenMoment

def OAI.CoordinateSweeps.MomentBound line 100
Source documentation
Real exponential version of the exact conditional main estimate, used only as the induction predicate; its equivalence to logMoment includes zero moments.
Also declared: ComparatorChallenges/CoordinateSweeps.lean:237 (same declaration text).
```
def MomentBound (G : Grid) (q : ℕ) (z : ℝ) : Prop :=
…
```
Mentions: OAI.CoordinateSweeps.Grid
def OAI.CoordinateSweeps.cHat line 104
def OAI.CoordinateSweeps.eHat line 105
theorem OAI.CoordinateSweeps.Grid.Holes.hook_auxiliary line 110
lemma OAI.CoordinateSweeps.YoungCorner.log_factorial_lower line 191
lemma OAI.CoordinateSweeps.YoungCorner.shape_finrank_pos line 198

lemma OAI.CoordinateSweeps.YoungCorner.removed_dimension_entropy line 209

Source documentation

The translated removed diagram has the entropy required in the large-k branch, using the checked factorial/rank-count lower bound.

lemma removed_dimension_entropy (μ : YoungDiagram) (p s : ℕ)
    (hs : 0<s) (hM : Fintype.card (Boxes μ) ≤ s)
    (hfloor : (s:ℝ)^a ≤ p+1) (hL : 800 ≤ Real.log s)
    (hk : (s:ℝ)^(1-a/2) ≤ Fintype.card (Boxes (removedPart μ p))) :
    (a/4)*(Fintype.card (Boxes (removedPart μ p)):ℝ)*Real.log s ≤
      Real.log (Module.finrank ℂ (shapeSubrep (removedPart μ p) (Equiv.refl _)).toSubmodule) := by
…

Mentions: OAI.CoordinateSweeps.YoungCorner.Boxes, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.YoungCorner.removedPart, OAI.CoordinateSweeps.YoungCorner.shapeSubrep

lemma OAI.CoordinateSweeps.Grid.Holes.exists_initial_shape line 268
lemma OAI.CoordinateSweeps.Grid.Holes.augmented_boxesChart line 282
lemma OAI.CoordinateSweeps.Grid.Holes.retained_log_dimension line 288

theorem OAI.CoordinateSweeps.Grid.Holes.conditional_large_main line 311

Source documentation

Large-dimension branch of the exact main: actual retained constituent, actual augmented paths, induced placement-cycle estimate, and absorbed entropy.

theorem conditional_large_main (hr : ScaleLarge r) (hA : A.Allowed r) (hB : B.Allowed r)
    (hAB : A.b≤B.b) (hBA : B.b≤2*A.b) (hq : 1≤q)
    (hS : MainSizeReady q (concat A B).size)
    (z : ℝ) (hz : 0≤z) (hz' : z<1)
    (hlo : ∀ j g, (1/2:ℝ)*FiniteLaw.uniform _ g≤lineLaw ((concat A B).bits j) z hz hz'.le g)
    (hhi : ∀ j g, lineLaw ((concat A B).bits j) z hz hz'.le g≤2*FiniteLaw.uniform _ g)
    (hIA : MomentBound A q z) (hIB : MomentBound B q z)
    (hf : H.Feasible) (σ : UnitaryIrrep H.stabilizer)
    (hF : ((concat A B).size:ℝ)^(1-a/4)≤Real.log σ.dimension) :
    schattenMoment q (H.conditionalAverage hf z σ)≤
      Real.exp (-c (concat A B).size*Real.log σ.dimension+
        e (concat A B).size*h*Real.log (concat A B).size-H.cost) := by
…

Mentions: OAI.CoordinateSweeps.ScaleLarge, OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.size, OAI.CoordinateSweeps.FiniteLaw.uniform, OAI.CoordinateSweeps.lineLaw, OAI.CoordinateSweeps.MomentBound, OAI.CoordinateSweeps.UnitaryIrrep, OAI.CoordinateSweeps.a, OAI.CoordinateSweeps.schattenMoment, OAI.CoordinateSweeps.c, OAI.CoordinateSweeps.e

lemma OAI.CoordinateSweeps.eventually_scaleLarge line 392
lemma OAI.CoordinateSweeps.exists_main_scale line 398
theorem OAI.CoordinateSweeps.all_grid_moment line 412
Source documentation
Strong induction on the literal ordered coordinate count; every child is an actual conditioned row/column grid, not a surrogate representation law.
Distinct definitions of this name: ComparatorChallenges/CoordinateSweeps.lean:300 (same statement text; different proof or body). Qualify references as OAI.CoordinateSweeps.all_grid_moment@path.
```
theorem all_grid_moment {r : ℕ} (hr : ScaleLarge r) (hrS : SparseScalar.ScaleReady r)
    (hS : ∀ G : Grid, G.Allowed r → ScalarInduction.MainSizeReady SparseScalar.q G.size)
    {zStar : ℝ} (hζ : SparsePerturb r zStar) {z : ℝ} (hz : z∈Set.Icc 0 zStar) :
    ∀ G : Grid, G.Allowed r → MomentBound G SparseScalar.q z := by
…
```
Mentions: OAI.CoordinateSweeps.ScaleLarge, OAI.CoordinateSweeps.SparseScalar.ScaleReady, OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.ScalarInduction.MainSizeReady, OAI.CoordinateSweeps.SparseScalar.q, OAI.CoordinateSweeps.SparsePerturb, OAI.CoordinateSweeps.MomentBound
theorem OAI.CoordinateSweeps.conditional_main line 454
Source documentation
Manuscript03 thm:conditional / ac:main, with c₀=e₀=a/100, a=1/100, natural logarithms, unnormalized integer Schatten moments, all feasible disjoint paths (including none and all), and log(0)=−∞.
Distinct definitions of this name: ComparatorChallenges/CoordinateSweeps.lean:307 (same statement text; different proof or body). Qualify references as OAI.CoordinateSweeps.conditional_main@path.
```
theorem conditional_main : ConditionalMain := by
…
```
Mentions: OAI.CoordinateSweeps.ConditionalMain