phi_ring_certificate
plain-language theorem explainer
The declaration certifies that the ring ℤ[φ] satisfies φ² = φ + 1, possesses a multiplicative norm N(a + bφ) = a² + ab - b², and admits Galois conjugation that is an involutive ring automorphism with N(φ) = -1. Recognition Science modelers building the J-cost function and quadratic-integer layer would cite this to anchor algebraic operations. The proof is a term-mode tuple that directly assembles six prior lemmas without additional reasoning.
Claim. In the ring ℤ[φ] of elements a + bφ with a, b ∈ ℤ, the golden ratio satisfies φ² = φ + 1. The norm N(zw) = N(z)N(w) holds for all z, w. Conjugation σ is an involution (σ(σ(z)) = z) and ring homomorphism (σ(zw) = σ(z)σ(w)). Moreover N(1) = 1 and N(φ) = -1.
background
PhiInt is the structure whose elements are pairs (a, b) representing a + bφ with a, b integers; its toReal embedding recovers the usual real value. The norm on this ring is the multiplicative function N(a + bφ) = a² + ab - b², and conjugation is the map sending a + bφ to its Galois conjugate. The local setting is the PhiRing module, which equips ℤ[φ] with ring operations and links it to the cost algebra via J-automorphisms. Upstream, phiInt_sq establishes the minimal polynomial φ² = φ + 1 by direct computation on coefficients, while multiplicative from CostAlgebra records that J-automorphisms preserve the posMul operation.
proof idea
The proof is a one-line term that constructs the required six-tuple by referencing the component lemmas: phiInt_sq supplies the defining equation, PhiInt.norm_mul supplies multiplicativity of the norm, PhiInt.conj_involution and PhiInt.conj_mul supply the involution and homomorphism properties of conjugation, and PhiInt.norm_one together with PhiInt.norm_phi supply the two norm evaluations.
why it matters
This certificate bundles the algebraic facts needed to treat φ as a unit in the quadratic ring that underlies the Recognition Composition Law and J-cost computations. It directly records the connection to cost algebra noted in the module documentation and aligns with the self-similar fixed-point role of φ in the T5–T6 forcing chain. With zero recorded downstream uses, its integration into mass-ladder or Berry-threshold arguments remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.