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)
21structure NSParams where
22 /-- Spatial dimension (use 2 first, then lift to 3). -/
23 d : ℕ := 3
proof body
Definition body.
24 /-- Kinematic viscosity. -/
25 ν : ℝ := 1
26
27/-- Validity predicate for parameters (keep proofs out of the structure to avoid hidden coercions). -/
28def NSParams.Valid (p : NSParams) : Prop :=
29 0 < p.ν ∧ 2 ≤ p.d
30
31/-- A discrete time step (Δt > 0). -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
-
RSNSBridgeSpec
in IndisputableMonolith.ClassicalBridge.Fluids.Bridge
decl_use
-
DiscreteModel
in IndisputableMonolith.ClassicalBridge.Fluids.Discrete
decl_use
depends on (11)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
step
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
A
in IndisputableMonolith.Masses.Anchor
decl_use
-
A
in IndisputableMonolith.Modal.Actualization
decl_use
-
Valid
in IndisputableMonolith.Recognition.Certification
decl_use