`phi_ring_certificate`

proved

show as: view math explainer →

module: IndisputableMonolith.Algebra.PhiRing
domain: Algebra
line: 471 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Algebra.PhiRing on GitHub at line 471.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 468    5. φ² = φ + 1 (defining relation) ✓
 469    6. N(φ) = −1 (φ is a unit) ✓
 470    7. Connection to cost algebra: J(φ) computed ✓ -/
 471theorem phi_ring_certificate :
 472    -- φ satisfies defining equation
 473    (PhiInt.phi * PhiInt.phi = PhiInt.phi + PhiInt.one) ∧
 474    -- Norm is multiplicative
 475    (∀ z w : PhiInt, PhiInt.norm (z * w) = PhiInt.norm z * PhiInt.norm w) ∧
 476    -- Conjugation is involution
 477    (∀ z : PhiInt, z.conj.conj = z) ∧
 478    -- Conjugation preserves multiplication
 479    (∀ z w : PhiInt, (z * w).conj = z.conj * w.conj) ∧
 480    -- N(1) = 1
 481    PhiInt.norm 1 = 1 ∧
 482    -- N(φ) = -1
 483    PhiInt.norm PhiInt.phi = -1 :=
 484  ⟨phiInt_sq, PhiInt.norm_mul, PhiInt.conj_involution,
 485   PhiInt.conj_mul, PhiInt.norm_one, PhiInt.norm_phi⟩
 486
 487end PhiRing
 488end Algebra
 489end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.