Foundation Many Worlds From Jcost Many Worlds3 Cert

The certificate

Many-worlds interpretation of quantum mechanics, the idea that every quantum possibility branches into a separate universe, has a long history and a simple core: the wavefunction never collapses, it just splits. In the Recognition Science framework, that branching is tied to a ledger, a discrete record of recognition events, and to the cost of recognition, a number that measures how hard it is to tell two states apart. The declaration ManyWorlds3Cert is a machine-checked certificate, a formal object that packages three proved facts about that cost function.

The three facts are plain. First, when the two inputs to the cost are equal, the cost is zero: domainCost r r = 0. Second, for positive inputs, the cost is never negative. Third, the number phi - 3/2, which the framework calls the canonical threshold, is positive; here phi is the golden ratio, about 1.618, so the threshold is about 0.118. These are not deep theorems about many-worlds. They are elementary consequences of the definition of the cost function, and the certificate simply records that they hold.

What the certificate does not do matters more. The documentation states that it proves nothing specific to many-worlds, because the cost is defined as Jcost (m / e) without any definition of what m and e mean in this subject. The research note attached to the module says branches multiply when J(amplitude) exceeds J(phi), and that small-amplitude branches are recognition-undetectable, but that note is a plan, not a result. The certificate itself contains no such claim.

In plain terms, ManyWorlds3Cert is a box that holds three true statements about a function. The box does not contain the many-worlds story, even though the box sits in a file with that name. A reader who wants the branching claim must look for a definition of m and e in the subject's own terms; the certificate does not supply it.

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 branches multiply when J(amplitude) exceeds J(phi). The certificate does not establish that small-amplitude branches are recognition-undetectable. The certificate does not define m and e in physical terms.

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/Foundation/ManyWorldsFromJCost.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: