ControlledBlocks.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Physical signal and derivative control through actual repeated blocks, cyclic prediction, and tag selection.

theorem OAI.ThreeTorus.exists_colored_controlled_signal line 19

Source documentation

Symmetric actual refresh--signal pairs, retaining the complete good arc with arbitrarily small excluded measure.

theorem exists_colored_controlled_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) ∧
      ∀ (R : Type) [DecidableEq R], ∀ (C : ColoredState R),
      ∀ τR : R → R, C.Reflection τR →
      ∀ margin : ℝ, 0 < margin → C.InBand b D margin →
      ∀ (a : R → UnitAddCircle → ℂ), (∀ r, Continuous (a r)) →
      ∀ ω : ℝ, 0 ≤ ω → C.Matches d a ω →
…

Mentions: OAI.ThreeTorus.ColoredState

def OAI.ThreeTorus.ColoredSignalControlledRealizes line 97

theorem OAI.ThreeTorus.exists_concrete_colored_controlled_signal line 113

Source documentation

The interface is discharged by the actual geometric construction.

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

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

theorem OAI.ThreeTorus.ColoredSignalControlledRealizes.iterate line 127

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 ColoredSignalControlledRealizes.iterate {b D γ ell : ℝ} {d : ℝ → ℂ}
    (hsignal : ColoredSignalControlledRealizes 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)
    (Q : PhysicalJetData) {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 ω → ∀ F : PhysicalFrame,
      ∃ 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.ColoredSignalControlledRealizes, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.colorMass, OAI.ThreeTorus.PhysicalFrame

theorem OAI.ThreeTorus.ColoredSignalControlledRealizes.block line 256

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

def OAI.ThreeTorus.ColoredAnchor.nextFrame line 342
lemma OAI.ThreeTorus.ColoredAnchor.nextFrame_chart line 345

theorem OAI.ThreeTorus.eventually_colored_controlled_anchor line 350

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_controlled_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) →
      ∀ (Q : PhysicalJetData) (F : PhysicalFrame) (ζ : ℝ), 0 < ζ →
      ∀ ε e ω κ : ℝ, 0 < ε → 0 < e → 0 < ω → 0 < κ →
      ∀ᶠ n : ℕ in atTop, ∃ s : ColoredAnchor C n,
        Q.Close ζ F C.packets.V (s.nextFrame F) s.final.V ∧
…

Mentions: OAI.ThreeTorus.ColoredState, OAI.ThreeTorus.PhysicalJetData, OAI.ThreeTorus.PhysicalFrame, OAI.ThreeTorus.ColoredAnchor

theorem OAI.ThreeTorus.actual_controlled_block_of_center line 448

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_controlled_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) (Q : PhysicalJetData) (F₀ : PhysicalFrame) :
…

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

theorem OAI.ThreeTorus.actual_controlled_block line 562
theorem OAI.ThreeTorus.actual_controlled_repeated_blocks line 596

theorem OAI.ThreeTorus.actual_controlled_density_prediction line 668

Source documentation

The source prediction estimate, for actual reflected packet passages. Every finite family of physical smooth restrictions is imposed in the actual passage selections, in the required quantifier order.

theorem actual_controlled_density_prediction {m : ℕ} (C : ColoredState (Fin m))
    (τR : Fin m → Fin m) (hτR : Involutive τR) (hrC : C.Reflection τR)
    (tags : Fin m → ℂ) (htags : ∀ r, ‖tags r‖ ≤ 1)
    (htrR : ∀ r, tags (τR r) = conj (tags r))
    {ε τ η κ : ℝ} (hε : 0 < ε) (hτ : 0 < τ) (hη : 0 < η) (hκ : 0 < κ)
    (hmass : (∫ z, blockTotal C.density z ∂phaseHaar) < 2) (Q : PhysicalJetData) (F₀ : PhysicalFrame) :
    ∃ E : ColoredState (Fin m), ∃ α : Equiv.Perm TripleTorus,
      ∃ Ψ : UnitAddCircle → ℂ, ∃ K : ℕ, ∃ A : UnitAddCircle → ℂ,
      0 < K ∧ ActualColoredBlocks C E K α A ∧ Ψ = (fun z => A z/(K:ℂ)) ∧
      (∀ r, physicalError (C.vector r) (E.vector r ∘ α) < η) ∧
      ((∫ z, Real.sqrt (blockTotal C.density z) ∂phaseHaar)-τ <
        ∫ z, Real.sqrt (blockTotal E.density z) ∂phaseHaar) ∧
…

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

theorem OAI.ThreeTorus.actual_controlled_cyclic_prediction line 717

Source documentation

Actual finite Laurent approximation to the OLD tagged packet sum after reflected signal blocks. Neither a cyclic-space oracle nor a formal spectral operator is used: the witness is a literal finite sum of twist iterates.

theorem actual_controlled_cyclic_prediction {m : ℕ} (C : ColoredState (Fin m))
    (τR : Fin m → Fin m) (hτR : Involutive τR) (hrC : C.Reflection τR)
    (tags : Fin m → ℂ) (htags : ∀ r, ‖tags r‖ ≤ 1)
    (htrR : ∀ r, tags (τR r) = conj (tags r))
    {ε τ η κ : ℝ} (hε : 0 < ε) (hτ : 0 < τ) (hη : 0 < η) (hκ : 0 < κ)
    (hmass : (∫ z, blockTotal C.density z ∂phaseHaar) < 2) (Q : PhysicalJetData) (F₀ : PhysicalFrame) :
    ∃ E : ColoredState (Fin m), ∃ α : Equiv.Perm TripleTorus,
      ∃ c : ℤ →₀ ℂ, ∃ K : ℕ, ∃ A : UnitAddCircle → ℂ,
      0 < K ∧ ActualColoredBlocks C E K α A ∧
      (∀ r, physicalError (C.vector r) (E.vector r ∘ α) < η) ∧
      ((∫ z, Real.sqrt (blockTotal C.density z) ∂phaseHaar)-τ <
        ∫ z, Real.sqrt (blockTotal E.density z) ∂phaseHaar) ∧
…

lemma OAI.ThreeTorus.ColoredState.laurent_smul line 778

theorem OAI.ThreeTorus.actual_controlled_tagged_prediction line 786

Source documentation

Arbitrary finite reflected tags, rescaled before any signal/jet choices.

theorem actual_controlled_tagged_prediction {m : ℕ} (C : ColoredState (Fin m))
    (τR : Fin m → Fin m) (hτR : Involutive τR) (hrC : C.Reflection τR)
    (tags : Fin m → ℂ) (htrR : ∀ r, tags (τR r) = conj (tags r))
    {ε τ η κ : ℝ} (hε : 0 < ε) (hτ : 0 < τ) (hη : 0 < η) (hκ : 0 < κ)
    (hmass : (∫ z, blockTotal C.density z ∂phaseHaar) < 2)
    (Q : PhysicalJetData) (F₀ : PhysicalFrame) :
    ∃ E : ColoredState (Fin m), ∃ α : Equiv.Perm TripleTorus,
      ∃ c : ℤ →₀ ℂ, ∃ K : ℕ, ∃ A : UnitAddCircle → ℂ,
      0 < K ∧ ActualColoredBlocks C E K α A ∧
      (∀ r, physicalError (C.vector r) (E.vector r ∘ α) < η) ∧
      ((∫ z, Real.sqrt (blockTotal C.density z) ∂phaseHaar)-τ <
        ∫ z, Real.sqrt (blockTotal E.density z) ∂phaseHaar) ∧
…