No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
309theorem decoded_simulation_one_step {N : ℕ} (H : DecodedSimulationHypothesis N) (u : GalerkinState N) :
310 decodeGalerkin2D (N := N)
proof body
Tactic-mode proof.
311 (field := independent.step H.P (encodeGalerkin2D u))
312 (hsize := by simp [LNALSemantics.independent, encodeGalerkin2D])
313 = H.step u :=
314 H.comm u
315
316/-- A constant LNAL program: decrement `nuPhi` by `1` (via `FOLD (-1)`). -/
depends on (14)
Lean names referenced from this declaration's body.
-
H
in IndisputableMonolith.Algebra.CostAlgebra
decl_use
-
GalerkinState
in IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D
decl_use
-
encodeGalerkin2D
in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
decl_use
-
independent
in IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics
decl_use
-
DecodedSimulationHypothesis
in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D
decl_use
-
decodeGalerkin2D
in IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D
decl_use
-
step
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
H
in IndisputableMonolith.Cost.FunctionalEquation
decl_use
-
via
in IndisputableMonolith.Derivations.MassToLight
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
independent
in IndisputableMonolith.Foundation.RSCoupledAxis
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
constant
in IndisputableMonolith.Relativity.Fields.Scalar
decl_use