Pith. sign in
module module moderate

IndisputableMonolith.Physics.Faraday_Constant_RS

show as:
view Lean formalization →

Defines the Faraday constant in Recognition Science units from the Cost and Constants layers, together with a domain cost, a canonical positive threshold, and a small certificate package. Experimentalists matching molar charge scales to the phi-ladder would cite it. The module is mostly definitions and elementary positivity or equality lemmas, not a deep derivation.

claimIn RS-native units the module introduces a domain cost $C$, a canonical threshold $\theta>0$, and the Faraday constant $F_{\mathrm{RS}}$ built from the RS cost and time quantum $\tau_0=1$, together with a certificate that the construction is inhabited and meets the stated positivity and evaluation identities.

background

Recognition Science fixes units so that $c=1$ and the fundamental tick is $\tau_0=1$, with $\hbar=\varphi^{-5}$ and $G=\varphi^5/\pi$. The Cost import supplies the J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and obeying the Recognition Composition Law.

This physics module sits downstream of those primitives. It packages a domain-level cost functional, evaluates it at a canonical point, and names the resulting Faraday-scale constant $F_{\mathrm{RS}}$. The Faraday constant in SI is $N_A e$; here the analogous object is expressed in the RS ladder language rather than as a fresh empirical input.

Sibling definitions cover nonnegativity of the domain cost, positivity of the canonical threshold, and a small certificate type witnessing that the construction is inhabited.

proof idea

Definition-heavy module. Core objects (domain cost, canonical threshold, $F_{\mathrm{RS}}$, certificate) are introduced by def or abbrev from Constants and Cost. Supporting lemmas are elementary: evaluation identities for the domain cost, nonnegativity, positivity of the threshold, and inhabitation of the certificate. No long tactic scripts or deep forcing-chain arguments appear at module scope; proofs reduce to unfolding and basic real arithmetic.

why it matters in Recognition Science

Gives the RS-native Faraday constant a named home next to the other physics constants built from $\varphi$ and $J$. That lets later electrochemistry or molar-charge comparisons cite a single RS object instead of re-deriving the scale from $\tau_0$ and Cost each time. The module currently has no recorded downstream dependents in the mirror graph, so it is a leaf packaging layer rather than a step inside T0–T8. It does not itself force $D=3$, the eight-tick octave, or the fine-structure band; it only exports the Faraday-scale constant and its certificate once those primitives are fixed.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)