phiLadderCutoff
plain-language theorem explainer
This definition assembles the complete certificate structure for the phi-ladder ultraviolet cutoff by supplying the non-negativity of J-cost, its zero characterization at unity, finite and monotone cascade depth, sub-dissipation decay to zero, finite rungs below any scale, and bounded J-cost excluding blowup. A researcher working on Navier-Stokes regularity via the discrete lattice cutoff would cite it as the assembled result closing the module. The construction is a direct record definition that references the upstream lemmas for each field.
Claim. The phi-ladder cutoff certificate is the structure containing non-negativity of the J-cost function $J(x) geq 0$ for all $x > 0$, the equivalence $J(x) = 0 iff x = 1$, existence of a finite natural number $N$ such that cascade depth equals $N$ for every Reynolds number, monotonicity of cascade depth under increasing Reynolds number above 1, the sub-dissipation decay factor strictly less than 1 with convergence to zero, only finitely many rungs below any scale $L$, and bounded J-cost implying bounded maximum value.
background
The module formalizes the algebraic and combinatorial core of the argument that the phi-ladder provides an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the Recognition Science discrete lattice. Key definitions include the J-cost function, whose non-negativity follows from the AM-GM inequality on $x + x^{-1} geq 2$, and cascade depth, which counts the number of phi-rungs needed for a given Reynolds number. The certificate structure packages these together with decay and boundedness properties drawn from the Cost module and local siblings such as bounded_Jcost_bounded_max.
proof idea
This is a definition that constructs the certificate record by direct assignment of each field to an upstream lemma: Jcost_nonneg supplies the non-negativity certificate, Jcost_eq_zero_iff supplies the zero-iff-unity equivalence, cascadeDepth_finite supplies finiteness, cascadeDepth_mono supplies monotonicity, subDissipationDecayFactor_lt_one and sub_dissipation_decay_to_zero supply the decay statements, finitely_many_rungs_below supplies the finite-rungs claim, and bounded_Jcost_bounded_max supplies the blowup exclusion.
why it matters
This declaration completes the assembly of results in the Navier-Stokes phi-ladder cutoff module and is the main certificate referenced in the paper NS_Regularity_Phi_Ladder_Cutoff.tex. It packages the properties needed to show that the phi-ladder terminates the energy cascade, connecting to the Recognition Science framework landmarks of J-uniqueness and the phi-ladder for discrete regularization. No downstream uses are recorded, indicating it serves as the terminal packaging step for the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.