IndisputableMonolith.Analysis.BernsteinInequality
The BernsteinInequality module defines frequency-bounded functions and their derivative bounds in Recognition Science. It supplies FrequencyBounded, BernsteinBound, amplitude sums, and BernsteinCert using the time quantum from Constants. The module consists of definitions plus elementary nonnegativity lemmas.
claimFrequencyBounded$(f,\omega)$ asserts a function $f$ has frequency support at most $\omega$ (in units with $\tau_0=1$). BernsteinBound$(f,\omega)$ states $\|f'\|\leq\omega\|f\|$. BernsteinCert witnesses the bound via amplitude_sum and derivative_amplitude_sum.
background
The module sits in the Analysis domain and imports the RS time quantum $\tau_0=1$ tick from IndisputableMonolith.Constants. It introduces FrequencyBounded, amplitude_sum, derivative_amplitude_sum, and derivative_bounded_by_frequency to set up the classical Bernstein inequality inside RS-native units.
No module-level doc comment is supplied. The sibling declarations establish nonnegativity of the bounds and existence of a certificate, all resting on the imported constant.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the Bernstein inequality primitives that feed into parent theorems on wave propagation and frequency analysis within the Recognition framework. It fills the analysis layer required before mass-ladder or J-cost constructions that rely on bounded derivatives.
scope and limits
- Does not derive the bound from the Recognition Composition Law.
- Does not incorporate the phi-ladder or mass formula.
- Does not treat non-frequency-bounded or infinite-bandwidth cases.
- Does not address spatial dimensions or the eight-tick octave.