FiniteBlocks.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

Symmetric anchored blocks, unconditional block production, physical mass, and estimator regularity.

def OAI.ThreeTorus.ColoredSignalReflectedRealizes line 19

theorem OAI.ThreeTorus.exists_concrete_colored_reflected_signal line 34

Source documentation

The interface is discharged by the actual geometric construction.

theorem exists_concrete_colored_reflected_signal {b D : ℝ} (hb : 0 < b) (hbD : b < D)
    {d : ℝ → ℂ} (hd : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d)
    (hdc : HasCompactSupport d) (hdr : ∀ v, d (-v) = starRingEnd ℂ (d v))
    (hd0 : d 0 = 0) (hds : support d ⊆ Icc (-D) D) :
    ∃ L : ℕ, ∃ γ₀ : ℝ, 2 ≤ L ∧ D/b < L ∧ 0 < γ₀ ∧
      ∀ γ : ℝ, 0 < γ → γ ≤ γ₀ →
      (∀ v, 2*γ*‖d v‖ ≤ 1/2) ∧
      ColoredSignalReflectedRealizes b D d γ (refreshedStrength (signalPrimeProduct L) γ) :=
…

Mentions: OAI.ThreeTorus.ColoredSignalReflectedRealizes, OAI.ThreeTorus.refreshedStrength, OAI.ThreeTorus.signalPrimeProduct

theorem OAI.ThreeTorus.ColoredSignalReflectedRealizes.iterate line 48

Source documentation

Fixed data and a small coefficient tolerance first; the threshold tree is chosen on the actual initial state; ALL diagonals above that tree are realized with small product-model and physical errors. No independence of the diagonal, modeled next state, or unproved packet producer is used.

theorem ColoredSignalReflectedRealizes.iterate {b D γ ell : ℝ} {d : ℝ → ℂ}
    (hsignal : ColoredSignalReflectedRealizes b D d γ ell)
    (hd : Continuous d) (hdc : HasCompactSupport d) (hγ : 0 < γ)
    (hell : 0 ≤ ell) (hells : 6*ell ≤ 1)
    (m n : ℕ) (τR : Fin m → Fin m) (a : Fin m → UnitAddCircle → ℂ)
    (ha : ∀ r, Continuous (a r)) (ha3 : ∀ r z, ‖a r z‖ ≤ 3)
    {M ε κ : ℝ} (hM : 0 ≤ M) (hε : 0 < ε) (hκ : 0 < κ) :
    ∃ ω : ℝ, 0 < ω ∧ ∀ C : ColoredState (Fin m), C.Reflection τR →
      colorMass C.density ≤ M → ∀ margin : ℝ, 0 < margin → C.InBand b D margin →
      C.Matches d a ω →
      ∃ B : (j : ℕ) → (Fin j → ℤ) → ℤ, ∀ L : Fin n → ℤ,
        (∀ j : Fin n, B j (fun i => L ⟨i.val,i.isLt.trans j.isLt⟩) < L j) →
…

Mentions: OAI.ThreeTorus.ColoredSignalReflectedRealizes, OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.colorMass

theorem OAI.ThreeTorus.ColoredSignalReflectedRealizes.block line 168

Source documentation

Accuracy requirements for the actual anchor are fixed BEFORE that anchor is made. Given any such actual anchor, the two block tests are achieved on one actual endpoint of a sequence of neutral/signal pairs.

theorem ColoredSignalReflectedRealizes.block {b D γ ell : ℝ} {d : ℝ → ℂ}
    (hsignal : ColoredSignalReflectedRealizes b D d γ ell)
    (hdc : Continuous d) (hds : HasCompactSupport d) (hγ : 0 < γ)
    {m n : ℕ} {p : Fin m → UnitAddCircle → ℝ}
    (hp : ∀ r z, 0 ≤ p r z) (hc : ∀ r, Continuous (p r)) (tags : Fin m → ℂ)
    (htags : ∀ r, ‖tags r‖ ≤ 1) {q A : UnitAddCircle → ℂ} (hq : Continuous q)
    (hqB : ∀ z, ‖q z‖ ≤ 2) (hA : Continuous A) (k : ℕ)
    {delta nu ε : ℝ} (hell : 0 < ell) (hells : 6*ell ≤ 1)
    (hd : 0 < delta) (hd1 : delta ≤ 1/100)
    (hn0 : delta/2 ≤ (n:ℝ)*ell^2) (hn1 : (n:ℝ)*ell^2 ≤ delta)
    (hmass : (∫ z, blockTotal p z ∂phaseHaar) ≤ 2)
    (hcenter : (∫ z, Real.sqrt (blockTotal p z)*‖blockTagMean p tags z-q z‖^2 ∂phaseHaar) ≤ delta)
…

Mentions: OAI.ThreeTorus.ColoredSignalReflectedRealizes, OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.blockTagMean

theorem OAI.ThreeTorus.eventually_reflected_anchor_state line 254

Source documentation

Carrier first; signal, band and all block tolerances afterwards; anchor integer last and still arbitrarily large. No modeled next densities occur.

theorem eventually_reflected_anchor_state {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) (hi : Injective F.m) (hmod : F.SpareIndependent)
    {τref : ι → ι} (hr : F.Reflection τref) :
    ∀ᶠ c : ℕ in atTop,
      ∀ (d : ℝ → ℂ) (q : UnitAddCircle → ℂ) (a : ι → ℂ), Continuous q →
      ∀ b D margin τ : ℝ, 0 < τ →
      (∀ i x, x ∈ F.core i → ∀ s,
        |s-(F.m i:ℝ)*((c:ℝ)+F.V x)| < τ →
        d s = a i-q (s:UnitAddCircle) ∧ b+margin ≤ |s| ∧ |s| ≤ D-margin) →
      ∀ ε ω κ : ℝ, 0 < ε → 0 < ω → 0 < κ →
      ∃ g : PassageGeometryFamily F.V, g.c = c ∧
      ∃ δ : ℝ, ∃ cut : LawCutoffs δ, ∃ L : ℝ,
…

Mentions: OAI.ThreeTorus.PassagePackets, OAI.ThreeTorus.PassageGeometryFamily, OAI.ThreeTorus.LawCutoffs

theorem OAI.ThreeTorus.eventually_colored_reflected_anchor line 331

Source documentation

The carrier precedes the block signal and every block accuracy requirement. The output retains the literal actual geometry and finite amplitudes.

theorem eventually_colored_reflected_anchor {m : ℕ} (C : ColoredState (Fin m))
    {τR : Fin m → Fin m} (hrC : C.Reflection τR) :
    ∀ᶠ c : ℕ in atTop,
      ∀ (d : ℝ → ℂ) (q : UnitAddCircle → ℂ) (tags : Fin m → ℂ), Continuous q →
      ∀ b D margin τ : ℝ, 0 < τ →
      (∀ i x, x ∈ C.packets.core i → ∀ s,
        |s-(C.packets.m i:ℝ)*((c:ℝ)+C.packets.V x)| < τ →
        d s = tags (C.color i)-q (s:UnitAddCircle) ∧ b+margin ≤ |s| ∧ |s| ≤ D-margin) →
      ∀ ε e ω κ : ℝ, 0 < ε → 0 < e → 0 < ω → 0 < κ →
      ∀ᶠ n : ℕ in atTop, ∃ s : ColoredAnchor C n,
        s.geometry.c = c ∧
        (∃ δ : ℝ, ∃ cut : LawCutoffs δ, ∃ K : ℝ,
…

Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.ColoredAnchor, OAI.ThreeTorus.LawCutoffs

theorem OAI.ThreeTorus.actual_reflected_block_of_center line 421

Source documentation

All signal parameters and tolerances are fixed before the anchor. The endpoint is a genuine actual state linked by its anchor and finite passage path, and satisfies both prescribed source block inequalities. The input reflection hypotheses are the ordinary packet reality conditions needed to construct the real-symmetric band signal.

theorem actual_reflected_block_of_center {m : ℕ} (C : ColoredState (Fin m))
    (τR : Fin m → Fin m) (hrC : C.Reflection τR)
    (tags : Fin m → ℂ) (htags : ∀ r, ‖tags r‖ ≤ 1)
    (htrR : ∀ r, tags (τR r) = conj (tags r))
    {q A : UnitAddCircle → ℂ} (hq : Continuous q)
    (hqs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : ℝ => q (x:UnitAddCircle)))
    (hqr : ∀ z, q (-z) = conj (q z)) (hqB : ∀ z, ‖q z‖ ≤ 2)
    (hA : Continuous A) (k : ℕ) {delta nu ε κ : ℝ}
    (hd : 0 < delta) (hd1 : delta ≤ 1/100) (hnu : 0 < nu) (hε : 0 < ε) (hκ : 0 < κ)
    (hmass : (∫ z, blockTotal C.density z ∂phaseHaar) ≤ 2)
    (hcenter : (∫ z, Real.sqrt (blockTotal C.density z)*
      ‖blockTagMean C.density tags z-q z‖^2 ∂phaseHaar) ≤ delta) :
…

Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.blockTagMean

structure OAI.ThreeTorus.ActualColoredBlock line 534
Source documentation
An actual finite block, centered using its ACTUAL input packet densities. The finite chain contains the anchor and every signal/refresh pair.
```
structure ActualColoredBlock {m : ℕ} (C E : ColoredState (Fin m))
    (β : Equiv.Perm TripleTorus) (D : UnitAddCircle → ℂ) : Prop where
…
```
Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.TripleTorus
lemma OAI.ThreeTorus.ActualColoredBlock.continuous line 548
lemma OAI.ThreeTorus.ActualColoredBlock.preserves line 551
lemma OAI.ThreeTorus.ActualColoredBlock.physicalError_eq line 554
lemma OAI.ThreeTorus.ActualColoredBlock.estimator_continuous line 560
theorem OAI.ThreeTorus.actual_reflected_block line 565
def OAI.ThreeTorus.physicalEnergy line 600
lemma OAI.ThreeTorus.physicalEnergy_nonneg line 601
lemma OAI.ThreeTorus.physicalEnergy_integrable line 603
lemma OAI.ThreeTorus.scalar_energy_comparison line 607
lemma OAI.ThreeTorus.physicalEnergy_comparison line 615
lemma OAI.ThreeTorus.exists_physical_mass_tolerance line 633
lemma OAI.ThreeTorus.ActualColoredBlock.physicalEnergy_eq line 665
lemma OAI.ThreeTorus.ColoredState.mass_transport_tolerance line 672
lemma OAI.ThreeTorus.fourier_diagonal_smooth_lift line 711
lemma OAI.ThreeTorus.blockDiagonalEstimator_smooth line 719
lemma OAI.ThreeTorus.blockDiagonalEstimator_reflection line 726
lemma OAI.ThreeTorus.ActualColoredBlock.estimator_smooth line 740
lemma OAI.ThreeTorus.ActualColoredBlock.estimator_reflection line 744