Stages.lean`

42 declarations, 0 contain sorry, 0 declared as axioms

Good-arc flattening, exact predicted whitening, unconditional one-stage construction, and stage states and successors.

lemma OAI.ThreeTorus.PassagePackets.amplitude_supported line 14

theorem OAI.ThreeTorus.PassagePackets.exists_disjoint_flat line 26

Source documentation

A literal spare-independent flat pair supported in the SAME good arc, whose angular modes avoid the entire finite old family.

theorem PassagePackets.exists_disjoint_flat {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) {δ : ℝ} (hδ : 0 < δ) (hg : F.GoodArc δ) :
    ∃ l u : ℝ, δ < l ∧ l < u ∧ u < 1-δ ∧
      (∀ i, support (F.A i) ⊆ ((fun x : ℝ => (x:UnitAddCircle)) '' Icc l u) ×ˢ univ) ∧
      ∃ k : ℤ, k ≠ 0 ∧ (∀ i, F.m i ≠ k ∧ F.m i ≠ -k) ∧
      ∃ A : UnitAddCircle × UnitAddCircle → ℂ,
        Measurable A ∧ MemLp A 2 slowVolume ∧ (∀ ua, conj (A ua) = A ua) ∧
        packetSpectralMeasure (fun z => (F.periodic.lift z:UnitAddCircle)) k A =
          ENNReal.ofReal (1/2:ℝ) • phaseHaar ∧
        packetSpectralMeasure (fun z => (F.periodic.lift z:UnitAddCircle)) (-k) A =
          ENNReal.ofReal (1/2:ℝ) • phaseHaar ∧
        support A ⊆ ((fun x : ℝ => (x:UnitAddCircle)) '' Icc l u) ×ˢ univ := by
…

Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.slowVolume, OAI.ThreeTorus.packetSpectralMeasure, OAI.ThreeTorus.phaseHaar

lemma OAI.ThreeTorus.paddedReflection_involutive line 87
lemma OAI.ThreeTorus.ColoredState.laurent_finite line 97

theorem OAI.ThreeTorus.ColoredState.exists_whitening line 104

Source documentation

This theorem is unconditional once the concrete predicted smooth packet family has been produced. The flat filler uses fresh actual angular modes.

theorem exists_whitening {τR : Fin n → Fin n} (hr : C.Reflection τR)
    (hτR : Involutive τR) {δ : ℝ} (hδ : 0 < δ) (hg : C.packets.GoodArc δ) :
    ∃ W : MeasurablePackets, ∃ l u : ℝ, δ < l ∧ l < u ∧ u < 1-δ ∧
      W.Supported l u ∧ (∃ τ, W.Reflection τ) ∧
      W.spectrum (fun z => (C.packets.periodic.lift z:UnitAddCircle)) = phaseHaar ∧
      (∫ x, ‖W.vector x-C.totalVector x‖^2 ∂tripleVolume) =
        (∫ z, blockTotal C.density z ∂phaseHaar)+1-
          2*(∫ z, Real.sqrt (blockTotal C.density z) ∂phaseHaar) ∧
      ∀ (c : ℤ →₀ ℂ) (ε : ℝ), 0 < ε → ∃ d : ℤ →₀ ℂ,
        physicalError (C.laurent c) (finitePacketLaurent
          (fun z => (C.packets.periodic.lift z:UnitAddCircle)) W.m W.A d) < ε^2 := by
…

Mentions: OAI.ThreeTorus.MeasurablePackets, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.physicalError, OAI.ThreeTorus.finitePacketLaurent

lemma OAI.ThreeTorus.MeasurablePackets.laurent_memLp line 237
lemma OAI.ThreeTorus.ColoredState.density_integrable line 248
lemma OAI.ThreeTorus.ColoredState.mass_eq_norm_sq line 252

theorem OAI.ThreeTorus.exists_predicted_whitening line 259

Source documentation

The ACTUAL reflected prediction output is whitened, not replaced by an unrelated Hilbert witness. Small input density error controls the same vector.

theorem exists_predicted_whitening {n : ℕ} (C : ColoredState (Fin n))
    (ρ : Fin n → Fin n) (hρ : Involutive ρ) (hr : C.Reflection ρ)
    (b : Fin n → ℂ) (hb : ∀ i, b (ρ i)=conj (b i))
    (Q : PhysicalJetData) (frame : PhysicalFrame)
    {e r η κ ζ : ℝ} (he : 0 < e) (hr0 : 0 < r) (hr1 : r < 1)
    (her : e ≤ (r^2/64)^2) (hη : 0 < η) (hκ : 0 < κ) (hζ : 0 < ζ)
    (hpC : (∫ z, |blockTotal C.density z-1| ∂phaseHaar) < e) :
    ∃ W : MeasurablePackets, ∃ V : ℝ → ℝ, ∃ hp : Periodic V 1,
      ∃ _hs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V,
      ∃ δ l u : ℝ, ∃ β : Equiv.Perm TripleTorus, ∃ frame' : PhysicalFrame, ∃ d : ℤ →₀ ℂ,
      0 < δ ∧ δ < 1/8 ∧ δ < κ ∧ δ < l ∧ l < u ∧ u < 1-δ ∧
      (∀ x ∈ Ioo δ (1-δ), 0 < deriv V x) ∧ W.Supported l u ∧
…

Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame, OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.MeasurablePackets, OAI.ThreeTorus.TripleTorus

theorem OAI.ThreeTorus.exists_one_stage line 377

Source documentation

The unconditional one-stage producer (source05 Proposition stage). All packets, tags, two separations, actual prediction and whitening are constructed. The three tolerances are independent; finite physical jets include both signs.

theorem exists_one_stage (F : MeasurablePackets)
    {τ : F.Index → F.Index} (hr : F.Reflection τ)
    {δ l u : ℝ} (hδ : 0 ≤ δ) (hd : δ < 1/2) (hdl : δ < l) (hud : u < 1-δ)
    (hsupp : F.Supported l u)
    (V : ℝ → ℝ) (hp : Periodic V 1) (hs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) V)
    (hv : ∀ x ∈ Ioo δ (1-δ), 0 < deriv V x)
    (hflat : F.spectrum (fun z => (hp.lift z:UnitAddCircle))=phaseHaar)
    {h : TripleTorus → ℂ} (hh : Continuous h) (hrh : ∀ x, conj (h x)=h x)
    (hch : ∫ x, h x ∂tripleVolume=0) (hbh : ∀ x, ‖h x‖ ≤ 1)
    (Q : PhysicalJetData) (frame : PhysicalFrame)
    {ε η κ ζ : ℝ} (hε : 0 < ε) (hη : 0 < η) (hκ : 0 < κ) (hζ : 0 < ζ) :
    ∃ W : MeasurablePackets, ∃ V' : ℝ → ℝ, ∃ hp' : Periodic V' 1,
…

Mentions: OAI.ThreeTorus.MeasurablePackets, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.tripleVolume, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame

lemma OAI.ThreeTorus.measurePreserving_shear line 451
structure OAI.ThreeTorus.StageState line 462
Source documentation
Literal admissible states in physical coordinates. No successor or basis is part of the data; successors are produced by the unconditional stage theorem.
```
structure StageState where
…
```
def OAI.ThreeTorus.StageState.speed line 485
lemma OAI.ThreeTorus.StageState.speed_cont line 486
def OAI.ThreeTorus.StageState.chartHomeo line 489
lemma OAI.ThreeTorus.StageState.chart_symm_cont line 490
lemma OAI.ThreeTorus.StageState.chart_symm_mp line 491
def OAI.ThreeTorus.StageState.twistEquiv line 494
def OAI.ThreeTorus.StageState.mapPow line 500
def OAI.ThreeTorus.StageState.vector line 503
lemma OAI.ThreeTorus.StageState.vector_memLp line 504
abbrev OAI.ThreeTorus.StageState.L2 line 506
def OAI.ThreeTorus.StageState.vec line 507
lemma OAI.ThreeTorus.StageState.vec_ae line 508
lemma OAI.ThreeTorus.StageState.mapPow_cont line 510
lemma OAI.ThreeTorus.StageState.mapPow_mp line 516
lemma OAI.ThreeTorus.StageState.mapPow_apply line 519
lemma OAI.ThreeTorus.StageState.mapPow_add line 522
lemma OAI.ThreeTorus.StageState.mapPow_zero line 525
lemma OAI.ThreeTorus.StageState.mapPow_graph line 527
lemma OAI.ThreeTorus.StageState.vector_centered line 540
lemma OAI.ThreeTorus.StageState.vector_real line 544
def OAI.ThreeTorus.StageState.orbit line 548
lemma OAI.ThreeTorus.StageState.orbit_ae line 549
def OAI.ThreeTorus.StageState.laurent line 554
lemma OAI.ThreeTorus.StageState.laurent_ae line 555
structure OAI.ThreeTorus.PhysicalTest line 580
Source documentation
A real bounded physical test. The dense test family will be constructed explicitly; this structure only records the hypotheses of the one-stage lemma.
```
structure PhysicalTest where
…
```
lemma OAI.ThreeTorus.PhysicalTest.memLp line 587
def OAI.ThreeTorus.PhysicalTest.vec line 588
lemma OAI.ThreeTorus.PhysicalTest.vec_ae line 589
lemma OAI.ThreeTorus.physicalDist_reps line 592

theorem OAI.ThreeTorus.StageState.exists_step line 604

Source documentation

The already proved stage producer, transferred to the SAME global physical coordinates. Real tests are pulled back only to apply that producer.

theorem exists_step (s : StageState) (h : PhysicalTest) (Q : PhysicalJetData)
    {ε η κ ζ : ℝ} (hε : 0 < ε) (hη : 0 < η) (hκ : 0 < κ) (hζ : 0 < ζ) :
    ∃ t : StageState, ∃ c : ℤ →₀ ℂ,
      t.δ < κ ∧ Q.Close ζ s.frame s.V t.frame t.V ∧
      dist s.vec t.vec < ε ∧ dist h.vec (t.laurent c) < Real.sqrt (2*s.δ)+η := by
…

Mentions: OAI.ThreeTorus.StageState, OAI.ThreeTorus.PhysicalTest, OAI.ThreeTorus.PhysicalJetData