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)
77theorem observational_regime_covered :
78 linearized_covers_observational = true := by decide
proof body
Term-mode proof.
79
80/-! ## CMS Regularity Conditions
81
82The Cheeger-Muller-Schrader theorem requires:
831. Uniform edge length bounds (ratio bounded)
842. Non-degeneracy of simplices (minimum dihedral angle bounded)
853. Bounded topology (genus bounded)
86
87The φ-lattice satisfies all three by construction. -/
88
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (10)
Lean names referenced from this declaration's body.
-
all
in IndisputableMonolith.Aesthetics.NarrativeGeodesic
decl_use
-
all
in IndisputableMonolith.Anthropology.KinshipGraphCohomology
decl_use
-
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
-
all
in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy
decl_use
-
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
-
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
-
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
-
linearized_covers_observational
in IndisputableMonolith.Gravity.NonlinearReggeProof
decl_use
-
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
-
all
in IndisputableMonolith.Musicology.ModalPreferenceFromPhi
decl_use