recognition /
Papers /
Papers.DraftV1 /
explainer
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)
148 noncomputable def apsidalAngle (D : ℕ) : ℝ :=
proof body
Definition body.
149 (2 * Real.pi) / Real.sqrt (4 - (D : ℝ))
150
151 /-- A direct formalization of the paper's last step:
152 `Δθ = 2π` holds iff `D=3` for the substituted closed-form apsidal angle. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (12)
Lean names referenced from this declaration's body.
of
in IndisputableMonolith.Astrophysics.NucleosynthesisTiers
decl_use
last
in IndisputableMonolith.Chain
decl_use
step
in IndisputableMonolith.Complexity.CellularAutomata
decl_use
of
in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization
decl_use
A
in IndisputableMonolith.Foundation.IntegrationGap
decl_use
of
in IndisputableMonolith.Foundation.PhiForcingDerived
decl_use
of
in IndisputableMonolith.Foundation.SpectralEmergence
decl_use
for
in IndisputableMonolith.Foundation.UniversalForcingSelfReference
decl_use
of
in IndisputableMonolith.Information.PhysicsComplexityStructure
decl_use
A
in IndisputableMonolith.Masses.Anchor
decl_use
A
in IndisputableMonolith.Modal.Actualization
decl_use
last
in IndisputableMonolith.Recognition
decl_use