pith. machine review for the scientific record. sign in
def definition def or abbrev high

row_alphaG_pred

show as:
view Lean formalization →

The declaration defines the RS-native gravitational fine-structure constant for the electron as G times the square of the structural electron mass divided by ħ c. Recognition Science workers on the mass ladder cite it as the P0-AG row that initiates the dimensionless coupling scorecard. The definition is a direct one-line abbreviation that composes the imported constants G, ħ, c with the electron mass expression.

claim$α_G^{RS} := G m_e^2 / (ℏ c)$, where $G$ is the RS-native gravitational constant, $ℏ$ the reduced Planck constant in RS units, $c$ the speed of light, and $m_e$ the structural electron mass.

background

The module sets up the predicted RS-native gravitational coupling α_G^RS in coherence-mass units as the Phase 0 row P0-AG. It uses the constants G = λ_rec² c³ / (π ℏ) and ℏ = φ^{-5} together with the structural electron mass from the phi-ladder. The local setting is the hypothesis bridge that records the raw RS-native value before any external calibration map converts coherence masses to SI kilograms.

proof idea

One-line definition that directly assembles the product G * (electron_structural_mass)^2 / (hbar * c) from the imported constants.

why it matters in Recognition Science

It supplies the starting expression for the AlphaGScoreCard, feeding the closed phi-form theorem alphaG_pred_eq and the numerical bracket theorems alphaG_pred_lower and alphaG_pred_upper. The row marks the explicit hypothesis bridge between the RS-native O(10^9) value and the CODATA O(10^{-45}) target, highlighting the dimensional conversion that remains open in the framework.

scope and limits

Lean usage

have h : row_alphaG_pred = electron_structural_mass ^ 2 * phi ^ (10 : ℝ) / Real.pi := by rw [alphaG_pred_eq]

formal statement (Lean)

  49noncomputable def row_alphaG_pred : ℝ := G * electron_structural_mass ^ 2 / (hbar * c)

proof body

Definition body.

  50

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.