pith. machine review for the scientific record. sign in
def definition def or abbrev

earthBrainResonance_forced

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 341def earthBrainResonance_forced : EarthBrainResonanceCert where
 342  formula_zero_params   := fun _ => rfl

proof body

Definition body.

 343  fundamental_is_3phi2  := fundamental_eq_D_phi_sq
 344  fundamental_is_phi4p1 := fundamental_eq_phi4_plus_1
 345  harmonic_spacing      := spacing_eq
 346  strictly_increasing   := schumannRS_strictMono
 347  forced_label          := .forced
 348  match_h1              := harmonic1_matches
 349  match_h2              := harmonic2_matches
 350  match_h3              := harmonic3_matches
 351  match_h4              := harmonic4_matches
 352  match_h5              := harmonic5_matches
 353  worst_case_bound      := all_harmonics_match
 354  eeg_coverage          := schumann_spans_eeg_bands
 355  empirical_label       := .empirical
 356
 357/-! ## Part IX: Falsification Criteria -/
 358

depends on (12)

Lean names referenced from this declaration's body.