IndisputableMonolith.NavierStokes.FourierExtraction
The module establishes composed extraction at step m for Fourier columns in the Navier-Stokes setting, guaranteeing convergence from 0 to m. Analysts of the Recognition Science approach to fluid dynamics would reference these convergence tools. It builds via a collection of monotonicity and limit lemmas on strict mono functions and bounded sequences.
claimComposed extraction $CE_m$ ensures convergence of Fourier columns indexed $0$ through $m$.
background
Located in the NavierStokes domain, the module introduces convergence infrastructure for Fourier extraction. Key definitions include CE as the composed extraction operator, CL and LE as companion limit and extraction maps, with base cases CE_zero and CE_succ. Supporting results cover composition of strict monotonic functions with limits, identity bounds under strict mono, and convergence of bounded subsequences, plus monotonicity and convergence statements.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the extraction machinery required for the Navier-Stokes Fourier analysis within Recognition Science. It supports parent results on fluid equation solutions by ensuring column convergence at each step m.
scope and limits
- Does not address full Navier-Stokes solvability.
- Does not incorporate the J-cost or phi-ladder directly.
- Does not prove existence of solutions, only convergence of extractions.
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