ConditionalCompletionRoute
plain-language theorem explainer
ConditionalCompletionRoute encodes an abstract chain of implications from finite recognition cost on a profile to Navier-Stokes regularity. Workers on the Recognition Science lattice-to-PDE bridge cite this structure to keep the logical skeleton separate from the heavy analysis. The definition is a direct packaging of the five predicates and four implications with no additional proof content.
Claim. A structure on a type $α$ consisting of five predicates $FRC, InjectionDamping, DirectionConstancy, RigidRotationVeto, Regularity : α → Prop$ together with the four implications $∀a, FRC(a) → InjectionDamping(a)$, $∀a, InjectionDamping(a) → DirectionConstancy(a)$, $∀a, DirectionConstancy(a) → RigidRotationVeto(a)$, and $∀a, RigidRotationVeto(a) → Regularity(a)$.
background
The 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 feeds into the route FRC → injection damping → direction constancy → rigid rotation veto → regularity. The PDE-heavy steps remain external; only the exact logical bridge is formalized here.
proof idea
The declaration is the direct definition of the structure; no tactics or lemmas are applied.
why it matters
The structure supplies the hypothesis used by close_conditional_loop, FRCBridgeCert, LatticeRegularityCertificate, and lattice_regular_via_direction_constancy. It isolates the logical bridge from the lattice cutoff theorem (RSLatticeFRC) to the conditional paper, allowing the Recognition Science eight-tick octave and phi-ladder cutoff to reach regularity without embedding the full PDE argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.