NoPersistentNullAlignmentHypothesis
plain-language theorem explainer
The structure encodes an abstract implication: existence of c > 0 such that every large tail strain event at positive scales epsilon and r forces a hit event. Researchers proving Navier-Stokes regularity under the RM2U closure would cite it to enforce the spec-layer non-parasitism gate. It is introduced directly as a structure definition that packages the existential quantifier and universal implication without further reduction.
Claim. There exists a constant $c > 0$ such that for all $ε > 0$ and $r > 0$, if a large tail strain event occurs at scales $ε, r$ then a hit event occurs at those scales.
background
The RM2U.NonParasitism module isolates the single hard non-parasitism statement as a hypothesis so the remainder of the RM2U to RM2 pipeline stays clean. Non-parasitism is the condition that the tail-flux or boundary term at infinity vanishes for the relevant ℓ=2 coefficient. The structure supplies the spec-layer version of no persistent null alignment: a large tail strain event forces nontrivial interaction with the vorticity direction and thereby avoids the null-eigenvector cone on a time-thick top band set.
proof idea
This is a structure definition whose sole field directly states the existential quantifier over c together with the universal quantification and implication between the two event predicates. No lemmas are invoked and no tactics are used; the declaration is the primitive packaging of the hypothesis.
why it matters
It supplies the single hard gate required by the RM2U.NonParasitism module, allowing the rest of the pipeline to proceed without circularity. The declaration fills the spec-layer requirement that non-parasitism be expressed as an abstract implication between tail events and hit events. In the Recognition Science framework it supports the forcing chain (T0-T8) and the derivation of Navier-Stokes regularity by excluding persistent null alignments that would otherwise permit parasitic solutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.