tauZeroCert
plain-language theorem explainer
tauZeroCert assembles a single record bundling the alpha-band membership of 5φ, its fifth-mode band membership, and the existence of the RS time calibration scalar τ₀. Researchers deriving cortical or plasma frequency predictions from Recognition Science constants would cite the record to invoke the complete calibration check at once. The definition is a direct structure constructor that references the three upstream theorems without further reasoning.
Claim. The TauZeroCert record asserts that the cortical resonance frequency satisfies $8.05 < 5φ < 8.10$, the fifth-mode band condition $7.5 < 5φ < 8.1$, and that the calibration scalar τ₀ exists as a positive real.
background
In the Tau-Zero Calibrator module, τ₀ is the single scalar fixing the RS time unit, with the module claiming all Hz-scale predictions follow from τ₀ alone. The quantity corticalResonance5phi stands for the frequency 5φ (in units normalized so τ₀ = 1), whose bounds are checked against experimental alpha and fifth-mode bands. The upstream theorem corticalResonance_band proves 5φ lies in (8.05, 8.10) by direct comparison with the known interval for φ. The companion theorem corticalResonance_fifth_mode_band places 5φ inside (7.5, 8.1) using looser bounds on φ. The theorem tauZero_exists exhibits the unit value 1 as witness for tauZeroDefinition.
proof idea
The definition is a one-line structure constructor. It populates the cortical_band field by direct reference to the theorem corticalResonance_band, the fifth_mode_band field by reference to corticalResonance_fifth_mode_band, and the tau0_exists field by reference to tauZero_exists.
why it matters
This definition supplies a single reusable certificate for the τ₀ calibration step. It collects the numerical checks required by the module documentation for cortical resonance alignment and the trivial existence of the time unit. In the Recognition Science framework it supports the claim that τ₀ alone determines all Hz-scale predictions (Schumann resonances, ALEXIS plasma control) once the calibration is fixed, consistent with the module's uniqueness statement. No downstream theorems inside the repository currently depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.