Foundation Superposition Cost Rs Superposition Cost Cert

What the certificate proves

Superposition is the quantum idea that a system can be in a combination of states at once, written as ψ = α|0> + β|1>. The Recognition Science framework assigns each such state a cost, a number meant to measure how hard that state is to recognize. The declaration SuperpositionCostCert bundles three proved facts about that cost into one package: the cost is zero when the two amplitudes are equal, it is never negative for positive inputs, and a certain threshold involving the golden ratio is positive. These are the three facts the certificate certifies.

Each fact is a theorem in the machine-checked library of formal theorems. The first says that when the two amplitudes have the same absolute value, the cost is exactly zero. The second says that for positive amplitudes, the cost never goes below zero. The third says that φ − 3/2, where φ is the golden ratio, is greater than zero. The certificate simply collects these three theorems into a single structure, and the library proves that such a certificate exists.

What the certificate does not claim is more important. The framework's own documentation states plainly: the paragraph describing superposition cost is a research note, not a result. The cost function is defined as J(m/e) without any reference to superposition, so the three proved facts hold for any positive numbers m and e, not specifically for quantum amplitudes. The certificate proves nothing about superposition itself. The module is one of 2383 siblings sharing the same body; what would make it a theorem about superposition is a definition of m and e in quantum terms, which the framework has not supplied.

In plain terms: the certificate is a small, correct package of general facts about a cost function. It is not a derivation of quantum mechanics. The framework labels this honestly as an open target, not a result.

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 superposition states have zero cost at equal amplitudes; it proves a general fact about the cost function for any positive numbers. The certificate does not derive the Born rule or any quantum measurement postulate. The framework does not claim that the research note about superposition is a proved result.

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: