AutonomousStartup.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Starting an autonomous periodic field from rest

The startup step in §6 of Universal Computation with Eventually Stationary Navier–Stokes Forcing. This proves the analytic transfer for an actual smooth field, including its material flow. The computational planar processor is a separate construction, not an assumption hidden in this transfer.

theorem OAI.ForcedComputation.residual_smooth line 24
theorem OAI.ForcedComputation.residual_solves_NS line 29
theorem OAI.ForcedComputation.ramp_smooth line 44
theorem OAI.ForcedComputation.ramp_periodic line 49
theorem OAI.ForcedComputation.ramp_lipschitz line 55
theorem OAI.ForcedComputation.ramp_materialFlow line 67
theorem OAI.ForcedComputation.startupRamp_abs_le_one line 88
theorem OAI.ForcedComputation.periodic_spatial_lipschitz line 92

theorem OAI.ForcedComputation.startup_materialFlow line 102

Source documentation

The fixed startup preserves every nonnegative-time observation event.

theorem startup_materialFlow {L : ℝ} (hL : 0 < L) {W : Space → Space}
    (hW : ContDiff ℝ ∞ W) (hp : ∀ x n, W (x + latticeVector L n) = W x) :
    ∃ Φ : ℝ → Space → Space,
      IsMaterialFlow L (fun y => W y.2) Φ ∧
      IsMaterialFlow L (rampVelocity startupRamp W)
        (fun t x => Φ (accumulatedClock startupRamp t) x) ∧
      ∀ x O, Reaches (fun t => Φ (accumulatedClock startupRamp t) x) O ↔
        Reaches (fun t => Φ t x) O := by
…

Mentions: OAI.ForcedComputation.rampVelocity, OAI.ForcedComputation.startupRamp, OAI.ForcedComputation.accumulatedClock, OAI.ForcedComputation.Reaches

theorem OAI.ForcedComputation.startup_solution line 122

Source documentation

The startup field is a classical forced solution from rest, with a force which is exactly stationary on the closed interval [1,∞).

theorem startup_solution {L : ℝ} {W : Space → Space}
    (hW : ContDiff ℝ ∞ W) (hp : ∀ x n, W (x + latticeVector L n) = W x)
    (hd : ∀ x, divergence W x = 0) (ν : ℝ) :
    ContDiff ℝ ∞ (rampVelocity startupRamp W) ∧
    ContDiff ℝ ∞ (residual ν (rampVelocity startupRamp W)) ∧
    IsClassicalSolution L ν (residual ν (rampVelocity startupRamp W))
      (rampVelocity startupRamp W) (fun _ => 0) ∧
    ∀ t, 1 ≤ t → ∀ x,
      residual ν (rampVelocity startupRamp W) (t, x) =
        advection W x - ν • laplacian W x := by
…

Mentions: OAI.ForcedComputation.rampVelocity, OAI.ForcedComputation.startupRamp, OAI.ForcedComputation.residual

theorem OAI.ForcedComputation.startup_solution_unique line 139
theorem OAI.ForcedComputation.startup_energy_bounded line 155