close_conditional_loop
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the FRC predicate on any concrete lattice profile.
- Does not discharge the PDE content inside the four implication maps.
- Does not extend to infinite-volume or non-lattice settings.
- Does not quantify over all possible routes; only those packaged as ConditionalCompletionRoute.
Lean usage
apply close_conditional_loop routeformal statement (Lean)
119theorem close_conditional_loop {α : Type} (route : ConditionalCompletionRoute α) {a : α}
120 (hFRC : route.FRC a) : route.Regularity a := by
proof body
Term-mode proof.
121 have hID : route.InjectionDamping a := route.frc_to_injectionDamping a hFRC
122 have hDC : route.DirectionConstancy a :=
123 route.injectionDamping_to_directionConstancy a hID
124 have hRR : route.RigidRotationVeto a :=
125 route.directionConstancy_to_rigidRotationVeto a hDC
126 exact route.rigidRotationVeto_to_regularity a hRR
127
128/-- A regularity certificate obtained by running the conditional route on a
129finite RS lattice profile. -/