Golden Integer Ring and Parity Conductor
Abstract
The golden coordinate ring is algebra-equivalent to the ring of integers of the golden number field, and the transported even-second-coordinate order has parity conductor (2).
Theorem 1.1 (The golden number field has discriminant five).
Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/GoldenIntegerRing.golden_numberField_discr (✓ std3). ∎
Source. Repository-derived.
Commentary.
GoldenNumberField is the quadratic algebra over the rationals with generator omega satisfying omega squared equals omega plus one. The theorem computes its number-field discriminant as exactly five.
The proof first computes discriminant five in the ordered rational basis (1, omega), proves that both basis vectors are integral, and compares it with Mathlib’s integral basis. Integrality of the change-of-basis determinant and integer divisibility leave only discriminant five.
Definition 1.2 (The coordinate ring is carried to the actual ring of integers).
Lean statement: D5/S3/Arith/Lattices/GoldenIntegerRing.goldenIntegerRingAlgEquiv
Formalization. D5/S3/Arith/Lattices/GoldenIntegerRing.goldenIntegerRingAlgEquiv (✓ std3).
Source. Repository-derived.
Commentary.
GoldenIntegerRing is an abbreviation for the ring of integers of GoldenNumberField. The module defines a GoldenInt algebra embedding that sends the coordinate pair (a, b) to a plus b times omega, proves the required integrality and fraction-ring instances, and uses integral-closure uniqueness to construct an Int-algebra equivalence from GoldenInt to GoldenIntegerRing.
This declaration is equivalence data, not an equality of the two carrier types. The associated definitions expose its underlying ring equivalence and the image of the golden generator phi.
Definition 1.3 (The even-second-coordinate subring is transported to the ring of integers).
Lean statement: D5/S3/Arith/Lattices/GoldenIntegerRing.goldenEvenSecondCoordinateOrder
Formalization. D5/S3/Arith/Lattices/GoldenIntegerRing.goldenEvenSecondCoordinateOrder (✓ std3).
Source. Repository-derived.
Commentary.
The module defines a coordinate subring of GoldenInt by requiring the second coordinate to be twice an integer. goldenEvenSecondCoordinateOrder is the image of that subring under goldenIntegerRingAlgEquiv.
Definition 1.4 (The mapped ideal generated by two defines a finite place).
Lean statement: D5/S3/Arith/Lattices/GoldenIntegerRing.goldenTwoFinitePlace
Formalization. D5/S3/Arith/Lattices/GoldenIntegerRing.goldenTwoFinitePlace (✓ std3).
Source. Repository-derived.
Commentary.
goldenTwoPrimeIdeal is defined by transporting the coordinate ideal generated by two into GoldenIntegerRing. Local proofs establish that this ideal is maximal and nonzero, and goldenTwoFinitePlace packages it as a height-one prime of the ring of integers. This is a constructed finite-place carrier, not a theorem classifying all places over two.
Definition 1.5 (The conductor is defined by multiplication into the parity order).
Lean statement: D5/S3/Arith/Lattices/GoldenIntegerRing.goldenEvenSecondCoordinateOrderConductor
Formalization. D5/S3/Arith/Lattices/GoldenIntegerRing.goldenEvenSecondCoordinateOrderConductor (✓ std3).
Source. Repository-derived.
Commentary.
goldenEvenSecondCoordinateOrderConductor is the ideal of elements x in GoldenIntegerRing such that x times every element of GoldenIntegerRing lies in goldenEvenSecondCoordinateOrder. Closure under zero, addition, and scalar multiplication is supplied as part of this ideal carrier.
Theorem 1.6 (The defined conductor is exactly the mapped ideal generated by two).
Proof. Machine-checked in Lean as D5/S3/Arith/Lattices/GoldenIntegerRing.goldenEvenSecondCoordinateOrderConductor_eq_goldenTwoPrimeIdeal (✓ std3). ∎
Source. Repository-derived.
Commentary.
The conductor condition applied to one makes the transported second coordinate even, and applied to the golden generator makes the first coordinate even as well. Hence a conductor element lies in the transported ideal generated by two.
Conversely, multiplying an arbitrary golden integer by two makes the second coordinate of every further product even. Transport through the ring equivalence therefore puts every element of the mapped ideal in the conductor, proving equality of the two ideals.
References
- Truth anchor:
D5/S3/Arith/Lattices/GoldenIntegerRing.goldenEvenSecondCoordinateOrder - Truth anchor:
D5/S3/Arith/Lattices/GoldenIntegerRing.goldenEvenSecondCoordinateOrderConductor - Truth anchor:
D5/S3/Arith/Lattices/GoldenIntegerRing.goldenEvenSecondCoordinateOrderConductor_eq_goldenTwoPrimeIdeal - Truth anchor:
D5/S3/Arith/Lattices/GoldenIntegerRing.goldenIntegerRingAlgEquiv - Truth anchor:
D5/S3/Arith/Lattices/GoldenIntegerRing.goldenTwoFinitePlace - Truth anchor:
D5/S3/Arith/Lattices/GoldenIntegerRing.golden_numberField_discr