NumericalMethod
plain-language theorem explainer
This inductive type enumerates the five canonical numerical methods in Recognition Science as Newton's method, Euler integration, Runge-Kutta, Gaussian elimination, and the fast Fourier transform. Researchers certifying numerical solvers against the RS configDim D=5 would cite the type when verifying cardinality. The declaration proceeds by direct inductive construction with derived Fintype to support automatic count computation.
Claim. Let $M$ be the inductive type generated by the five constructors corresponding to Newton's method, Euler integration, Runge-Kutta methods, Gaussian elimination, and the fast Fourier transform. Then $|M|=5$.
background
The module on Numerical Analysis from RS states that five canonical numerical methods correspond to the configuration dimension D=5. These methods are Newton's method for root finding, Euler integration for ordinary differential equations, Runge-Kutta for higher-order accuracy, Gaussian elimination for linear systems, and the fast Fourier transform for spectral work. The module further records that DFT-8 is canonical with eight modes (2^3 from the eight-tick octave) and that the FFT implementation uses 24 operations per tick (3 times 8).
proof idea
The declaration is a direct inductive definition that introduces five constructors and derives the instances DecidableEq, Repr, BEq, and Fintype. No separate proof body exists; the Fintype instance is generated automatically by the deriving clause.
why it matters
This definition supplies the enumeration required by the NumericalAnalysisCert structure, which asserts five_methods as Fintype.card NumericalMethod =5, eight_modes=8, and fft_ops=24. It anchors the RS numerical toolkit to the eight-tick octave (T7) and the derivation of three spatial dimensions (T8), confirming the fast Fourier transform as the O(N log N) realization of DFT-8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.