IndisputableMonolith.NavierStokes.FourierExtraction
The FourierExtraction module composes extraction steps at arbitrary m to force convergence of the first m Fourier columns in a Navier-Stokes setting. Researchers deriving fluid equations from the Recognition forcing chain would cite it when assembling mode-by-mode limits. The module collects a chain of monotonicity and tendsto lemmas to build the extraction inductively.
claimComposed extraction at step $m$ ensures Fourier columns indexed $0$ through $m$ converge.
background
The module lives inside the NavierStokes domain of Recognition Science and imports only Mathlib for analysis. It introduces tendsto_comp_strictMono (composition of strict monotonic maps with limits), strictMono_id_le (identity is strictly monotone), bounded_subseq_tendsto (bounded sequences admit convergent subsequences), and the family CE, CL, LE together with their zero, succ, strictMono and conv_at variants. These supply the inductive scaffolding for column-wise convergence under the Recognition Composition Law.
proof idea
This is a definition module, no proofs. The structure assembles the listed monotonicity and limit lemmas into an inductive extraction that reaches any finite column index m.
why it matters in Recognition Science
The module supplies the convergence engine required by downstream Navier-Stokes claims that apply the unified forcing chain (T0-T8) and the Recognition Composition Law to fluid modes. It closes the gap between the phi-ladder and concrete Fourier extraction without invoking the mass formula or Berry threshold.
scope and limits
- Does not prove existence or uniqueness of Navier-Stokes solutions.
- Does not incorporate the phi-ladder mass formula or Berry creation threshold.
- Does not address the alpha inverse interval or G constant.
- Does not force spatial dimension D=3 inside this extraction.
declarations in this module (19)
-
theorem
tendsto_comp_strictMono -
theorem
strictMono_id_le -
theorem
bounded_subseq_tendsto -
def
CE -
def
CL -
def
LE -
theorem
CE_zero -
theorem
CE_succ -
theorem
LE_strictMono -
theorem
CE_strictMono -
theorem
LE_conv -
theorem
CE_conv_at -
theorem
CE_conv_le -
theorem
CE_factor -
def
D -
theorem
D_succ_gt -
theorem
D_strictMono -
theorem
D_converges -
theorem
nat_diagonal_extraction