ConditionalCompletionRoute
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not supply concrete definitions or existence proofs for FRC on any specific lattice.
- Does not prove the PDE content of the implication steps; they remain external hypotheses.
- Does not address numerical values of constants such as phi or alpha.
- Does not extend the chain beyond the five listed properties.
formal statement (Lean)
107structure ConditionalCompletionRoute (α : Type) where
108 FRC : α → Prop
109 InjectionDamping : α → Prop
110 DirectionConstancy : α → Prop
111 RigidRotationVeto : α → Prop
112 Regularity : α → Prop
113 frc_to_injectionDamping : ∀ a, FRC a → InjectionDamping a
114 injectionDamping_to_directionConstancy : ∀ a, InjectionDamping a → DirectionConstancy a
115 directionConstancy_to_rigidRotationVeto : ∀ a, DirectionConstancy a → RigidRotationVeto a
116 rigidRotationVeto_to_regularity : ∀ a, RigidRotationVeto a → Regularity a
117
118/-- Once FRC is known on the lattice, any conditional-completion route closes. -/