Cosmology Sound Horizon5 Sound Horizon5 Cert

The certificate's scope

The cosmic microwave background, the oldest light in the universe, carries a ruler: the sound horizon, the distance a pressure wave traveled through the hot plasma before the universe cooled enough to let light through. Cosmologists measure that distance at about 147 megaparsecs, a scale that shows up as a subtle spacing in the patterns of the microwave sky. The Recognition Science library contains a declaration named SoundHorizon5Cert that appears to touch this number. In plain language, it establishes something far smaller and more general.

The certificate is a small structure in the framework's machine-checked library of formal theorems. It bundles three facts about a function called domainCost, a discrete record of the cost of recognizing one quantity as another. The facts are these: the cost is zero when the two quantities are equal; the cost is never negative when both quantities are positive; and a particular threshold value, the golden ratio minus three halves, is positive. Each fact is proved in the library's formal language, with no gaps left for human intuition to fill.

The declaration's name points at cosmology, but the proofs inside it do not. The function domainCost is defined as the cost function J applied to a ratio m/e, with no definition of what m and e mean in any physical setting. The three theorems hold for any positive real numbers, which is why they are true, and also why they say nothing about megaparsecs. The library itself records this plainly: the module proves nothing specific to the sound horizon, because the quantities in the cost function are not tied to any physical measurement.

What the certificate does establish is a template. The same three facts appear verbatim in more than two thousand sibling modules, all sharing one universally quantified statement in a central file. SoundHorizon5Cert is an instance of that template, a check that the general facts hold here too. It is a proof of consistency, not a discovery of a distance. The research note attached to the module sketches where the idea was meant to go, an exact match between the sound horizon and a formula built from the golden ratio, but the note is explicitly not a result.

For a reader of the library, the certificate is a small signpost. It shows that the framework's core cost function behaves well in this context, and it marks a location where a physical claim was intended but not yet made. The distance itself remains a target for future work, a goal that would require defining the two quantities in cosmological terms before any theorem about the horizon could be proved.

structure SoundHorizon5Cert where
  cost_at_eq : ∀ r : ℝ, r ≠ 0 → domainCost r r = 0
  cost_nonneg : ∀ m e : ℝ, 0 < m → 0 < e → 0 ≤ domainCost m e
  threshold_pos : 0 < canonicalThreshold

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

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

What this page does not claim

The certificate does not prove that the sound horizon equals any particular number of megaparsecs. The certificate does not establish that the golden ratio formula for the sound horizon is correct. The certificate does not define m or e in terms of any cosmological measurement.

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