frc_holds_on_RS_lattice
plain-language theorem explainer
frc_holds_on_RS_lattice asserts that every finite-volume vorticity profile on an RS lattice satisfies the strong lattice FRC bound. Navier-Stokes regularity researchers cite it to anchor the lattice hypothesis inside the conditional completion chain. The proof is a direct one-line application of the explicit finite-volume J-cost bound.
Claim. For any finite-volume vorticity profile $s$, the recognition cost of the normalized vorticity ratio satisfies $J(omegaMax/omegaRms) le sqrt(siteCount)$.
background
The FRCBridge module supplies the logical link between the lattice phi-ladder cutoff and the abstract conditional-completion route for Navier-Stokes regularity. FiniteVolumeProfile packages a positive integer siteCount, positive reals omegaMax and omegaRms obeying omegaRms le omegaMax, and the finite-volume control omegaMax le sqrt(siteCount) * omegaRms. RSLatticeFRC s is the proposition that Jcost of the normalized ratio omegaMax/omegaRms is at most sqrt(siteCount).
proof idea
The proof is a one-line wrapper that applies the finiteVolume_Jcost_bound theorem directly to the input profile s.
why it matters
It supplies the concrete lattice FRC instance used by frcBridgeCert to package the full bridge certificate and by lattice_regular_via_direction_constancy to derive regularity from the abstract route. In the Recognition Science setting it closes the lattice cutoff to the FRC hypothesis in the conditional chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.