close_conditional_loop
plain-language theorem explainer
If a conditional completion route satisfies the finite recognition cost property at an element a, then the route yields regularity at a. Navier-Stokes regularity researchers using the recognition-science lattice cutoff would cite this to close the bridge from finite-volume FRC to the PDE conclusion. The proof is a term-mode chain that applies the four implication fields of the route in sequence.
Claim. Let $R$ be a conditional completion route on a type $X$. For any element $a$ in $X$, if $R$ satisfies the finite recognition cost condition at $a$, then $R$ satisfies the regularity condition at $a$.
background
The ConditionalCompletionRoute structure isolates the logical skeleton of a regularity argument: it packages four predicates (FRC, InjectionDamping, DirectionConstancy, RigidRotationVeto, Regularity) together with the four implication maps that chain them. The module sits between the lattice cutoff result (finite RS lattice gives bounded normalized vorticity ratio and therefore finite J-cost) and the external PDE steps that would discharge the intermediate predicates. Upstream, the IntegrationGap.A and Masses.Anchor.A supply the active-edge count per tick that enters the phi-ladder cutoff; Modal.Actualization.A supplies the minimization operator that defines the recognition cost itself.
proof idea
The term proof introduces three intermediate hypotheses by applying the route's implication fields in order: frc_to_injectionDamping, injectionDamping_to_directionConstancy, directionConstancy_to_rigidRotationVeto. It then applies the final field rigidRotationVeto_to_regularity to obtain the target regularity statement.
why it matters
This theorem supplies the final logical step that lets the lattice FRC theorem instantiate any abstract conditional route, thereby feeding the downstream result lattice_regular_via_direction_constancy. It closes the explicit bridge described in the module doc-comment between the phi-ladder cutoff on a finite RS lattice and the regularity hypothesis used by the conditional Navier-Stokes paper. The construction relies on the eight-tick octave and D=3 spatial dimensions already fixed in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.