IndisputableMonolith.NavierStokes.PhiLadderCutoff
The PhiLadderCutoff module supplies the canonical recognition cost J and the phi-rung scaling primitives that implement discrete ladder cutoffs for Navier-Stokes regularity arguments. Discrete vorticity bookkeeping and stretching-pairs modules import it to obtain monotonicity and positivity facts. The module consists solely of definitions and elementary lemmas on non-negativity and strict monotonicity of the rung scales.
claim$J(x) = ½(x + x^{-1}) - 1$ for $x > 0$; the phi-rung scale at rung $r$ is the strictly increasing positive function satisfying the self-similar recurrence with fixed point $φ$.
background
Recognition Science places the J-cost at T5 of the forcing chain as the unique function satisfying the Recognition Composition Law. The module imports the RS time quantum $τ_0 = 1$ tick from Constants and defines Jcost together with its elementary properties (non-negativity, zero only at unity, positivity elsewhere). It further introduces phiRungScale as the scaling factor on the phi-ladder and cascadeDepth as the finite depth of the cutoff ladder. These objects furnish the exact algebraic bookkeeping required by the lattice Navier-Stokes program.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The definitions feed DiscreteVorticity for finite vorticity fields and RMS amplitudes, FRCBridge for the finite-volume vorticity ratio bound, PhiOptimalCascade for the variational minimization at $φ$, and StretchingPairs for exact RCL balance on paired events. The module thereby supplies the phi-ladder cutoff step that closes the conditional route to Navier-Stokes regularity on the RS lattice.
scope and limits
- Does not derive the Navier-Stokes equations themselves.
- Does not address the continuous-space limit.
- Does not prove global regularity.
- Does not compute numerical values of physical constants.
used by (4)
depends on (1)
declarations in this module (30)
-
def
Jcost -
theorem
Jcost_one -
theorem
Jcost_inv_eq -
theorem
Jcost_nonneg -
theorem
Jcost_eq_zero_iff -
theorem
Jcost_pos -
def
phiRungScale -
theorem
phiRungScale_pos -
theorem
phiRungScale_strictMono -
theorem
phiRungScale_succ -
def
cascadeDepth -
theorem
cascadeDepth_le_one -
theorem
cascadeDepth_finite -
theorem
cascadeDepth_mono -
theorem
finitely_many_rungs_below -
def
subDissipationDecayFactor -
theorem
subDissipationDecayFactor_pos -
theorem
subDissipationDecayFactor_lt_one -
theorem
sub_dissipation_decay_to_zero -
theorem
sub_dissipation_energy_decays -
def
phiRungWavenumber -
theorem
phiRungWavenumber_pos -
theorem
phiRungWavenumber_succ -
theorem
phiRungWavenumber_anti -
def
discreteVelocityDim -
theorem
discrete_finite_dim -
theorem
Jcost_ratio_bound -
theorem
bounded_Jcost_bounded_max -
structure
PhiLadderCutoffCert -
def
phiLadderCutoff