numericalAnalysisCert
plain-language theorem explainer
This definition builds the numerical analysis certificate by supplying the three required fields from their respective count theorems. Researchers modeling discrete dynamics in Recognition Science would cite it to verify that the toolkit contains exactly five methods, eight DFT modes, and twenty-four FFT operations. The construction is a direct structure literal that references the decide lemmas for each equality.
Claim. The numerical analysis certificate is the structure satisfying $Fintype.card(NumericalMethod)=5$, $dft8Modes=8$, and $fftOps=24$.
background
The module states that five canonical numerical methods (Newton, Euler, Runge-Kutta, Gaussian elimination, Fast Fourier Transform) equal configDim D=5. DFT-8 is the canonical algorithm with 2^D modes, and FFT realizes it in O(8×3)=24 operations per tick. The upstream theorems establish the three equalities by direct computation: numericalMethodCount shows the method cardinality is five, dft8Modes_8 shows the mode count is eight, and fftOps_24 shows the operation count is twenty-four.
proof idea
The definition constructs the NumericalAnalysisCert structure by assigning the five_methods field to numericalMethodCount, the eight_modes field to dft8Modes_8, and the fft_ops field to fftOps_24. Each assignment pulls a one-line theorem proved by decide.
why it matters
This certificate supplies the concrete counts required by the Recognition Science forcing chain at T7, where the eight-tick octave and D=3 yield the 24-operation FFT. It closes the discrete approximation layer by confirming alignment with the five methods and 8×3 operations. No downstream uses appear yet, leaving open its invocation in a larger simulation theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.