structure
definition
SpectrumFalsifier
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Cosmology.PrimordialSpectrum on GitHub at line 235.
browse module
All declarations in this module, on Recognition.
explainer page
formal source
232 1. n_s has no φ-connection
233 2. r contradicts (φ-1)⁴ prediction
234 3. Large non-Gaussianity found -/
235structure SpectrumFalsifier where
236 ns_no_phi : Prop
237 r_contradicts : Prop
238 large_nongaussianity : Prop
239 falsified : ns_no_phi ∧ r_contradicts → False
240
241end PrimordialSpectrum
242end Cosmology
243end IndisputableMonolith