InitializedMain.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The initialized-computation main theorem of Finite Instructions and Solenoidal Shear Flows. The machine-only body and input loader are explicit finite rational data.

def OAI.ForcedComputation.machineVelocity line 14
def OAI.ForcedComputation.machineForce line 18
def OAI.ForcedComputation.machineProgram line 23
Source documentation
The compiler outputs two finite rational instruction tables. The body is computed from the machine alone; only the one-period loader uses the input.
```
def machineProgram (I : Alternating.MachineInput) (hI : Alternating.ValidInput I) :
    Input × Input := (recorderLoader I hI, compiledInput I.1 hI.1)
```
Mentions: OAI.Alternating.MachineInput, OAI.Alternating.ValidInput
theorem OAI.ForcedComputation.machineVelocity_tail line 26
theorem OAI.ForcedComputation.machineForce_tail line 31
theorem OAI.ForcedComputation.initialized_computation line 36

theorem OAI.ForcedComputation.machineForce_effective line 94

Source documentation

The force is evaluated to every rational accuracy by the explicit finite loader/body program, with an oracle only for the viscosity and query point.

theorem machineForce_effective (I : Alternating.MachineInput)
    (hI : Alternating.ValidInput I) (ν : ℝ) (α : List (Fin 4))
    {a : ℕ → ℚ} (ha : IsFastRealName a ν) {b : ℕ → RationalSpaceTime}
    {y : SpaceTime} (hb : IsFastName b y) (ε : ℚ) (hε : 0 < ε) :
    ‖mixedDerivative (machineForce ν I hI) α y -
      rationalVector (evaluateInitializedForce (recorderLoader I hI) (compiledInput I.1 hI.1)
        (recorderLoader_valid I hI) (compiledInput_valid I.1 hI.1) α a b ε hε)‖ ≤ (ε : ℝ) :=
…

Mentions: OAI.Alternating.MachineInput, OAI.Alternating.ValidInput, OAI.ForcedComputation.machineForce, OAI.ForcedComputation.evaluateInitializedForce

theorem OAI.ForcedComputation.initialized_effective_computation line 106

Source documentation

The complete initialized main result, including the explicit evaluator and the machine-only tail of both velocity and forcing.

theorem initialized_effective_computation (I : Alternating.MachineInput)
    (hI : Alternating.ValidInput I) (ν : ℝ) (hν : 0 < ν) :
    InitializedFluidProperties 1 ν (machineVelocity I hI) ∧
    (∀ t x, 1 ≤ t →
      machineVelocity I hI (t, x) = (compiledInput I.1 hI.1).realizingVelocity (t, x) ∧
      machineForce ν I hI (t, x) = force ν (compiledInput I.1 hI.1).realizingVelocity (t, x)) ∧
    (∀ (α : List (Fin 4)) (a : ℕ → ℚ) (b : ℕ → RationalSpaceTime) (y : SpaceTime),
      IsFastRealName a ν → IsFastName b y → ∀ (ε : ℚ) (hε : 0 < ε),
        ‖mixedDerivative (machineForce ν I hI) α y -
          rationalVector (evaluateInitializedForce (recorderLoader I hI) (compiledInput I.1 hI.1)
            (recorderLoader_valid I hI) (compiledInput_valid I.1 hI.1) α a b ε hε)‖ ≤ (ε : ℝ)) ∧
    ∃ Φ : ℝ → Space → Space, IsMaterialFlow 1 (machineVelocity I hI) Φ ∧
…

Mentions: OAI.Alternating.MachineInput, OAI.Alternating.ValidInput, OAI.ForcedComputation.InitializedFluidProperties, OAI.ForcedComputation.machineVelocity, OAI.ForcedComputation.machineForce, OAI.ForcedComputation.evaluateInitializedForce