NavierStokes
NavierStokes modules in the audited public canon. Hand-written Lean theorems, sorry-free, with no domain-specific axioms.
| module | thm | lemma | def | lines | papers |
|---|---|---|---|---|---|
NavierStokes.DiscreteMaximumPrinciple |
9 | 0 | 0 | 190 | — |
NavierStokes.DiscreteNSOperator |
13 | 0 | 14 | 311 | — |
NavierStokes.DiscreteVorticity |
6 | 0 | 8 | 125 | — |
NavierStokes.EightTickDynamics |
6 | 0 | 2 | 91 | — |
NavierStokes.FRCBridge |
9 | 0 | 4 | 176 | — |
NavierStokes.FourierExtraction |
15 | 0 | 4 | 167 | — |
NavierStokes.Galerkin3D |
6 | 3 | 7 | 179 | — |
NavierStokes.GalerkinEquicontinuity |
7 | 0 | 1 | 185 | — |
NavierStokes.JcostMonotonicity |
2 | 0 | 1 | 63 | — |
NavierStokes.PhiLadderCutoff |
22 | 0 | 7 | 255 | — |
NavierStokes.PhiOptimalCascade |
8 | 0 | 2 | 109 | — |
NavierStokes.RM2U.BetInstantiation |
8 | 0 | 0 | 184 | — |
NavierStokes.RM2U.Core |
0 | 0 | 6 | 73 | — |
NavierStokes.RM2U.EnergyIdentity |
4 | 0 | 2 | 515 | — |
NavierStokes.RM2U.NonParasitism |
24 | 0 | 2 | 1145 | — |
NavierStokes.RM2U.ProjectedPDE |
0 | 0 | 0 | 136 | — |
NavierStokes.RM2U.RM2Closure |
2 | 0 | 1 | 179 | — |
NavierStokes.RM2U.TailFluxInstantiation |
13 | 0 | 3 | 502 | — |
NavierStokes.RunningMaxNormalization |
15 | 0 | 4 | 363 | — |
NavierStokes.SkewHarmGate |
0 | 6 | 0 | 461 | — |
NavierStokes.StretchingPairs |
6 | 0 | 4 | 98 | — |
NavierStokes.VortexStretching |
8 | 0 | 1 | 145 | — |