pith. sign in
module module high

IndisputableMonolith.Algebra.PhiRing

show as:
view Lean formalization →

The Algebra.PhiRing module defines the golden ratio φ = (1 + √5)/2 and establishes its core algebraic identities including φ > 1, φ² = φ + 1, and relations to its conjugate ψ. These facts ground the self-similar fixed point in the Recognition Science framework. The module imports Cost and CostAlgebra for cost-based grounding and supplies the algebraic base for RecognitionCategory constructions.

claimLet $φ = (1 + √5)/2$ and $ψ = (1 - √5)/2$. Then $φ > 1$, $φ² = φ + 1$, $ψ² = ψ + 1$, $φψ = -1$, and $φ + ψ = 1$.

background

This module sits in the Algebra domain and supplies the ring-theoretic foundation for φ in Recognition Science. It builds directly on the Cost module, which introduces the J-cost function J(x) = (x + x⁻¹)/2 - 1, and on CostAlgebra, which equips costs with ring operations. The sibling lemmas establish √5 > 0, positivity of φ, the quadratic equation satisfied by φ, and the product and sum identities linking φ and ψ.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

PhiRing supplies the algebraic properties of φ required by the RecognitionCategory module, which constructs the recognition structure on the phi-ladder. It fills the T6 self-similar fixed point step in the forcing chain and enables downstream use of phiPow and PhiInt in mass and dimension formulas.

scope and limits

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (14)