OAI/Dynamics/ThreeTorus/ColorBlocks.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Block transfer, cofinal frequency trees, color-density products, finite iteration, and actual anchored blocks.

  1. def OAI.ThreeTorus.blockModelColors line 16
  2. def OAI.ThreeTorus.blockDiagonalEstimator line 20
  3. lemma OAI.ThreeTorus.continuous_blockPhaseEstimator_diagonal line 24
  4. lemma OAI.ThreeTorus.continuous_blockModelColors line 30
  5. lemma OAI.ThreeTorus.blockModelColors_nonneg line 37
  6. lemma OAI.ThreeTorus.blockPhaseEstimator_norm line 50
  7. lemma OAI.ThreeTorus.block_estimator_weight_bound line 68
  8. lemma OAI.ThreeTorus.integral_blockErrorTest_diagonal line 89
  9. theorem OAI.ThreeTorus.block_diagonal_transfer line 104

    Source documentation

    The analytic tolerance is fixed before all diagonal frequency choices. The conclusion applies to any actual nonnegative continuous densities with that total color error. It makes no assertion that geometry realizes them.

    theorem block_diagonal_transfer {m n : ℕ} {p : Fin m → UnitAddCircle → ℝ}
    (hp : ∀ r z, 0 ≤ p r z) (hc : ∀ r, Continuous (p r)) (b : Fin m → ℂ)
    (hb : ∀ r, ‖b r‖ ≤ 1) {q A : UnitAddCircle → ℂ} (hq : Continuous q)
    (hqB : ∀ z, ‖q z‖ ≤ 2) (hA : Continuous A) (k : ℕ)
    {ell delta nu : ℝ} (hell : 0 < ell) (hs : 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 b z-q z‖^2 ∂phaseHaar) ≤ delta)
    (hnu : 0 < nu) :
    ∃ e0 : ℝ, 0 < e0 ∧ ∀ B : (j : ℕ) → (Fin j → ℤ) → ℤ,
      ∃ L : Fin n → ℤ, (∀ j, 0 < L j) ∧
…

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

  10. lemma OAI.ThreeTorus.finite_frequency_tree line 186
  11. def OAI.ThreeTorus.colorMass line 234
  12. def OAI.ThreeTorus.colorModel line 237
  13. lemma OAI.ThreeTorus.colorFactor_bounds line 242
  14. lemma OAI.ThreeTorus.continuous_colorModel line 254
  15. lemma OAI.ThreeTorus.colorModel_zero line 261
  16. lemma OAI.ThreeTorus.colorModel_snoc line 267
  17. lemma OAI.ThreeTorus.colorModel_bounds line 275
  18. lemma OAI.ThreeTorus.colorMass_le_add_distance line 287
  19. lemma OAI.ThreeTorus.colorModel_mass_bound line 304
  20. lemma OAI.ThreeTorus.colorL1Distance_symm line 316
  21. lemma OAI.ThreeTorus.colorModel_step_error line 321
  22. lemma OAI.ThreeTorus.colorModel_initial_error line 340
  23. lemma OAI.ThreeTorus.colorModel_eq_blockModelColors line 355
  24. lemma OAI.ThreeTorus.ColoredPair.physicalError_chart line 377
  25. inductive OAI.ThreeTorus.ColoredPath line 387

    Source documentation

    A finite trace contains actual neutral--signal pairs, including their smooth geometry and exact intermediate speeds.

    inductive ColoredPath {R : Type} (C : ColoredState R) :
    {k : ℕ} → (Fin k → ℤ) → ColoredState R → Equiv.Perm TripleTorus → Prop
  | nil : ColoredPath C (fun i => Fin.elim0 i) C (Equiv.refl TripleTorus)
  | snoc {k : ℕ} {L : Fin k → ℤ} {D : ColoredState R} {α : Equiv.Perm TripleTorus}
      (h : ColoredPath C L D α) {N : ℕ} (s : ColoredPair D N) :
      ColoredPath C (Fin.snoc L (N:ℤ)) s.output (α.trans s.chart)

namespace ColoredPath
variable {R : Type} {C D : ColoredState R} {k : ℕ} {L : Fin k → ℤ}
    {α : Equiv.Perm TripleTorus} (h : ColoredPath C L D α)
include h

    Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.TripleTorus, OAI.ThreeTorus.ColoredPair

  26. lemma OAI.ThreeTorus.ColoredPath.continuous line 398
  27. lemma OAI.ThreeTorus.ColoredPath.preserves line 402
  28. lemma OAI.ThreeTorus.ColoredPath.physicalError_eq line 406
  29. lemma OAI.ThreeTorus.eventually_int_of_eventually_nat line 415
  30. def OAI.ThreeTorus.iterationError line 432
  31. lemma OAI.ThreeTorus.iterationError_nonneg line 434
  32. lemma OAI.ThreeTorus.iterationError_step line 438
  33. lemma OAI.ThreeTorus.finite_iteration_budget line 448

    Source documentation

    Choices are uniform over the future actual packet states.

    lemma finite_iteration_budget (n : ℕ) {M γ ε : ℝ} (hM : 0 ≤ M) (hγ : 0 < γ)
    (hε : 0 < ε) :
    ∃ t ω U : ℝ, 0 < t ∧ 0 < ω ∧ 0 < U ∧ iterationError t n < ε ∧
      (∀ k ≤ n, M*2^k+iterationError t k ≤ U) ∧
      ∀ k ≤ n, 2*γ*(((k:ℝ)+1)*ω)*U ≤ t/2 := by
…

    Mentions: OAI.ThreeTorus.iterationError

  34. lemma OAI.ThreeTorus.finite_color_tolerance line 483
  35. def OAI.ThreeTorus.ColoredSignalRealizes line 508
  36. theorem OAI.ThreeTorus.exists_concrete_colored_signal line 520

    Source documentation

    The interface is discharged by the actual geometric construction.

    theorem exists_concrete_colored_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) ∧
      ColoredSignalRealizes b D d γ (refreshedStrength (signalPrimeProduct L) γ) :=
…

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

  37. theorem OAI.ThreeTorus.ColoredSignalRealizes.iterate line 534

    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 ColoredSignalRealizes.iterate {b D γ ell : ℝ} {d : ℝ → ℂ}
    (hsignal : ColoredSignalRealizes b D d γ ell)
    (hd : Continuous d) (hdc : HasCompactSupport d) (hγ : 0 < γ)
    (hell : 0 ≤ ell) (hells : 6*ell ≤ 1)
    (m n : ℕ) (a : Fin m → UnitAddCircle → ℂ)
    (ha : ∀ r, Continuous (a r)) (ha3 : ∀ r z, ‖a r z‖ ≤ 3)
    {M ε : ℝ} (hM : 0 ≤ M) (hε : 0 < ε) :
    ∃ ω : ℝ, 0 < ω ∧ ∀ C : ColoredState (Fin m),
      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.ColoredSignalRealizes, OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.colorMass

  38. lemma OAI.ThreeTorus.colorMass_eq_integral_total line 651
  39. theorem OAI.ThreeTorus.ColoredSignalRealizes.block line 662

    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 ColoredSignalRealizes.block {b D γ ell : ℝ} {d : ℝ → ℂ}
    (hsignal : ColoredSignalRealizes 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.ColoredSignalRealizes, OAI.ThreeTorus.blockTotal, OAI.ThreeTorus.phaseHaar, OAI.ThreeTorus.blockTagMean

  40. theorem OAI.ThreeTorus.exists_symmetric_anchor_band line 739

    Source documentation

    Smooth interpolation near a finite pairwise disjoint compact family off zero, with the exact reflection required by the real signal law.

    theorem exists_symmetric_anchor_band {ι : Type*} [Fintype ι]
    (K : ι → Set ℝ) (hK : ∀ i, IsCompact (K i))
    (hdisj : Pairwise (Disjoint on K)) (h0 : ∀ i, 0 ∉ K i)
    (τ : ι → ι) (hKr : ∀ i x, x ∈ K i → -x ∈ K (τ i))
    (b : ι → ℂ) (hbr : ∀ i, b (τ i) = conj (b i))
    {q : UnitAddCircle → ℂ}
    (hqs : ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) (fun x : ℝ => q (x:UnitAddCircle)))
    (hqr : ∀ z, q (-z) = conj (q z)) :
    ∃ d : ℝ → ℂ,
      ContDiff ℝ ((⊤ : ℕ∞) : WithTop ℕ∞) d ∧ HasCompactSupport d ∧
      d 0 = 0 ∧ (∀ x, d (-x) = conj (d x)) ∧
      ∀ i x, x ∈ K i → d =ᶠ[𝓝 x] (fun y => b i-q (y:UnitAddCircle)) := by
…
  41. lemma OAI.ThreeTorus.finite_positive_lower line 818
  42. theorem OAI.ThreeTorus.anchor_uniform_room line 837

    Source documentation

    A single positive enlargement works for every compact frequency image. The band bounds also contain the entire compact signal support.

    theorem anchor_uniform_room {ι : Type*} [Fintype ι]
    (K : ι → Set ℝ) (hK : ∀ i, IsCompact (K i)) (h0 : ∀ i, 0 ∉ K i)
    {d : ℝ → ℂ} (hdc : HasCompactSupport d)
    (a : ι → ℝ → ℂ) (hl : ∀ i x, x ∈ K i → d =ᶠ[𝓝 x] a i) :
    ∃ b D μ τ : ℝ, 0 < b ∧ b < D ∧ 0 < μ ∧ 0 < τ ∧
      support d ⊆ Icc (-D) D ∧
      ∀ i x, x ∈ K i → ∀ y, |y-x| < τ →
        d y = a i y ∧ b+μ ≤ |y| ∧ |y| ≤ D-μ := by
…

    Mentions: OAI.ThreeTorus.μ

  43. lemma OAI.ThreeTorus.anchor_temporal_deviation line 886
  44. theorem OAI.ThreeTorus.anchor_coefficient_budget line 900

    Source documentation

    Coefficient substitution on EVERY new speed point (not only a nonzero spectral-density set). This is what the next real packet passage needs.

    theorem anchor_coefficient_budget {ι : Type*} [Fintype ι]
    {q : UnitAddCircle → ℂ} (hq : Continuous q)
    {d : ℝ → ℂ} (a : ι → ℂ) {D ω : ℝ} (hω : 0 < ω) :
    ∀ R : ℝ, ∀ᶠ n : ℕ in atTop, 0 < n ∧
      ∀ (j : ℤ) (i : ι) (J : ℝ), |(j:ℝ)/(n:ℝ)| ≤ D → |J| ≤ R →
        d ((j:ℝ)/(n:ℝ)) = a i-q ((j:ℝ)/(n:ℝ):UnitAddCircle) →
        ‖d ((j:ℝ)/(n:ℝ))-(a i-q ((j:ℝ)*((1+J/(n:ℝ))/(n:ℝ)):UnitAddCircle))‖ < ω := by
…
  45. theorem OAI.ThreeTorus.eventually_anchor_state line 937

    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_anchor_state {ι : Type*} [Fintype ι]
    (F : PassagePackets ι) (hi : Injective F.m) (hmod : F.SpareIndependent) :
    ∀ᶠ 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 : ℝ,
        0 < δ ∧ δ < κ ∧ 0 < L ∧ g.J₀ = neutralJitterReal cut L 0 ∧
…

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

  46. lemma OAI.ThreeTorus.colorVector_output line 1009
  47. lemma OAI.ThreeTorus.colorDensity_output line 1022
  48. structure OAI.ThreeTorus.ColoredAnchor line 1035
  49. def OAI.ThreeTorus.ColoredAnchor.output line 1047
  50. def OAI.ThreeTorus.ColoredAnchor.chart line 1057
  51. lemma OAI.ThreeTorus.ColoredAnchor.chart_continuous line 1058
  52. lemma OAI.ThreeTorus.ColoredAnchor.chart_preserves line 1059
  53. theorem OAI.ThreeTorus.eventually_colored_anchor line 1065

    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_anchor {m : ℕ} (C : ColoredState (Fin m)) :
    ∀ᶠ 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 : ℝ,
          0 < δ ∧ δ < κ ∧ 0 < K ∧ s.geometry.J₀ = neutralJitterReal cut K 0) ∧
…

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

  54. lemma OAI.ThreeTorus.exists_block_length line 1146
  55. theorem OAI.ThreeTorus.actual_block_of_center line 1167

    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_block_of_center {m : ℕ} (C : ColoredState (Fin m))
    (τ : C.Index → C.Index)
    (hmr : ∀ i, C.packets.m (τ i) = -C.packets.m i)
    (hcore : ∀ i, C.packets.core i ⊆ C.packets.core (τ i))
    (tags : Fin m → ℂ) (htags : ∀ r, ‖tags r‖ ≤ 1)
    (htr : ∀ i, tags (C.color (τ i)) = conj (tags (C.color i)))
    {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)
…

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