Cosmology Cmbtemp3 From Jcost Cmbtemp3v2 Cert

What the certificate proves

The cosmic microwave background (CMB) is the faint glow left over from the hot early universe, measured at 2.725 kelvin. In Recognition Science, a research note attached to a formal declaration records an intended connection: that this temperature might follow from a golden-ratio scaling law. The declaration itself, however, proves no such connection.

What the declaration CMBTemp3v2Cert actually establishes is a small package of three general facts about a cost function. A cost function here is a rule that assigns a nonnegative number to a comparison between two quantities, here written as domainCost m e, defined as Jcost (m / e). The three facts are: the cost is zero when the two quantities are equal; the cost is never negative for positive inputs; and a certain threshold value, phi minus 3/2, is positive.

The machine-checked library of formal theorems proves these three statements for any positive real numbers m and e. The proofs are general: they rely only on the definition of the cost function and on the fact that the golden ratio phi is greater than 1.5. The certificate assembles these three proofs into a single structure and confirms that such a structure exists.

In Recognition Science, the framework models the CMB temperature as T_vac times phi to the power negative 196, where T_vac is the Planck temperature. That calculation gives 2.73 kelvin, close to the measured 2.725 kelvin. But this is a research note, not a theorem. The declaration does not define what m and e mean for the CMB, so it cannot connect the general cost facts to any specific physical quantity.

What the certificate changes is the epistemic status of the three cost facts: they are checked, not assumed. What it does not change is the status of the CMB temperature prediction, which remains a stated intention without a formal proof. A reader should take the certificate as a proof about cost functions, and as a record of where the CMB idea was meant to go, not as evidence for that idea.

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

The certificate does not prove that the CMB temperature equals 2.725 kelvin. The certificate does not prove any connection between the cost function and the golden ratio scaling law for the CMB. The certificate does not establish that the CMB temperature prediction is correct or even well-defined.

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/CMBTemp3_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: