PrefixMain.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The initialized prefix-computation main theorem: the fixed label and unit-torus observer are those in Prefix Instructions and Incompressible Flows. The repeated table uses the machine alone, and the input appears only in the finite rational loader.

def OAI.ForcedComputation.prefixStart line 13
def OAI.ForcedComputation.prefixProgram line 15
theorem OAI.ForcedComputation.prefixLoader_valid line 19
theorem OAI.ForcedComputation.prefixBody_valid line 24
def OAI.ForcedComputation.prefixVelocity line 28
def OAI.ForcedComputation.prefixForce line 31

theorem OAI.ForcedComputation.prefix_effective_computation line 36

Source documentation

Full fixed-label main result, with the finite force evaluator and the machine-only repeated velocity/force template exposed in its statement.

theorem prefix_effective_computation (I : Alternating.MachineInput)
    (hI : Alternating.ValidInput I) (ν : ℝ) (hν : 0 < ν) :
    InitializedFluidProperties 1 ν (prefixVelocity I hI) ∧
    (∀ t x, 1 ≤ t →
      prefixVelocity I hI (t, x) = (recorderInputAtHeight I.1 hI.1 (1 / 4)).realizingVelocity (t, x) ∧
      prefixForce ν I hI (t, x) =
        force ν (recorderInputAtHeight I.1 hI.1 (1 / 4)).realizingVelocity (t, x)) ∧
    (∀ (α : List (Fin 4)) (a : ℕ → ℚ) (b : ℕ → RationalSpaceTime) (y : SpaceTime),
      IsFastRealName a ν → IsFastName b y → ∀ (ε : ℚ) (hε : 0 < ε),
        ‖mixedDerivative (prefixForce ν I hI) α y -
          rationalVector (evaluateInitializedForce (prefixProgram I hI).1 (prefixProgram I hI).2
            (prefixLoader_valid I hI) (prefixBody_valid I hI) α a b ε hε)‖ ≤ (ε : ℝ)) ∧
…

Mentions: OAI.Alternating.MachineInput, OAI.Alternating.ValidInput, OAI.ForcedComputation.InitializedFluidProperties, OAI.ForcedComputation.prefixVelocity, OAI.ForcedComputation.prefixForce, OAI.ForcedComputation.evaluateInitializedForce, OAI.ForcedComputation.prefixProgram, OAI.ForcedComputation.prefixLoader_valid, OAI.ForcedComputation.prefixBody_valid