Physics Neutron Electric Dipole3 From Jcost

Neutron electric dipole and the cost function

The neutron electric dipole moment (nEDM) is a measure of how the neutron's internal charge distribution is separated. A nonzero value would violate time-reversal symmetry, a fundamental symmetry of nature. The current experimental upper bound is |d_n| < 1.8 × 10⁻²⁶ e·cm, meaning the neutron's charge distribution is spherical to extraordinary precision. This tiny number is a powerful constraint on theories of physics beyond the Standard Model.

In Recognition Science, a framework that derives physical structure from a single cost function, the nEDM is predicted to be exactly zero. The framework models reality as maintaining a discrete ledger of recognition events, where each event has a forced cost. The central theorem of the framework proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. From this function, the framework derives a chain of results including an eight-tick recognition cycle and three spatial dimensions.

The module Neutron_Electric_Dipole3_FromJCost applies this cost function to the neutron. It defines domainCost, a term for the cost of a recognition event when the mass m and charge e are in a certain ratio. The module proves three general facts about this cost function: it vanishes when the mass equals the charge, it is nonnegative for positive inputs, and a threshold constant involving the golden ratio is positive. These are formal theorems in the framework's machine-checked library.

The module explicitly states it proves nothing specific to the neutron. The definition of domainCost uses the ratio m/e without reference to the neutron's properties. The module is a template shared with 2383 sibling modules. What would make it a theorem about the nEDM is a definition of m and e in the neutron's own terms, which the module does not provide. The prediction that d_n = 0 exactly is a research note, not a proved result.

The framework's prediction of a zero neutron electric dipole moment is consistent with the current experimental bound, which only sets an upper limit. The exact vanishing follows from the framework's assumption that the QCD theta angle is zero, a consequence of the eight-tick uniqueness. This is a hypothesis with a named falsifier: a measured nonzero nEDM would refute it. The formal theorems in the module establish the general properties of the cost function, not the physical prediction.

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 the neutron electric dipole moment is zero. The framework does not derive the experimental upper bound of 1.8e-26 e·cm. The exact-zero prediction is a hypothesis, not a proved theorem.

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