Physics Tunneling Probability From Jcost

Tunneling and the cost function

Quantum tunneling is the phenomenon where a particle passes through a potential barrier even though its energy is lower than the barrier's height. In standard quantum mechanics, the probability of tunneling through a barrier is approximated by the WKB formula T = exp(-2∫κ dx), where κ is the decay constant inside the barrier. The exponential dependence means the probability is extremely sensitive to the barrier's width and height. This is not a mathematical curiosity: tunneling underlies nuclear fusion in stars, the operation of flash memory, and the scanning tunneling microscope that images surfaces atom by atom.

The WKB approximation dates to the 1920s, developed by Wentzel, Kramers, and Brillouin. It works when the potential varies slowly compared to the particle's wavelength. The formula gives the transmission probability as the exponential of minus twice the integral of the imaginary wave number across the barrier. For a simple rectangular barrier of height V and width L, the exponent becomes -2L√(2m(V-E))/ħ. The key feature is that the probability is never zero, even for a barrier far higher than the particle's energy, a result that classical mechanics forbids.

In Recognition Science, the framework models recognition events as a discrete ledger, a record of events with a forced cost. The cost function J(x) = (x + 1/x)/2 - 1 is proved unique under five plain conditions. The framework derives a tunneling probability by replacing the barrier integral with the cost function evaluated at a ratio of two quantities, m and e. The module defines domainCost m e = Jcost(m/e). The proposed recognition tunneling probability is T_recognition = exp(-J(φ)^(-1)) = exp(-8.47) ≈ 2.1×10^-4, where φ is the golden ratio. This is a research note, not a proved result.

What the machine-checked library of formal theorems actually establishes is more modest. The module proves three general facts about the cost function: the cost vanishes when m equals e, the cost is nonnegative for positive inputs, and the quantity φ - 3/2 is positive. These are true for any positive inputs, with no reference to tunneling. The module does not define m or e in terms of barrier height, particle mass, or any physical quantity. The docstring itself states that the module proves nothing specific to tunneling because domainCost is defined without reference to the subject.

The plain-language lesson is that a formal framework can prove general properties of a cost function, but those properties do not become physics until the abstract variables are tied to measurable quantities. The recognition tunneling probability of about 2.1×10^-4 is a proposed identification, not a derived result. The library's theorems guarantee the cost is zero at unity and nonnegative, which are sensible properties for any cost, but they say nothing about the actual probability of a particle crossing a barrier. The gap between the general theorem and the physical claim is exactly the missing definition of m and e in tunneling terms.

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 recognition tunneling probability of 2.1×10^-4 is not a proved theorem; it is a research note. This page does not claim that the framework derives the WKB formula or any specific barrier transmission coefficient. No claim is made that the cost function's nonnegativity implies a physical probability bound.

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/TunnelingProbability_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: