ConditionalCompletionRoute
plain-language theorem explainer
This structure encodes the abstract chain FRC implies InjectionDamping implies DirectionConstancy implies RigidRotationVeto implies Regularity on an arbitrary type alpha. It is cited by any argument that obtains Navier-Stokes regularity from a lattice finite-recognition-cost theorem while leaving the PDE steps external. The declaration is a plain structure definition that makes the four implications explicit fields.
Claim. A conditional completion route on a type $alpha$ consists of predicates $FRC, InjectionDamping, DirectionConstancy, RigidRotationVeto, Regularity : alpha to Prop$ together with the four implications $FRC(a) implies InjectionDamping(a)$, $InjectionDamping(a) implies DirectionConstancy(a)$, $DirectionConstancy(a) implies RigidRotationVeto(a)$, and $RigidRotationVeto(a) implies Regularity(a)$ for every $a : alpha$.
background
The module closes the logical loop between the lattice phi-ladder cutoff result and the conditional-completion route from the Navier-Stokes regularity paper. On a finite RS lattice the normalized vorticity ratio omega_max / omega_rms is automatically finite-volume controlled, supplying a finite recognition-cost bound that feeds the chain FRC to regularity. The structure isolates the heavy PDE part while making the bridge explicit. Upstream dependencies supply generic collision-free and edge-length statements that discharge as tautologies or named hypotheses.
proof idea
The declaration is a structure definition with no proof body. It simply lists the five predicates as fields and records the four implication arrows as additional fields. No lemmas or tactics are invoked; the content is the explicit interface itself.
why it matters
The structure supplies the skeleton instantiated by close_conditional_loop to obtain regularity once lattice FRC is known. It is used directly by FRCBridgeCert, LatticeRegularityCertificate, and lattice_regular_via_direction_constancy. In the Recognition framework it formalizes the exact logical bridge from the phi-ladder cutoff to the conditional paper's hypothesis, keeping the analysis external while connecting to the eight-tick octave and D=3 landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.