Foundation Neutron Proton Diff Rs5 Neut Proton Diff5 Cert

A certificate's scope

The neutron and proton differ in mass by about 1.293 MeV, a measured value from nuclear physics. The declaration NeutProtonDiff5Cert in the Recognition Science library looks as if it should certify a derivation of that number. The name suggests a result about the neutron-proton difference, and a research note in the source file records the intended target: an expression involving the golden ratio and the W boson mass that would land on 1.293 MeV. The actual formal content is much narrower.

What the declaration proves is three general facts about a cost function, a measure of how far one positive number is from another. The function is defined as J(m/e), where J is a fixed mathematical function from the framework's core. The three facts are: the cost is zero when the two numbers are equal, the cost is never negative for positive inputs, and a certain threshold constant involving the golden ratio is positive. These are properties that hold for any positive pair of numbers whatsoever. They say nothing specific about neutrons, protons, or any physical system.

The certificate bundles these three facts into a single structure and proves that such a structure exists. It is a formal object, a way of packaging three theorems together. The theorems themselves are proved in a machine-checked library of formal mathematics, meaning the logical steps have been verified by a computer. What the certificate does not do is define what m and e mean for the neutron and proton. Without such a definition, the cost function is just a function of two abstract numbers, and the certificate is about that abstract function, not about particle physics.

The research note in the source file is explicit about this gap. It states that the module proves nothing specific to the neutron-proton subject, because the cost is defined without reference to it. The note records where the idea was meant to go, not a result. The numerical agreement with 1.293 MeV that the note mentions is a hypothesis, a target for future work, not a proved consequence. The certificate itself is a small, correct piece of mathematics about a general cost function, and its name is a promise about a physical application that the formal content does not yet deliver.

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]

theorem cert_inhabited : Nonempty NeutProtonDiff5Cert := ⟨cert⟩

What this page does not claim

The certificate does not derive the measured 1.293 MeV neutron-proton mass difference. The certificate does not define what m and e mean for the neutron and proton. The numerical agreement in the research note is a hypothesis, not a proved result.

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