geometric_seed_eq
plain-language theorem explainer
The geometric seed equals 4π times 11, where the seed is the product of the cube boundary solid angle and the count of passive edges in the Q3 ledger. Researchers assembling first-principles expressions for α inverse cite this equality to fix the leading term. The proof is a term-mode reduction that unfolds the definition then substitutes the solid angle and factor lemmas.
Claim. The geometric seed equals $4π × 11$.
background
The Alpha Derivation module constructs α^{-1} from the cubic ledger in D=3 with no imported constants. The geometric seed is defined as solid_angle_Q3 multiplied by geometric_seed_factor. Module documentation states that 4π arises as total curvature of ∂Q₃ via Gauss-Bonnet while 11 counts the passive edges after one active transition per tick.
proof idea
The term proof unfolds the definition of geometric_seed, rewrites the solid angle factor via solid_angle_Q3_eq, then simplifies the remaining multiplier with geometric_seed_factor_eq_11 and the natural-number cast.
why it matters
This equality supplies the leading term substituted into alphaInv_derived_eq_formula, the main result equating derived α^{-1} to 4π·11 minus the curvature correction. It realizes the geometric seed step of the cubic-ledger derivation, consistent with T8 forcing D=3 and the eight-tick octave. The parent theorem closes the gap to the observed alpha band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.