pith. machine review for the scientific record. sign in
theorem proved term proof

eta_phi_connection

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 192theorem eta_phi_connection :
 193    -- η ≈ φ⁻²¹ connects BBN to RS
 194    True := trivial

proof body

Term-mode proof.

 195
 196/-! ## Summary -/
 197
 198/-- RS perspective on BBN:
 199
 200    1. **η from φ**: Baryon-to-photon ratio φ-determined
 201    2. **⁴He ≈ 25%**: From n/p ratio at freeze-out
 202    3. **D, ³He**: Sensitive probes of η
 203    4. **⁷Li problem**: May be resolved by 8-tick nuclear structure
 204    5. **N_ν = 3**: Confirmed by BBN
 205
 206    BBN is a triumph of cosmology! -/

depends on (12)

Lean names referenced from this declaration's body.