PhiLadderCutoffCert
plain-language theorem explainer
PhiLadderCutoffCert packages eight properties of the recognition cost J, cascade depth, sub-dissipation decay, rung finiteness, and blowup exclusion to certify the phi-ladder ultraviolet cutoff for Navier-Stokes energy cascades on the RS lattice. Fluid dynamicists working on discrete regularizations would cite it to invoke termination of the cascade. The proof is a sorry stub that simply assembles existing module lemmas into one record.
Claim. A record certifying: for all $x>0$, the recognition cost $J(x)=(x+x^{-1})/2-1$ obeys $J(x)≥0$ with equality precisely when $x=1$; for every Reynolds number $re$ the cascade depth is finite and monotone non-decreasing for $re>1$; the sub-dissipation decay factor is strictly less than 1 with powers tending to 0; only finitely many phi-rungs lie below any scale $L$; and if $J(max_val/ref_val)≤B$ then $max_val≤(2B+2)ref_val$.
background
The module formalizes the algebraic and combinatorial core of the claim that the φ-ladder supplies an ultraviolet cutoff terminating the Navier-Stokes energy cascade on the RS discrete lattice. Jcost is the recognition cost $J(x)=(x+x^{-1})/2-1$ for $x>0$, normalized so that $J(1)=0$. cascadeDepth and phiRungScale quantify the depth of the energy cascade for a given Reynolds number and the scale at each rung of the phi-ladder, respectively.
proof idea
The declaration is a scaffolding structure whose body is a sorry stub. It packages the lemmas Jcost_nonneg, Jcost_eq_zero_iff, cascadeDepth_finite, cascadeDepth_mono, subDissipationDecayFactor_lt_one, sub_dissipation_decay_to_zero, finitely_many_rungs_below and the blowup exclusion statement directly into the eight fields.
why it matters
This certificate supplies the main packaging for the phi-ladder cutoff argument and is consumed by the downstream definition phiLadderCutoff, which assembles the results with zero sorry. It fills the combinatorial core of the ultraviolet cutoff on the RS lattice, linking J-cost properties to cascade termination and decay to zero. The open question it touches is the full discharge of the stub to obtain a complete theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.