Foundation Proton Radius3 From Jcost Proton Radius3 Cert

What the certificate proves

The proton is a composite particle made of quarks and gluons, and its charge radius is a measured property of how that internal structure spreads out electric charge. The accepted value is about 0.841 femtometers, a length so small that a million of them laid end to end would still be far thinner than a single atom. The Recognition Science framework, which derives physical structure from a forced cost of recognition, has a file named ProtonRadius3Cert that sounds as if it should certify a derivation of that radius. It does not. The file proves three general facts about the framework's cost function, and nothing about protons.

The framework's cost is a number that measures the price of recognizing one quantity in terms of another; the framework proves that any cost satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The certificate's first two facts are about this cost. It vanishes when the two quantities are equal, so recognizing a thing in terms of itself costs zero. It is never negative for positive inputs, so recognition never has a negative price. The third fact is that the golden ratio minus 1.5 is positive, a small numerical threshold that appears in the framework's chain of derivations. Each of these is a proved theorem in the machine-checked library of formal theorems, and the certificate bundles them into one structure.

What the certificate does not do is connect those facts to the proton. The cost function in the file is defined as J(m/e) for two real numbers m and e, with no definition of what m or e mean in the proton's physics. The file's own documentation says this plainly: the Lean code proves nothing specific to the proton radius, because the quantities are not tied to any physical model. The research note above the code tries a guess, r_p = phi^(-3) times the electron Compton wavelength, and gets 572 femtometers, which is wrong by a factor of about 680. A second guess using the Planck length gives 0.016 femtometers, also wrong. The note ends with the word "Structural," meaning the attempt failed structurally, not that it was abandoned for lack of effort.

So the certificate is a small, honest piece of formal work: three general theorems about the cost function, collected under a name that records an intention, not an achievement. The intention was to derive the proton radius from the framework's phi-ladder, and the file shows that derivation does not yet exist. What a reader can take away is a clear example of the framework's discipline: a declaration named after a physical quantity may contain only general mathematics, and the gap between the name and the content is flagged in the file itself.

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 certificate does not derive the proton charge radius, and the research note's guesses are explicitly wrong. The certificate does not prove that the cost function's general properties apply to any specific physical system. The certificate does not establish the golden ratio threshold as physically meaningful for the proton.

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