TauZeroCert
plain-language theorem explainer
TauZeroCert packages the numerical band checks for the cortical resonance frequency 5φ together with the existence of a positive τ₀. Researchers calibrating RS predictions against EEG alpha rhythms or plasma control frequencies would reference this structure to assert the alignment. It is introduced as a plain record whose fields are the two interval statements and the tauZeroDefinition proposition. The structure carries no computational content and is populated downstream by direct field assignment.
Claim. A structure certifying that the cortical resonance frequency satisfies $8.05 < 5φ < 8.10$ and $7.5 < 5φ < 8.1$, together with the proposition that a positive real calibration scalar $τ_0$ exists.
background
In the Tau-Zero Calibrator module, τ₀ is the single calibration scalar that fixes the RS time unit, with the module predicting τ₀ ≈ 7.3 × 10^{-15} s. The definition corticalResonance5phi sets this frequency to 5φ, where φ is the self-similar fixed point from the forcing chain. tauZeroDefinition is the proposition ∃(τ₀ : ℝ), τ₀ > 0.
proof idea
The declaration is a structure definition that directly records the three required properties as fields. No lemmas are applied; the structure simply packages the interval inequalities on corticalResonance5phi and the existential statement from tauZeroDefinition.
why it matters
This structure is instantiated in the downstream definition tauZeroCert, which supplies concrete witnesses for the bands and the existence claim. It fills the role of certifying the numerical alignment between the RS-derived cortical resonance 5φ and observed EEG bands, as described in the module documentation. Within the Recognition framework it supports the calibration step that derives all Hz-scale predictions from τ₀ alone, linking to the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.