seam_numerator_at_D3
plain-language theorem explainer
The seam numerator for the cubic ledger evaluates to 103 at spatial dimension three. Researchers assembling the curvature term in the alpha derivation from voxel topology would cite this evaluation. The proof is a one-line native decision that reduces the arithmetic definition seam_numerator D directly to the constant 103.
Claim. For spatial dimension $D=3$, the seam numerator (base normalization plus Euler closure) equals 103.
background
The module derives the fine-structure constant from the geometry of the cubic ledger Q3. The spatial dimension D is defined as 3, the value forced by the requirement that linking occurs only in three dimensions. The seam numerator is the function seam_numerator(d) := seam_denominator(d) + euler_closure; its doc-comment states that this is where 103 comes from, arising from base normalization 6 times 17 equals 102 plus the +1 Euler closure term.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the definition seam_numerator D, which expands to seam_denominator D plus euler_closure and evaluates arithmetically to 103.
why it matters
This supplies the numerator 103 that appears in the curvature term equality curvature_term = -103/(102 pi^5) and in the downstream curvature correction formula. It fills the explicit evaluation step in the alpha derivation from cubic geometry, consistent with the forced D=3 and the eight-tick octave. The result is used by curvature_correction_eq_formula, curvature_power_family_matches_derived_iff, and seam_ratio_from_topology to enforce the exponent 5 and the seam ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.