LatticeFRC
plain-language theorem explainer
LatticeFRC asserts the existence of a finite upper bound on the recognition cost of the normalized vorticity ratio for any finite-volume profile on an RS lattice. Conditional-completion analyses of Navier-Stokes regularity cite it as the lattice-derived FRC input. The definition is a direct existential wrapper around the cost function applied to the ratio of maximum to root-mean-square vorticity.
Claim. For a finite-volume vorticity profile $s$, the property holds if there exists a real number $B$ such that the recognition cost of the ratio of maximum vorticity to root-mean-square vorticity is at most $B$.
background
A FiniteVolumeProfile records a positive integer site count together with positive real amplitudes for maximum and root-mean-square vorticity. The profile obeys the finite-volume control relation that the maximum amplitude does not exceed the root-mean-square amplitude multiplied by the square root of the site count. This encodes the norm-equivalence control available on any finite RS lattice.
proof idea
This declaration is a one-line definition that packages the existential claim of a finite upper bound on the J-cost of the normalized ratio.
why it matters
LatticeFRC supplies the frc_exists_bound component of FRCBridgeCert, the structure that packages the complete logical closure from lattice cutoff to the conditional-completion route. The route proceeds from the finite recognition cost hypothesis through injection damping, direction constancy, and rigid rotation veto to regularity. It directly implements the bound promised by the phi-ladder cutoff result on RS lattices and feeds the abstract interface used in the Navier-Stokes regularity analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.