generationStepDerived
This definition assembles the lepton generation step as eleven passive edges plus the single active edge scaled by the fractional solid angle per direction. Physicists deriving muon-electron mass ratios from cellular-automaton geometry cite it to isolate the differential transition from the integrated coupling. The definition is a direct algebraic sum of the passive count, active count, and reciprocal total solid angle.
claimThe generation step is defined by $s = N_p + N_a / 4π$, where $N_p = 11$ counts the passive field edges in three dimensions, $N_a = 1$ counts the active edge per tick, and the factor $1/4π$ is the solid-angle fraction contributed by the active direction.
background
Recognition events unfold on a cellular-automaton tape; each tick applies a local rule to a radius-1 neighborhood, producing a successor configuration. In this setting the module distinguishes passive edges (eleven, fixed by the cube geometry of D=3) that integrate over the full sphere from the single active edge that drives the differential mass step between lepton generations. The upstream definitions supply activeEdgeCount = 1, passiveEdgeCount = 11, and fractionalSolidAngle = 1/totalSolidAngle, with the latter equal to 1/(4π) by the sphere-surface formula.
proof idea
The declaration is a one-line definition that casts the passive and active edge counts to reals and adds their weighted sum using the already-defined fractionalSolidAngle. No tactics or lemmas are invoked beyond the sibling definitions of passiveEdgeCount, activeEdgeCount, and fractionalSolidAngle.
why it matters in Recognition Science
The definition supplies the differential step that enters the electron-to-muon mass ratio. It is used by the downstream theorems fractional_step_is_forced and alpha_step_relationship, which demonstrate that the same geometric ingredients (4π solid angle, 11 passive edges, 1 active edge) appear in both the α seed and the generation step but combine multiplicatively versus additively. This closes the structural gap between integrated coupling and generation transition inside the Recognition forcing chain.
scope and limits
- Does not include the α² correction present in the full lepton-step formula.
- Does not compute numerical mass ratios or higher-generation steps.
- Does not incorporate renormalization or quantum-loop effects.
- Does not address non-lepton sectors or non-D=3 geometries.
Lean usage
unfold generationStepDerived fractionalSolidAngle; ringformal statement (Lean)
155noncomputable def generationStepDerived : ℝ :=
proof body
Definition body.
156 (passiveEdgeCount : ℝ) + (activeEdgeCount : ℝ) * fractionalSolidAngle
157
158/-- The generation step equals 11 + 1/(4π). -/