 294The complete Earth-Brain Resonance theorem packages all results. -/
 295
 296/-- Provenance label separating forced results from empirical predictions. -/
 297inductive Provenance where
 298  | forced     : Provenance
 299  | empirical  : Provenance
 300
 301/-- The complete Earth-Brain Resonance certificate. -/
 302structure EarthBrainResonanceCert where
 303  -- FORCED (from RCL alone: T6 forces φ, T8 forces D=3)
 304  formula_zero_params   : ∀ n, schumannRS n = (4 * (n : ℝ) - 1) * phi + 3
 305  fundamental_is_3phi2  : schumannRS 1 = 3 * phi ^ 2
 306  fundamental_is_phi4p1 : schumannRS 1 = phi ^ 4 + 1
 307  harmonic_spacing      : ∀ n, schumannRS (n + 1) - schumannRS n = 4 * phi
 308  strictly_increasing   : ∀ m n : ℕ, m < n → schumannRS m < schumannRS n
 309  forced_label          : Provenance
 310  -- EMPIRICAL PREDICTIONS (Earth's radius is contingent)
 311  match_h1 : |schumannRS 1 - 7.83| < 0.03
 312  match_h2 : |schumannRS 2 - 14.3| < 0.04
 313  match_h3 : |schumannRS 3 - 20.8| < 0.01
 314  match_h4 : |schumannRS 4 - 27.3| < 0.03
 315  match_h5 : |schumannRS 5 - 33.8| < 0.06
 316  worst_case_bound : |schumannRS 1 - 7.83| < 0.06 ∧
 317                     |schumannRS 2 - 14.3| < 0.06 ∧
 318                     |schumannRS 3 - 20.8| < 0.06 ∧
 319                     |schumannRS 4 - 27.3| < 0.06 ∧
 320                     |schumannRS 5 - 33.8| < 0.06
 321  eeg_coverage : inFreqBand (schumannRS 1) 4 8 ∧
 322                 inFreqBand (schumannRS 2) 13 30 ∧
 323                 inFreqBand (schumannRS 3) 13 30 ∧
 324                 inFreqBand (schumannRS 4) 13 30 ∧
 325                 inFreqBand (schumannRS 5) 30 100
 326  empirical_label : Provenance
 327

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.