Astrophysics Pulsar Spindown From Jcost Pulsar Spindown Cert

What the certificate proves

A pulsar is a rotating neutron star that emits beams of radiation, and its spin-down is the gradual slowing of that rotation. Astronomers measure this through the period derivative, P-dot, and often quote a characteristic age tau = P / (2 P-dot). In the Recognition Science (RS) framework, the idea was to connect this age to a ladder built from the golden ratio phi, with a planned formula like tau = phi^k times tau_0, hoping to reach about 122 Gyr for millisecond pulsars.

What the machine-checked library of formal theorems actually proves is narrower. It defines a cost function on real numbers, domainCost(m, e) = Jcost(m / e), where Jcost is the framework's forced cost function. The certificate PulsarSpindownCert then bundles three proved facts: the cost is zero when m equals e, the cost is nonnegative for positive inputs, and the threshold phi - 3/2 is positive. These are general properties of the cost function, not statements about pulsars.

The library's own documentation is explicit on this point. The module proves nothing specific to pulsar spin-down because the definition of domainCost never references a pulsar, a period, or a spin-down rate. The pulsar formula appears only in a research note, a record of where the idea was meant to go. The same three general facts are stated once, universally quantified, in a shared template module, and this pulsar file is one of 2383 siblings that reuse that template verbatim.

What would make this a theorem about pulsars is a definition of m and e in the subject's own terms, connecting them to period and period derivative. That step is missing. The certificate is therefore a valid piece of mathematics about the cost function, but it does not establish any empirical claim about pulsars, their ages, or their spin-down rates.

theorem cert_inhabited : Nonempty PulsarSpindownCert := ⟨cert⟩

theorem domainCost_at_eq (r : ℝ) (h : r ≠ 0) : domainCost r r = 0 := by
  unfold domainCost; rw [div_self h]; exact Jcost_unit0

theorem domainCost_nonneg (m e : ℝ) (hm : 0 < m) (he : 0 < e) : 0 ≤ domainCost m e := by
  unfold domainCost; exact Jcost_nonneg (div_pos hm he)

theorem canonicalThreshold_pos : 0 < canonicalThreshold := by
  unfold canonicalThreshold; linarith [phi_gt_onePointFive]

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

What this page does not claim

Does not establish any empirical claim about pulsar ages or spin-down rates. Does not derive the characteristic age formula tau = phi^k times tau_0 from the cost function. Does not connect the golden ratio phi to any measured pulsar property.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Astrophysics/PulsarSpindownFromJCost.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: