N_e_factorization
plain-language theorem explainer
Natural-number identity 55 = 5 × 11, recorded as a named factorization in the baryon φ-rung arithmetic. Cosmology proofs that split the N_e count through the passive-mode factor 11 and the five-fold factor cite it. The proof is a one-line norm_num evaluation.
Claim. As natural numbers, $55 = 5 \times 11$.
background
The module fixes the baryon-asymmetry rung on the Recognition Science φ-ladder: rung 44 carries η_B = φ^{-44}, and then records the pure arithmetic factorizations that relate that rung to the eight-tick period and the passive-mode count.
N_e appears among the sibling arithmetic lemmas (with N_e_arithmetic and the “11 times table”). The factorization 55 = 5 × 11 is the five-fold multiple of the passive-mode factor 11; the same table also records 4 × 11 = 44 (the baryon rung itself) and the difference 11. Upstream gap and Clifford/8-tick material supplies the structural reason those integers appear, but this declaration is only the integer identity.
proof idea
Term-mode proof discharged by norm_num: Lean reduces both sides of the natural-number equality to decimal form and checks they match. No lemmas are invoked beyond the built-in numeral evaluator.
why it matters
Keeps the N_e side of the baryon φ-rung bookkeeping fully explicit and sorry-free. The module status line is “0 sorry, 0 axiom”; naming 55 = 5 × 11 lets later certificates (PhiRungLadderCert, eleven_times_table, baryon_rung_factorization) rewrite without re-proving elementary arithmetic. In the broader RS chain the integers 5 and 11 sit next to the eight-tick octave (T7) and the gap-45 construction, but this lemma itself only certifies the product. No downstream theorems currently depend on it; it is infrastructure for the local rung table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.