IndisputableMonolith.Algebra.PhiRing
The PhiRing module establishes the algebraic properties of the golden ratio phi and its conjugate psi as the foundation for self-similar scaling in Recognition Science. It proves sqrt(5) > 0, phi > 1, the quadratic equation phi^2 = phi + 1, and the product and sum identities with psi. These facts are required for the Recognition Composition Law and downstream category constructions. The module consists of sequential basic lemmas on real arithmetic.
claim$\sqrt{5} > 0$, $\phi > 0$, $\phi > 1$, $\phi^2 = \phi + 1$, $\psi^2 = \psi + 1$, $\phi\psi = -1$, $\phi + \psi = 1$ where $\phi = (1 + \sqrt{5})/2$ and $\psi = (1 - \sqrt{5})/2$.
background
PhiRing operates in the Algebra domain, importing Cost and CostAlgebra to embed phi within the cost structure of Recognition Science. It introduces phi as the positive root of the quadratic x^2 - x - 1 = 0 together with its conjugate psi, along with the phi-ladder scaling that appears in mass formulas.
The local setting is the real numbers equipped with the J-cost operations. Upstream results from CostAlgebra supply the ring axioms compatible with the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).
proof idea
This is a definition module collecting elementary lemmas on phi; the structure consists of sequential definitions (PhiInt, phiPow) followed by direct applications of real-number inequalities and algebraic identities.
why it matters in Recognition Science
PhiRing supplies the algebraic identities for phi that are imported by IndisputableMonolith.Algebra.RecognitionCategory. It realizes the self-similar fixed point required by T6 of the forcing chain and makes the phi-ladder available for the Recognition Composition Law and the eight-tick octave constructions.
scope and limits
- Does not prove J-uniqueness or the forcing chain T0-T8.
- Does not derive physical constants alpha, G, or hbar.
- Does not address the mass formula or Berry creation threshold.
- Does not construct the RecognitionCategory itself.