eta_B_rung_from_dimension_at_D3
plain-language theorem explainer
The theorem shows that the gap-from-dimension witness for the baryon-to-photon rung equals -44 at spatial dimension D=3. Recognition Science researchers deriving exact constants for the baryon asymmetry would cite this result when assembling the full rung certification. The short tactic proof unfolds the definition, substitutes the pre-established integration gap value of 45, and decides the resulting arithmetic equality.
Claim. At spatial dimension $D=3$, the gap-from-dimension witness satisfies $1 - $integrationGap$(D) = -44$, where integrationGap$(D) = 45$.
background
The module derives the integer rung -44 for the baryon-to-photon ratio η_B via three combinatorial witnesses that all reduce to integrationGap D - 1 = 44 at D=3. The integration gap is defined as parityCount d times configDim d. The upstream theorem integrationGap_at_D3 establishes that this product equals 45 when D=3.
proof idea
The proof unfolds the definition of eta_B_rung_from_dimension to expose the subtraction A - integrationGap D. It obtains the hypothesis that integrationGap D equals 45 from integrationGap_at_D3 via exact_mod_cast. Rewriting with this hypothesis reduces the goal to an arithmetic statement that decide verifies directly.
why it matters
This supplies witness A for the certification theorem etaBExactRungCert, which assembles the three witnesses together with their pairwise agreement theorems. It completes the gap-from-dimension path in the η_B rung derivation. The result supports exact constant computation at D=3, consistent with the framework's forcing of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
All fermion masses and α from one equation and the cube
"The η_B rung integer −44 from gap-from-dimension D²(D+2)−1 at D=3 (integrationGap−1=44)."