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

ml_nucleosynthesis_eq_phi

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)

 118theorem ml_nucleosynthesis_eq_phi : ml_nucleosynthesis = φ := by

proof body

Term-mode proof.

 119  unfold ml_nucleosynthesis phi_ladder tier_difference
 120  simp [nuclear_tier_local, luminosity_tier_local, zpow_one]
 121
 122/-! ## Eight-Tick Quantization -/
 123
 124/-- Nuclear reactions are quantized by the eight-tick cycle.
 125
 126Each nuclear reaction step:
 1271. Requires 8 ticks for one complete recognition cycle
 1282. Releases energy in units of E_coh × φ^{-r} for some rung r
 1293. Updates the ledger with conserved quantities
 130
 131This forces tier indices to be integers. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (31)

Lean names referenced from this declaration's body.

… and 1 more