lattice_regular_via_direction_constancy
plain-language theorem explainer
lattice_regular_via_direction_constancy shows that lattice FRC on any finite-volume profile is enough to close an arbitrary conditional completion route to regularity for that profile. Researchers formalizing Navier-Stokes regularity via Recognition Science lattices would cite this bridge result. The proof is a one-line wrapper that applies close_conditional_loop after instantiating the FRC premise with frc_holds_on_RS_lattice.
Claim. Let $R$ be a conditional completion route on finite-volume profiles and let $P$ be a finite-volume profile. If $R$ satisfies FRC on every profile $s$ for which RSLatticeFRC holds, then $R$ satisfies Regularity on $P$.
background
The module closes the logical loop between the Recognition Science lattice cutoff and the abstract conditional-completion route for Navier-Stokes regularity. A FiniteVolumeProfile packages a positive site count together with maximum and RMS vorticity values obeying the finite-volume control omegaMax ≤ sqrt(siteCount) * omegaRms. RSLatticeFRC asserts that the J-cost of the normalized ratio is bounded by sqrt(siteCount). ConditionalCompletionRoute is the structure containing the chain FRC implies InjectionDamping implies DirectionConstancy implies RigidRotationVeto implies Regularity, with the four implication fields made explicit. The upstream close_conditional_loop states that FRC on a profile yields Regularity via the full chain; frc_holds_on_RS_lattice proves RSLatticeFRC by finiteVolume_Jcost_bound.
proof idea
The term proof applies close_conditional_loop to the supplied route. It then supplies the required FRC premise by feeding the profile and the result of frc_holds_on_RS_lattice profile into the hypothesis hFRCBridge.
why it matters
This theorem supplies the final step inside frcBridgeCert, the packaged certificate that records frc_on_lattice, frc_exists_bound and the conditional_loop closure. It realizes the module goal of turning the lattice φ-ladder cutoff into an instance of the conditional route from the Navier-Stokes regularity paper. The construction sits inside the Recognition Science forcing chain, using the J-cost bounds that follow from the eight-tick octave and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.