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

phi_pos

show as:
view Lean formalization →

The golden ratio φ satisfies φ > 0. Researchers deriving the golden ratio from J-cost minimization in the Recognition Science framework cite this as the basic positivity property needed for the φ-ladder. The proof is a one-line term wrapper that invokes the corresponding fact inside the Constants structure.

claimLet φ denote the golden ratio. Then φ > 0.

background

The Φ-Emergence module derives the golden ratio from J-cost minimization. The Constants structure from LawOfExistence bundles CPM constants including φ, with nonnegativity constraints such as 0 ≤ Knet. Upstream results supply the abstract bundle definition and collision-free program classes that underwrite the constant extraction.

proof idea

This is a one-line wrapper that directly applies Constants.phi_pos from the LawOfExistence module.

why it matters in Recognition Science

The result supplies the positivity foundation for the φ-ladder and self-similarity properties in the Recognition framework, directly supporting T5 J-uniqueness and T6 phi fixed-point emergence. It fills the initial positivity step in the φ-Emergence module whose doc-comment states the derivation from J-cost minimization. No open questions are addressed.

scope and limits

formal statement (Lean)

  26theorem phi_pos : φ > 0 := Constants.phi_pos

proof body

Term-mode proof.

  27
  28/-- The golden ratio is greater than 1 -/

depends on (5)

Lean names referenced from this declaration's body.