baryonRung_gap45
plain-language theorem explainer
The theorem fixes the baryon rung index at 44 on the phi-ladder used for asymmetry calculations. Cosmologists applying Recognition Science to baryogenesis reference this value when setting eta_B near phi to the minus 44. The proof is immediate reflexivity on the definition of baryonRung as 44.
Claim. The rung index for baryon asymmetry on the phi-ladder equals 44.
background
Recognition Science places baryon asymmetry on the phi-ladder, where mass scales follow yardstick times phi raised to (rung minus 8 plus gap). The module derives eta_B approximately equal to phi to the minus 44 and records the bound phi to the 44 greater than 10 to the 8. The upstream definition baryonRung equals 44 appears in both this module and CosmicMicrowaveBackgroundFromRS, supplying the fixed index for the asymmetry certificate.
proof idea
One-line wrapper that applies reflexivity to the definition baryonRung equals 44.
why it matters
The equality supplies the rung field inside baryonAsymmetryCert, which also carries etaB_pos, phi44_gt_1e8 and etaB_small. It completes the A3 Baryogenesis section of the module by locking the exponent that makes eta_B small. The construction sits inside the phi-ladder structure forced by the self-similar fixed point and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.