Foundation Electron Compton From Jcost

The Compton wavelength

The Compton wavelength of an electron is the distance scale at which a photon's energy equals the electron's rest energy. It is defined as λ_C = h / (m_e c), where h is Planck's constant, m_e is the electron mass, and c is the speed of light. Its value is about 2426 femtometers, roughly the size of a large atomic nucleus. The scale matters because it sets the threshold where quantum mechanics and relativity meet: a photon with wavelength shorter than this can create electron-positron pairs.

In the framework of Recognition Science, the ledger (a discrete record of events) treats this wavelength as a structural quantity. The framework defines a cost function on the ratio of a mass to the electron mass, and proves three general facts about it. The cost is zero when the ratio is 1, it is never negative for positive inputs, and a threshold constant φ − 3/2 is positive. These are properties of the cost function itself, not of the electron.

The research note records an intended connection: the Compton wavelength divided by the Planck length equals φ^k, where φ is the golden ratio and k ≈ 97.5. This would make the wavelength a power of φ times the Planck length. But the framework proves nothing specific to this subject, because its cost function is defined without reference to the electron's mass or charge. The note is a research direction, not a result.

What the framework does establish is a template: any future definition of mass and charge in its own terms that makes the cost vanish at equality and stay nonnegative will fit the same structure. The three proved facts are universally quantified, so they hold for any positive inputs. The framework is a placeholder, not a derivation of the electron's properties.

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 framework does not derive the electron's Compton wavelength from first principles. The φ-power relation between the Compton wavelength and the Planck length is not proved in this framework.

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