Physics Dark Photon3 From Jcost

A template, not a prediction

A dark photon is a hypothetical particle, a heavier cousin of the ordinary photon, that could carry a new force in the dark sector. The module named dark photon3 from jcost in the Recognition Science library does not predict its mass. It proves three general facts about a cost function, and leaves the physics as a research note.

The core definition is domainCost (m e) = Jcost (m / e), where Jcost is the framework's unique cost function, J(x) = (x + 1/x)/2 - 1. The module proves that this cost is zero when the two masses are equal, that it is nonnegative for positive inputs, and that a certain threshold, phi - 3/2, is positive. These are properties of the cost function itself, not of any dark photon.

The file's docstring records an intended research direction: a dark photon mass around 2 GeV, estimated from a ratio involving the Z boson mass. But the Lean code defines domainCost without any reference to a dark photon, its mass, or its coupling. The module is a template, shared verbatim with 2383 sibling modules, each of which would need its own physical definition of m and e to become a theorem about its subject.

What the module does establish, in plain language, is that the cost function has the basic properties one would want from a measure of mismatch: it vanishes at agreement, it never goes negative, and it has a built-in positive threshold. The dark photon prediction itself remains a research note, not a proved result.

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]

What this page does not claim

The module does not predict the dark photon mass. The 2 GeV value is a research note, not a proved result. The cost function's properties are not specific to dark photons.

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