Physics Qed Corrections3 From Jcost

The module's actual scope

In quantum electrodynamics, the leading correction to the electron's magnetic moment is a famous number: alpha divided by pi, roughly 0.00232 per loop of interaction. The module physics qed corrections3 from jcost in the Recognition Science library was intended to derive that correction from the framework's cost function. The research note attached to the file records the hoped-for match: the framework's value of 0.0125 for the first loop, and 0.00148 for the second, compared against the measured 0.00232. That note is a plan, not a proof.

What the machine-checked code actually establishes is narrower and fully general. The module defines a cost function, a measure of the price of recognition, applied to the ratio of two masses m and e. It proves three facts about that function: the cost is zero when the two masses are equal, the cost is never negative for positive masses, and the golden-ratio constant phi minus 1.5 is positive. These are properties of the cost function itself, true for any positive numbers you substitute. The module contains no definition of m or e in terms of electrons, photons, or any other particle.

The file is one of 2383 sibling modules that share the same body, a template the framework uses to record where a derivation was meant to go. The shared content lives in a single universally quantified module, DomainCostTemplate; this file instantiates it with the ratio m over e. The certificate structure it builds, QEDCorrect3Cert, packages the three proved facts into one object. That object is inhabited, meaning the three facts are consistent, but it says nothing about quantum electrodynamics.

In plain language: the module proves that the cost function behaves sensibly at equality and stays nonnegative, and that a certain threshold is positive. It does not prove any correction to any physical quantity. The bridge from the cost function to a specific particle theory, a definition of m and e in that theory's own terms, remains open. A reader who wants the QED correction must look elsewhere; this page records the gap honestly.

def domainCost (m e : ℝ) : ℝ := Jcost (m / e)

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 proves no correction to any quantum electrodynamics quantity. The numerical agreement in the research note is not a proved result. The cost function's properties here do not depend on any particle physics definition.

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