FRCBridgeCert
plain-language theorem explainer
The lattice FRC bridge certificate packages three properties for finite-volume vorticity profiles on RS lattices: the strong J-cost bound by sqrt(siteCount), the weak existence of a finite bound, and the conditional loop that feeds lattice FRC into any abstract completion route to obtain regularity. Researchers formalizing Navier-Stokes regularity inside Recognition Science cite this to certify closure between the phi-ladder cutoff and the conditional hypothesis. The declaration is a structure definition that directly assembles three sibling le
Claim. Let $s$ be a finite-volume vorticity profile. The certificate asserts $J(ω_{max}/ω_{rms}) ≤ √(siteCount)$, the existence of a finite $B$ with $J(ω_{max}/ω_{rms}) ≤ B$, and that any conditional-completion route whose FRC predicate holds on all such profiles yields regularity for the given profile.
background
A FiniteVolumeProfile packages a finite window on the RS lattice with siteCount, omegaMax, omegaRms, and the finiteVolumeControl inequality omegaMax ≤ sqrt(siteCount) * omegaRms. RSLatticeFRC s asserts that the J-cost of the normalized ratio is at most sqrt(siteCount), while LatticeFRC s only requires some finite bound B. The ConditionalCompletionRoute structure isolates the PDE steps by chaining FRC to InjectionDamping to DirectionConstancy to RigidRotationVeto to Regularity.
proof idea
The declaration is a structure definition that directly assembles the three properties from sibling lemmas: frc_holds_on_RS_lattice for the strong bound, frc_holds_on_RS_lattice_exists for the weak bound, and lattice_regular_via_direction_constancy for the conditional loop. No tactics are used; it is a pure packaging of the upstream results into a single certificate object.
why it matters
This structure earns its place by providing the explicit logical bridge that feeds the lattice FRC results into the conditional-completion route, thereby closing the loop to regularity. It is used by the frcBridgeCert definition, which instantiates the certificate with the concrete lattice lemmas. In the Recognition Science framework it connects the phi-ladder cutoff and J-cost bound on normalized vorticity ratios to the Navier-Stokes regularity problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.