def definition def or abbrev

`reciprocalPrimeSum`

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

formal statement (Lean)

 239noncomputable def reciprocalPrimeSum (n : ℕ) : ℝ :=

proof body

Definition body.

 240  n.factorization.sum fun p k => (k : ℝ) / (p : ℝ)
 241
 242/-- Per-summand identity: each prime-power contribution to `c(n)` decomposes
 243    into half of `k·p`, half of `k/p`, minus `k`.  Used to derive the
 244    closed-form decomposition below. -/

depends on (11)

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
identity in IndisputableMonolith.Foundation.ObserverForcing decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
half in IndisputableMonolith.QFT.SpinStatistics decl_use
half in IndisputableMonolith.RecogSpec.Core decl_use
identity in IndisputableMonolith.RRF.Foundation.VantageCategory decl_use
half in IndisputableMonolith.Support.RungFractions decl_use