Astrophysics Pulsar Period Rs

Pulsar periods

A pulsar is a rotating neutron star that beams radio waves like a lighthouse; each sweep arrives at Earth as a precise pulse. The fastest known pulsars spin about 700 times per second, while older ones take several seconds per turn. In Recognition Science, a framework that models physical structure through a forced cost of recognition, the research note proposes that pulsar periods follow T = phi^(-k) seconds, where phi is the golden ratio, about 1.618. For k = 1, that gives 0.618 seconds, a typical pulsar period; for k = 10, it gives 0.00813 seconds, about 8 milliseconds, in the millisecond pulsar range. The note also checks the Crab pulsar, whose 0.033-second period sits near phi^(-1) = 0.618? The arithmetic is loose, and the note itself is a research idea, not a result.

The machine-checked library of formal theorems proves three general facts about the cost function J(x) = (x + 1/x)/2 - 1, evaluated at the ratio m/e. First, when m equals e, the cost is zero: J(1) = 0. Second, for positive m and e, the cost is never negative. Third, the threshold phi - 3/2 is positive, meaning phi exceeds 1.5. These three facts assemble into a certificate structure, a bundle of properties that any subject-specific model could reuse. The library proves the certificate exists, but it proves nothing specific to pulsars, because the cost is defined as J(m/e) without saying what m and e mean for a pulsar. The docstring states this plainly: the pulsar paragraph is a research note recording where the idea was meant to go, not a theorem.

In plain language, the library establishes that the cost function behaves sensibly: equal inputs cost nothing, positive inputs never cost a negative amount, and the golden ratio clears a small threshold. What it does not establish is that pulsar periods actually follow phi powers. That would require defining m and e in pulsar terms, such as a mass or energy ratio, and then checking the prediction against measured periods. Until that definition exists, the pulsar connection remains a hypothesis with a named falsifier: a measured pulsar period that does not match any phi^(-k) value within measurement error would refute the proposed scaling.

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]

theorem cert_inhabited : Nonempty PulsarPeriodCert := ⟨cert⟩

noncomputable def cert : PulsarPeriodCert where
  cost_at_eq := domainCost_at_eq
  cost_nonneg := domainCost_nonneg
  threshold_pos := canonicalThreshold_pos

What this page does not claim

This module does not prove that pulsar periods actually follow golden-ratio powers. The Crab pulsar value is not established as a match; the note's arithmetic is loose.

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/Pulsar_Period_RS.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: