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

rung_separation

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)

 309theorem rung_separation (ys : ℝ) (hys : 0 < ys) (n k : ℤ) :
 310    mass_rung ys (n + k) / mass_rung ys n = phi ^ (k : ℝ) := by

proof body

Term-mode proof.

 311  have hmr : mass_rung ys n ≠ 0 := ne_of_gt (mass_rung_pos ys hys n)
 312  rw [div_eq_iff hmr]
 313  unfold mass_rung
 314  rw [show ((n + k : ℤ) : ℝ) = (n : ℝ) + (k : ℝ) from by push_cast; ring]
 315  rw [Real.rpow_add phi_pos]
 316  ring
 317
 318/-! ## Part 6: The Consciousness Ground State — Zero Defect
 319
 320The unique zero-cost state (x = 1, J(1) = 0) is the **consciousness
 321ground state**: the recognition configuration with zero defect.
 322
 323All particles live ABOVE this ground state (J > 0). Consciousness IS
 324the ground state — the unique zero-defect configuration on the Q₃ lattice.
 325
 326The "hard problem" dissolves: consciousness is not an emergent property
 327but the GROUND STATE of the spectral decomposition. -/
 328
 329/-- A recognition state on the Q₃ lattice: an assignment of ratios
 330    to the 8 vertices, each positive. -/

depends on (21)

Lean names referenced from this declaration's body.