Cosmology Reionization Endpoint3 From Jcost Reion End3 Cert

The certificate's scope

Reionization is the epoch, roughly a billion years after the Big Bang, when radiation from the first stars and galaxies split neutral hydrogen into protons and electrons, letting ultraviolet light travel freely. The period's end is a target for observation, with the Planck mission's measurements placing it at a redshift z of about 5.5 to 6. A redshift near 6 corresponds to a universe about a billion years old. This is the classical picture, established by telescope surveys and satellite data, not by any single theoretical certificate.

In Recognition Science, a ledger (a discrete record of events) assigns a cost (a forced penalty) to a ratio of two quantities. The framework's machine-checked library of formal theorems proves three general facts about this cost function. First, the cost is zero when the two quantities are equal. Second, the cost is never negative for positive inputs. Third, a particular threshold value, the golden ratio minus 1.5, is positive. These three statements are bundled into a structure called ReionEnd3Cert, and the library proves such a certificate exists.

The certificate's name suggests a connection to reionization, but the library's own documentation is explicit: the certificate proves nothing specific to that subject. The cost function is defined as J(m/e), a purely mathematical expression with no reference to astrophysics. The three proved facts hold for any positive real numbers m and e. To make this a theorem about reionization, one would need a definition of m and e in that subject's own terms, for instance as a matter density and an energy scale. No such definition appears in the certificate.

What the certificate does establish is a consistency check. It shows that the framework's core cost function has the basic properties one would expect of any sensible penalty: it vanishes at equality, stays nonnegative, and has a positive canonical threshold. The research note attached to the module records an intended application, where the end of reionization might correspond to a redshift of phi^4, about 6.85, a value near the Planck range. That note is a research aspiration, not a proved result. The certificate itself remains a piece of pure mathematics, ready to be connected to physics by a future definition.

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

ReionEnd3Cert does not prove that reionization ended at any particular redshift. The certificate does not define m and e in astrophysical terms. The research note's value of 6.85 is not a theorem.

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/Cosmology/ReionizationEndpoint3_FromJCost.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: