BernsteinBound
BernsteinBound records a positive bandwidth Ω taken from the recognition bandwidth definition together with the equality that sets the derivative bound to 2πΩ. Analysts replacing the Bernstein finite-sum axiom with an explicit constant in Recognition Science would cite this record. The declaration is a plain structure definition containing no lemmas or computational steps.
claimLet Ω > 0 be a bandwidth. A Bernstein bound consists of Ω together with the equality that the derivative bound equals 2πΩ.
background
The module supplies the structural framework for Bernstein's inequality on bandlimited functions, aiming to replace three axioms (pointwise derivative bound, finite trigonometric sum bound, and far-field zero-free region) with Mathlib proofs. Upstream, bandwidth is defined as the maximum recognition events per unit time allowed by the holographic bound: area divided by (4 planckArea ⋅ k_R ⋅ eightTickCadence), where k_R = ln(φ). The theorem bandwidth_pos shows this quantity is positive for positive area.
proof idea
The declaration is a structure definition that directly assembles the four fields: the bandwidth value, its positivity witness, the derivative bound real number, and the equality relating them. No lemmas are invoked; it is a pure record constructor.
why it matters in Recognition Science
BernsteinBound supplies the concrete derivative bound value consumed by the downstream theorem bernstein_bound_pos, which proves positivity of that bound. It fills the finite trigonometric sum case in the module's replacement of the bernstein_inequality_finite_axiom. Within the Recognition framework it links the holographic bandwidth (derived from the T0-T8 forcing chain) to derivative control for bandlimited functions.
scope and limits
- Does not prove Bernstein's inequality for general bandlimited functions.
- Does not address the far-field zero-free region axiom.
- Does not compute explicit numerical values for given areas.
- Applies only to the finite trigonometric polynomial setting.
formal statement (Lean)
59structure BernsteinBound where
60 bandwidth : ℝ
61 bandwidth_pos : 0 < bandwidth
62 derivative_bound : ℝ
63 bound_eq : derivative_bound = 2 * Real.pi * bandwidth
64