close_conditional_loop
plain-language theorem explainer
Once FRC holds on a lattice element a, the conditional-completion route yields regularity. Navier-Stokes researchers working with Recognition Science lattices cite this result to close the bridge from the phi-ladder cutoff to the regularity conclusion. The proof is a direct term chain that applies the four implication functions inside the route structure in sequence.
Claim. Let $R$ be an abstract conditional-completion route on a type $α$, equipped with predicates FRC, InjectionDamping, DirectionConstancy, RigidRotationVeto, Regularity together with the four implication maps connecting them in order. For any element $a:α$, if FRC($a$) holds then Regularity($a$) holds.
background
The Lattice FRC Bridge module closes the logical loop between the lattice φ-ladder cutoff result and the conditional-completion route from the Navier-Stokes regularity paper. On a finite RS lattice the normalized vorticity ratio ω_max/ω_rms is automatically finite-volume controlled, supplying a finite recognition-cost bound that can be fed into any abstract route of the form FRC → InjectionDamping → DirectionConstancy → RigidRotationVeto → Regularity. The module isolates the exact logical bridge while leaving the PDE-heavy steps external.
proof idea
The term-mode proof constructs three intermediate facts by successive application of the route's implication functions: frc_to_injectionDamping yields InjectionDamping from FRC, injectionDamping_to_directionConstancy yields DirectionConstancy, and directionConstancy_to_rigidRotationVeto yields RigidRotationVeto; the final exact step applies rigidRotationVeto_to_regularity.
why it matters
The theorem is invoked by lattice_regular_via_direction_constancy to conclude that the lattice FRC theorem is enough to instantiate the conditional route and obtain regularity. It supplies the explicit logical bridge described in the module doc-comment between the lattice φ-ladder cutoff and the conditional-completion route of the Navier-Stokes regularity paper, connecting the Recognition Science phi-ladder cutoff to regularity claims in D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.