module module

`IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.ClassicalBridge.Fluids.Regularity2D module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D module_import
IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics module_import

declarations in this module (21)

def foldPlusOneProgram L41
lemma voxelStep_foldPlusOneProgram L45
def foldPlusOneStep L51
lemma floor_abs_intCast L58
lemma cast_lt_zero_iff L64
lemma clampI32_pos_of_ge_one L74
lemma coeffMag_foldPlusOneStep L94
lemma coeffSign_foldPlusOneStep L127
lemma decide_lt_zero_foldPlusOneStep L166
lemma voxelStep_foldPlusOne_encodeIndex L203
def decodeMag L222
def decodeCoeff L226
def decodeGalerkin2D L233
structure SimulationHypothesis L240
theorem simulation_one_step L280
structure DecodedSimulationHypothesis L295
theorem decoded_simulation_one_step L309
def foldMinusOneProgram L317
lemma voxelStep_foldMinusOneProgram L321
def foldMinusOneDecodedStep L329
lemma decodeCoeff_voxelStep_foldMinusOne_encodeIndex L337