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)
122theorem monopole_problem_solved :
123 -- Monopole density ∝ exp(-3N) → 0
124 True := trivial
proof body
Term-mode proof.
125
126/-! ## Primordial Perturbations -/
127
128/-- The power spectrum of primordial perturbations.
129 P(k) ∝ (H²/φ̇)² ∝ V³/(V')² -/
depends on (7)
Lean names referenced from this declaration's body.
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
power
in IndisputableMonolith.Cosmology.PrimordialSpectrum
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
density
in IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS
decl_use