IndisputableMonolith.Algebra.PhiRing
This module supplies the algebraic lemmas and definitions for the golden ratio φ and its conjugate in the Recognition Science setting. It is cited by downstream work on RecognitionCategory and the phi-ladder mass formula. The content consists of direct statements of positivity, fixed-point equations, and product-sum identities with no complex derivations.
claimLet $\phi = (1 + \sqrt{5})/2$ and $\psi = (1 - \sqrt{5})/2$. The module records $\sqrt{5} > 0$, $\phi > 1$, $\phi^2 = \phi + 1$, $\psi^2 = \psi + 1$, $\phi \psi = -1$, $\phi + \psi = 1$, and the associated integer powers $\phi^n$ together with the type $\mathrm{PhiInt}$.
background
Recognition Science derives φ as the self-similar fixed point forced by T6 after J-uniqueness (T5). The module imports Cost and CostAlgebra to supply the ring operations needed for later recognition structures. Sibling declarations establish the basic arithmetic facts: sqrt5_pos asserts positivity of the square root, phi_equation and psi_equation record the quadratic relations, phi_psi_product and phi_psi_sum record the elementary symmetric identities, and phiPow together with PhiInt introduce the integer powers and the integer span.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the algebraic substrate required by IndisputableMonolith.Algebra.RecognitionCategory. It directly supports the phi-ladder rung construction and the native-unit constants (G = φ^5/π, ħ = φ^{-5}) that appear in the forcing chain T0–T8.
scope and limits
- Does not derive the forcing chain T5–T6.
- Does not compute numerical values of physical constants.
- Does not define the RecognitionCategory itself.
- Does not treat non-integer powers or real exponents.