NumericalAnalysisCert
plain-language theorem explainer
NumericalAnalysisCert packages the alignment of five canonical numerical methods with the eight-tick octave and three-dimensional structure by requiring the cardinality of NumericalMethod to be five, dft8Modes to equal eight, and fftOps to equal twenty-four. A physicist implementing RS-derived discretizations would cite it to confirm that DFT-8 and its fast transform match the period 2^3 and the 8 times 3 operation count. The declaration is realized as a bare structure whose fields are populated directly by the upstream constants and the Fintyp
Claim. A structure $C$ such that the finite cardinality of the set of canonical numerical methods equals five, the number of DFT-8 modes equals eight, and the number of FFT operations per tick equals twenty-four.
background
The module identifies five canonical numerical methods (Newton, Euler integration, Runge-Kutta, Gaussian elimination, FFT) with configuration dimension D equal to five; these are collected in the inductive type NumericalMethod. Upstream, dft8Modes is defined as 2^3 and fftOps as 8 times 3, encoding the relation that the fast Fourier transform performs twenty-four operations per tick for the eight-mode case. The module states that DFT-8 is the canonical numerical algorithm with eight modes equal to 2^D and that FFT achieves O(N log N) complexity matching eight times three operations per tick.
proof idea
The declaration is a structure definition. Its first field asserts that the Fintype cardinality of NumericalMethod equals five. The second field equates eight_modes with the constant dft8Modes. The third field equates fft_ops with the constant fftOps. No lemmas or tactics are invoked beyond these direct assignments.
why it matters
NumericalAnalysisCert supplies the certificate consumed by numericalAnalysisCert, closing the numerical-analysis layer of the Recognition Science framework. It ties the five methods to configDim D equals five and the eight modes to the eight-tick octave (T7, period 2^3). The twenty-four operations follow from the three spatial dimensions (T8). The structure introduces no new axioms and completes the numerical facts required by the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.