CompactDetectorMain.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The general-center injection, stirring and waiting theorem, including both numerical pairs and the input-relative effective force. The scalar existence, heat estimate and smooth-dependence inputs remain explicit.

structure OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput line 17
Source documentation
The prescribed periodic planar processor and its effective derivative data. The force compiler invokes only this input oracle.
```
structure ProcessorInput (V : ℝ → Plane → Plane) where
…
```
theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.third_component line 25
theorem OAI.ForcedComputation.VelocityDetector.CompactCenter.compact_detector line 33
Source documentation
Injection, stirring and waiting. The same prescribed force works for either quantitative (d,H) pair.
```
theorem compact_detector (hE : TorusScalarExistence) (hK : TorusHeatInput)
    {V : ℝ → Plane → Plane} (hV : ProcessorInput V)
    (Ψ : ℝ → ℝ → Plane → Plane) (hΨ : IsPlanarTransition V Ψ)
    (hv : PlanarVariations V Ψ)
    (hback : ContDiff ℝ ∞ (fun y : ℝ × Plane => Ψ y.1 (-y.1) y.2))
    (L : ℕ) (hL : 0 < L)
    (h₁ : ∀ s x, ‖fderiv ℝ (euclideanMap (V s)) x‖ ≤ (L : ℝ))
    (h₂ : ∀ s x, ‖fderiv ℝ (fderiv ℝ (euclideanMap (V s))) x‖ ≤ (L : ℝ))
    (p : Plane) (b : ℕ → RationalSpaceTime)
    (hb : IsFastName b (shiftSpaceTime (centerShift p))) :
    let C := detectorBumpDerivativeBound
…
```
Mentions: OAI.ForcedComputation.VelocityDetector.TorusScalarExistence, OAI.ForcedComputation.VelocityDetector.TorusHeatInput, OAI.ForcedComputation.VelocityDetector.CompactCenter.ProcessorInput, OAI.ForcedComputation.IsPlanarTransition, OAI.ForcedComputation.PlanarVariations, OAI.ForcedComputation.euclideanMap, OAI.ForcedComputation.VelocityDetector.CompactCenter.shiftSpaceTime, OAI.ForcedComputation.VelocityDetector.CompactCenter.centerShift, OAI.ForcedComputation.VelocityDetector.detectorBumpDerivativeBound