electron_strength
plain-language theorem explainer
The declaration defines the recognition strength for the electron by delegating to the general recognition_strength function on the electron fermion species and an input RG residue value. A physicist comparing geometric mass residues to perturbative RG flow would cite this when quantifying the amplification factor needed for the underlying recognition interaction. It is realized as a direct one-line abbreviation around the sibling recognition_strength definition.
Claim. Let $g^e_{rec}(r)$ denote the electron recognition strength for RG residue $r$. Then $g^e_{rec}(r) := F(Z_e)/r$, where $F(Z) = ln(1 + Z/φ)/ln(φ)$ is the gap function and $Z_e$ is the electron charge index.
background
The RecognitionCoupling module formalizes the discrepancy between the geometric residue $F(Z)$ required by the mass formula and the small residue $f_{RG}$ obtained from integrating Standard Model beta functions. Recognition strength is introduced as the ratio bridging this gap, treating Standard Model forces as shadows of a stronger recognition force. The gap function is supplied by Masses.RSBridge.Anchor.gap as $F(Z) := ln(1 + Z/φ)/ln(φ)$, and Fermion.e is the electron constructor in the Fermion inductive type from the same anchor module. Upstream results include PrimitiveDistinction.from, which extracts four structural conditions from seven axioms, and UniversalForcingSelfReference.for, which records meta-realization properties.
proof idea
This is a one-line wrapper that applies recognition_strength to Fermion.e and the supplied rg_val parameter.
why it matters
This definition supplies the concrete electron instance used by the downstream theorem electron_strength_gt_100, which establishes a lower bound greater than 100 for the specific RG residue 0.04942583. It operationalizes the module's comparison of geometric predictions (F ≈ 13.95 for Z=1332) against perturbative RG residues. Within the Recognition Science framework it connects the phi-ladder mass formula to the gap function without asserting a universal constant across species.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.