IndisputableMonolith.Analysis.BernsteinInequality
The BernsteinInequality module supplies the analytic scaffolding for frequency-limited functions in Recognition Science. It introduces predicates and bounds that relate derivative growth to a frequency parameter scaled by the RS time quantum. The structure consists of auxiliary amplitude-sum definitions and a certificate object that together encode the classical Bernstein relation.
claimFor a function $f$ that is FrequencyBounded with frequency parameter $ω$, the BernsteinBound asserts that the amplitude sum of $f'$ is at most $ω$ times the amplitude sum of $f$, witnessed by a BernsteinCert.
background
The module sits in the Analysis domain and imports the RS time quantum $τ_0 = 1$ tick from Constants. FrequencyBounded encodes the restriction that the function's spectral support lies below a cutoff derived from $τ_0$. BernsteinBound is the inequality that controls the derivative amplitude sum by the product of frequency and the original amplitude sum. The certificate BernsteinCert packages the data needed to verify the bound without external Fourier machinery.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the frequency-control tools required by later analytic steps in the Recognition framework. It prepares bounds that can be applied to signals propagating through the eight-tick octave and the phi-ladder, although no downstream declarations currently reference it.
scope and limits
- Does not treat continuous spectra or non-band-limited cases.
- Does not supply explicit constants for the alpha band or G.
- Does not address multi-dimensional spatial derivatives.
- Does not connect directly to the J-cost or defectDist predicates.