Astrophysics Cmb Lensing3 From Jcost Cmblensing3 Cert

What the certificate proves

The cosmic microwave background (CMB) is the oldest light in the universe, a faint glow left over from about 380,000 years after the Big Bang. Its subtle temperature patterns carry information about the distribution of matter, and the way that distribution bends this light, an effect called lensing, leaves a measurable imprint on the CMB's power spectrum. The spectrum's lensing peak appears at an angular scale of roughly l = 70 to 80 in maps from the Planck satellite, a fact measured by that mission and reported in its data releases.

In Recognition Science, the framework's machine-checked library of formal theorems contains a declaration named CMBLensing3Cert. Despite the name, it does not establish anything about the CMB. The certificate bundles three general facts about a function called cost, a measure of recognition effort that the framework derives from forced conditions. The three facts are: the cost vanishes when its two inputs are equal, the cost is never negative for positive inputs, and a certain threshold value phi minus 1.5 is positive. Each fact is proved from the definition of cost, and the certificate simply packages them into one structure.

The definition behind the certificate is domainCost(m, e) = Jcost(m / e), where Jcost is the framework's cost function and m and e are real numbers. The three theorems that fill the certificate are general: they hold for any positive m and e, not for any particular physical quantity. The docstring attached to the module says plainly that it proves nothing specific to this subject, because the definition does not reference the CMB at all. The name CMBLensing3Cert records where the idea was meant to go, not a result about lensing.

The research note in the module does mention a possible connection: the framework's golden-ratio scaling predicts a lensing peak at l = phi^9, which is about 76, consistent with the measured range of 70 to 80. That is a hypothesis, not a theorem. What the certificate itself establishes is only the three general cost facts. A real theorem about CMB lensing would require defining m and e in terms of the CMB's own physics, which the module does not do.

structure CMBLensing3Cert 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

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)

structure CMBLensing3Cert 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

structure CMBLensing3Cert 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

What this page does not claim

The certificate does not prove that the CMB lensing peak is at l = 76. The certificate does not derive any property of the cosmic microwave background from the cost function. The name CMBLensing3Cert does not indicate a proved result about lensing.

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