Physics Quantum Erasure From Jcost

Quantum erasure and its cost

Quantum erasure is a two-step experiment in quantum mechanics. First, a particle is sent through a double slit, but with a device that records which slit it took. That which-path information destroys the interference pattern on the screen; the particle behaves like a classical object going through one slit or the other. Second, the experimenter erases that recorded information. Once the which-path record is gone, the interference pattern comes back. The surprising fact is that the erasure can happen after the particle has already hit the screen, and the pattern still returns, as if the particle's past had been rewritten. The effect was demonstrated in 1982 by Marlan Scully and Kai Drühl, and the standard explanation is that erasing the which-path information makes the two paths indistinguishable again, so their quantum amplitudes can interfere.

The framework of Recognition Science (RS) starts from a different question: what does it cost to recognize a difference between two things? Its central object is a cost function J, which measures the price of distinguishing a measured value from a reference value. The function is forced by a set of plain axioms to have the form J(x) = (x + 1/x)/2 - 1. It is zero when the two values are equal, and it grows as they diverge. In RS, this cost is not a metaphor; it is the engine that produces structure, including the golden ratio and the number of spatial dimensions. The framework's library is a machine-checked collection of formal theorems that derive these consequences from the cost function.

In Recognition Science, the quantum eraser appears as a proposed application of that cost function. The idea, recorded in a research note, is that the quality of interference restoration after erasure should be 1 - J(phi) * (residual_which_path_info), where phi is the golden ratio and the residual which-path information is some number between 0 and 1. Full restoration happens when the cost J is zero, which occurs when the residual information is zero, meaning perfect erasure. The note calls this the "quantum eraser from J-cost": the cost of recognition between the two paths is what destroys interference, and erasing that cost restores it.

The machine-checked module for this subject proves three general facts about the cost function, but nothing specific to quantum erasure. It proves that the cost is zero when the two inputs are equal, that it is never negative for positive inputs, and that the golden ratio minus 3/2 is positive. The module defines a "domainCost" as the cost of the ratio m/e, but it never defines what m and e mean in the quantum eraser context. The docstring is explicit about this: the module proves nothing specific to the subject, because the definition does not reference it. The research note is a statement of where the idea was meant to go, not a result.

What the module does establish, in plain language, is a certificate: a packaged set of the three proved facts, bundled into a structure called QuantumEraserCert. This certificate is a formal object that could be used by future work, if someone defines m and e in terms of which-path information and interference visibility. Until that definition exists, the quantum eraser from J-cost remains a research direction, not a theorem. The honest summary is that the framework has a cost function with the right shape for the idea, but the bridge from cost to the quantum eraser experiment is not yet built.

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]

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

What this page does not claim

The module does not prove that erasing which-path information restores interference. The golden ratio phi minus 3/2 being positive is not a statement about quantum erasure. The research note's formula for restoration quality is not 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/Physics/QuantumErasure_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: