CompactDetectorCore.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The injection, stirring and waiting argument for an arbitrary planar processor at a fixed reference center. Both numerical pairs use the same prescribed program.

def OAI.ForcedComputation.VelocityDetector.DetectorPair line 14
theorem OAI.ForcedComputation.VelocityDetector.DetectorPair.clearance line 17

theorem OAI.ForcedComputation.VelocityDetector.fixed_center_compact_detector line 22

Source documentation

The scalar construction and its two observation implications do not depend on a machine encoding or on the geometry of a particular target.

theorem fixed_center_compact_detector (hE : TorusScalarExistence) (hK : TorusHeatInput)
    {V : ℝ → Plane → Plane} {Ψ : ℝ → ℝ → Plane → Plane}
    (hV : ContDiff ℝ ∞ (Function.uncurry V)) (hp : ∀ s, PlanePeriodic (V s))
    (hdiv : ∀ s x, PlanarHamiltonian.divergence (V s) x = 0)
    (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 : ℝ)) :
    ∃ w : ℝ → Plane → ℝ,
      GlobalTorusScalarSolution 1 (detectorDrift V detectorBumpDerivativeBound L)
        (detectorSource detectorBumpDerivativeBound L) w (fun _ => 0) ∧
…