Foundation Superposition Cost Rs

Superposition cost

A quantum system can exist in a superposition, a blend of two or more states at once, written as a weighted sum like ψ = α|0⟩ + β|1⟩. The weights α and β are complex numbers whose squared magnitudes give the probabilities of measuring each state. In Recognition Science, the cost of recognizing such a superposition is not a free choice; it is a function of the ratio of the amplitudes' magnitudes.

The framework defines this cost as J(|α|/|β|), where J is the unique cost function forced by the framework's five axioms. At equal superposition, where |α| = |β|, the ratio is 1 and the cost is zero, the minimum possible. A maximally coherent state, one where both outcomes are equally likely, therefore carries no recognition cost. The framework's library, a machine-checked collection of formal theorems, proves three general facts about this cost: it vanishes when the two magnitudes are equal, it is never negative for positive inputs, and a threshold value φ − 3/2 is positive.

These three facts are assembled into a certificate, a structure that bundles them together. The library proves this certificate exists. But the module is careful about what it does not claim. The cost function is defined directly on the ratio of two real numbers, without any reference to a specific physical system. The library proves facts about that function, not about any particular quantum state. The definition of what m and e are, in a subject's own terms, is left open. The module is a template, not a completed physical theory.

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

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]

What this page does not claim

This module proves nothing about any specific physical system, because m and e are left undefined. The cost function is not derived from the framework's axioms here; it is defined directly as J(m/e). The module does not establish that a maximally coherent state is physically preferred, only that its cost is zero.

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