PeriodicLatticeCorollaryMain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The rapid-torus corollary with its stated fixed particle and observation slab. The construction is a rational transverse change of the proved lattice program; in particular no Poisson existence or computation assumption is used.

def OAI.PeriodicLattice.RapidTorus.IsCorollaryParticle line 17
def OAI.PeriodicLattice.RapidTorus.CorollaryConclusion line 21
theorem OAI.PeriodicLattice.RapidTorus.solenoidal_rapid_torus line 36
Source documentation
Corollary cor:rapid-torus of paper 379-06: the exact fixed label is (1/2,1/4,1/2) and the open observation slab is 1/4 < x₀ < 3/8. Both the velocity and solenoidal force have terminating evaluators and computable bounds for every mixed derivative and every polynomial decay rate.
```
theorem solenoidal_rapid_torus (ν : ℝ) (hν : 0 < ν) (hc : ComputableReal ν) :
    IsOpen corollaryDetector ∧
    ∃ (U f : Input → VectorField) (p : Input → ScalarField)
      (C : Input → ℕ → MultiIndex → ℕ → ℕ),
      UniformlyEffective U ∧ UniformlyEffective f ∧ EffectiveConstants C ∧
      ∀ d : Input, d.WellFormed → CorollaryConclusion ν d (U d) (f d) (p d) (C d) := by
…
```
Mentions: OAI.PeriodicLattice.ComputableReal, OAI.PeriodicLattice.RapidTorus.corollaryDetector, OAI.PeriodicLattice.Input, OAI.PeriodicLattice.VectorField, OAI.PeriodicLattice.ScalarField, OAI.PeriodicLattice.MultiIndex, OAI.PeriodicLattice.UniformlyEffective, OAI.PeriodicLattice.EffectiveConstants, OAI.PeriodicLattice.RapidTorus.CorollaryConclusion