theorem proved term proof

`rs_predicts_core`

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

formal statement (Lean)

 148theorem rs_predicts_core :
 149    -- High-density ledger interactions → core, not cusp
 150    True := trivial

proof body

Term-mode proof.

 151
 152/-! ## MOND Alternative -/
 153
 154/-- Modified Newtonian Dynamics (MOND):
 155
 156    At low accelerations (a < a₀ ~ 10⁻¹⁰ m/s²):
 157    The effective gravitational force is enhanced:
 158    F = ma√(a/a₀) instead of F = ma
 159
 160    This gives flat rotation curves WITHOUT dark matter!
 161
 162    But: MOND fails for galaxy clusters and CMB. -/

depends on (15)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
F in IndisputableMonolith.Physics.AnchorPolicy decl_use
F in IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation decl_use
density in IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS decl_use
F in IndisputableMonolith.Pipelines decl_use