BalancedMain.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The compact balanced main theorem includes a terminating evaluator for every mixed derivative of the prescribed force.

theorem OAI.ForcedComputation.Balanced.balanced_three_stack_realization line 16

Source documentation

The two finite coefficients prescribe the compact zero-data flow for every viscosity; named finite queries evaluate every force derivative.

theorem balanced_three_stack_realization :
    IsCompact BalancedVelocity.support ∧
    ∀ (I : Alternating.MachineInput) (hI : Alternating.ValidInput I),
      (∀ ν : ℝ, force I hI ν = BalancedVelocity.force₀ I hI +
        ν • BalancedVelocity.force₁ I hI) ∧
      (∀ (α : List (Fin 4)) (b : ℕ → RationalSpaceTime) (y : SpaceTime),
        IsFastName b y → ∀ (ε : ℚ) (hε : 0 < ε),
          ‖mixedDerivative (BalancedVelocity.force₀ I hI) α y -
            rationalVector (BalancedExpressions.evaluateCoefficient₀ I hI α b ε hε)‖ ≤ (ε : ℝ) ∧
          ‖mixedDerivative (BalancedVelocity.force₁ I hI) α y -
            rationalVector (BalancedExpressions.evaluateCoefficient₁ I hI α b ε hε)‖ ≤ (ε : ℝ)) ∧
      (∀ ν : ℝ, 0 < ν → FluidProperties I hI ν) ∧
…

Mentions: OAI.ForcedComputation.BalancedVelocity.support, OAI.Alternating.MachineInput, OAI.Alternating.ValidInput, OAI.ForcedComputation.Balanced.force, OAI.ForcedComputation.BalancedVelocity.force₀, OAI.ForcedComputation.BalancedVelocity.force₁, OAI.ForcedComputation.BalancedExpressions.evaluateCoefficient₀, OAI.ForcedComputation.BalancedExpressions.evaluateCoefficient₁, OAI.ForcedComputation.Balanced.FluidProperties