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

E_coh_pos

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)

 229theorem E_coh_pos : 0 < E_coh := by

proof body

Term-mode proof.

 230  simp only [E_coh]
 231  exact zpow_pos phi_pos (-5)
 232
 233/-! ## Summary: The Forcing Chain -/
 234
 235/-- **PHI FORCING PRINCIPLE**
 236
 237The golden ratio φ is forced by self-similarity in a discrete J-cost ledger:
 238
 2391. Discrete ledger with J-symmetry (from previous levels)
 2402. Self-similarity: the structure references itself at different scales
 2413. Compositional constraint: r² = r + 1 (next scale = current + base)
 2424. Unique positive solution: r = φ = (1 + √5)/2
 243
 244This is Level 4 of the forcing chain:
 245Composition law → J unique → Discreteness → Ledger → **φ** → D=3 → physics -/

used by (9)

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

depends on (23)

Lean names referenced from this declaration's body.