Physics Faraday Constant Rs

The Faraday constant

The Faraday constant, F, is the total electric charge carried by one mole of electrons. Its measured value is approximately 96,485 coulombs per mole (C/mol), and it is defined exactly as the product of the elementary charge e and Avogadro's constant N_A: F = e × N_A. This definition is the classical, framework-neutral starting point; the constant is a bridge between the microscopic scale of a single electron and the macroscopic scale of a mole of matter.

In the Recognition Science framework, the ledger (a discrete record of events) associated with this constant is not a new measurement or a derivation of F. Instead, it defines a cost function (a measure of the price of a recognition event) on the ratio of two masses, m/e. The central definition is domainCost, which applies the framework's universal cost function J(x) = (x + 1/x)/2 - 1 to the ratio m/e. The module then proves three general facts about this cost: it is zero when m equals e, it is never negative for positive inputs, and a threshold value involving the golden ratio is positive.

These three facts are proved in the machine-checked library of formal theorems. The first, domainCost_at_eq, states that the cost of recognizing a mass equal to the elementary charge is zero. The second, domainCost_nonneg, states that the cost is always nonnegative. The third, canonicalThreshold_pos, states that the golden ratio minus 1.5 is greater than zero. These are packaged into a structure called FaradayConstRS and a certificate that the structure is inhabited.

In plain language, the framework establishes that its cost function behaves well when applied to the ratio of a mass to the elementary charge. It does not establish that this ratio has any particular value, nor that the Faraday constant itself is derived from the framework. The documentation above the formal code is a research note recording where the idea was meant to go, not a result. The formal theorems prove only the general properties of the cost function, which are shared verbatim with over two thousand sibling modules in the library.

The consequence is a clear boundary between what is proved and what is hoped. The framework proves that its cost function, when applied to this ratio, has the same basic properties it has for any positive ratio. What would make this a theorem about the Faraday constant is a definition of m and e in the subject's own terms, which the module does not provide.

structure FaradayConstRS where
  cost_at_eq : ∀ r : ℝ, r ≠ 0 → domainCost r r = 0
  cost_nonneg : ∀ m e : ℝ, 0 < m → 0 < e → 0 ≤ domainCost m e
  threshold_pos : 0 < canonicalThreshold

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 does not derive the measured value of the Faraday constant from the framework. The module does not prove any property specific to the Faraday constant beyond the general properties of the cost function. The module's research note about a structural value phi^34 * 0.135 C/mol is 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/Physics/Faraday_Constant_RS.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: