PhiInt
plain-language theorem explainer
PhiInt defines the ring ℤ[φ] as integer pairs (a, b) representing a + bφ with operations reduced by φ² = φ + 1. Algebraists and Recognition Science researchers modeling the phi-ladder or quadratic extensions would cite this carrier. The structure is declared directly, followed by explicit ring operations and axiom proofs via case analysis plus the omega tactic.
Claim. Let φ satisfy φ² = φ + 1. The ring ℤ[φ] consists of elements a + bφ with a, b ∈ ℤ. Addition is componentwise: (a + bφ) + (c + dφ) = (a + c) + (b + d)φ. Multiplication is (a + bφ)(c + dφ) = (ac + bd) + (ad + bc + bd)φ.
background
In Recognition Science, φ is the self-similar fixed point forced at T6 of the UnifiedForcingChain. ℤ[φ] supplies the discrete lattice for the phi-ladder appearing in mass formulas. The module imports CostAlgebra (whose multiplicative theorem asserts f(xy) = f(x)f(y) for JAut on PosReal) and LedgerAlgebra (whose conj_involution states e.conj.conj = e).
proof idea
PhiInt is introduced as a plain structure with fields a : ℤ and b : ℤ. Addition, negation, and multiplication are defined by direct formulas, with multiplication reduced using φ² = φ + 1. Ring axioms are established by exhaustive case analysis on constructors followed by the omega tactic on integer equalities.
why it matters
This definition supplies the algebraic carrier for the phi-ladder and J-cost constructions in the algebra layer. It supports downstream work in CostAlgebra and LedgerAlgebra even though used_by_count is zero, marking foundational status. It directly instantiates the T6 phi fixed point and prepares the eight-tick octave (T7) and D = 3 spatial structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.