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

ground_state_paradox

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)

 431theorem ground_state_paradox {N : ℕ} (hN : 0 < N) :
 432    (∀ x : ℝ, 0 < x → LawOfExistence.defect x = 0 → x = 1)
 433    ∧ ¬ T4_Recognition (InitialCondition.unity_config N hN) :=

proof body

Term-mode proof.

 434  ⟨fun _x hx hd => (LawOfExistence.defect_zero_iff_one hx).mp hd,
 435   ground_state_recognition_impossible hN⟩
 436
 437/-- **The Origin Question Resolved** — every sub-question answered by T0–T8:
 438    - What drives creation? T4 (recognition requires content)
 439    - Why φ? T6 (closure on geometric sequence)
 440    - Why is the barrier crossable? J(φ) < 1 (finite cost)
 441    - Why the full ladder? Fibonacci cascade + ledger symmetry
 442    - Why unavoidable? T7 (8-tick non-degeneracy) -/

depends on (16)

Lean names referenced from this declaration's body.