Foundation Wave Particle Duality3 From Jcost

The cost of choosing

Wave-particle duality is the quantum puzzle where light and matter behave like waves in some experiments and like particles in others. The classic picture is a toggle: an electron is either a wave or a particle depending on the measurement. Recognition Science offers a different picture, one where the toggle becomes a dial. The framework defines a cost, a number that records how expensive a recognition event is, and uses it to grade the transition between wave-like and particle-like behavior.

The key object is a function called J-cost. For any positive ratio, the cost is J(x) = (x + 1/x)/2 - 1. This function has a simple shape: it is zero when the ratio is 1, and it grows as the ratio moves away from 1 in either direction. The framework applies this to duality by taking the ratio of two quantities, one for interference (the wave side) and one for detection (the particle side). When the ratio is 1, the cost is 0, which the framework reads as pure wave behavior. When the ratio is very large or very small, the cost approaches 1, which it reads as pure particle behavior. In between, the cost moves continuously, so the duality is a smooth transition, not a binary switch.

In Recognition Science, the framework models this as a continuous transition in J-cost between wave (J=0) and particle (J=1) limits. The machine-checked library of formal theorems, called the framework's library, proves three general facts about this cost function. First, the cost vanishes when the two inputs are equal. Second, the cost is never negative for positive inputs. Third, a specific threshold value, phi - 3/2, is positive, where phi is the golden ratio. These are the theorems in the module, and they hold for any positive inputs, not just for wave and particle quantities.

What the module does not do is say what those inputs are. The definition takes two real numbers m and e, but it never defines m as interference or e as detection. The library proves facts about the abstract cost function, but the link to wave-particle duality is a research note, not a theorem. The structure WPDuality3Cert packages the three proven facts, and the theorem cert_inhabited shows such a certificate exists. The mathematics is solid, but the physical interpretation is a plan for future work, not a result.

The consequence is a clear target. The framework has the mathematical machinery to describe a smooth wave-particle transition, but it needs a definition of the two quantities in physical terms. Once someone defines m and e for a real experiment, the cost function gives a concrete prediction for how the wave-particle balance shifts with the setup. Until then, the module is a proof of the cost function's basic properties, with the duality story waiting for its physical input.

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]

theorem cert_inhabited : Nonempty WPDuality3Cert := ⟨cert⟩

What this page does not claim

The module does not prove that wave-particle duality is continuous in any real experiment. The module does not define what m and e mean physically. The module does not derive J-cost itself; it uses the proved J-cost function.

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