CubicSupplementaryPeriodicityProof.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Modulo 9v periodicity of the actual cubic numerator symbol.

The ramified factor is treated by reciprocity against an auxiliary primary argument. The unit factor follows from Euler's finite-field definition. This proves the elementary specialization recorded in DR v3, §1.2 (1.4)--(1.5), including the zero values at common prime factors.

lemma OAI.CubicFirstMoment.omega_ne_zero line 18
lemma OAI.CubicFirstMoment.primary_coprime_three' line 20
lemma OAI.CubicFirstMoment.symbol_three_aux line 26
Source documentation
Reciprocity compares the value at three whenever both quotients are primary.
```
private lemma symbol_three_aux {a r x : Eisenstein}
    (ha : primary a) (hr : primary r) (hx : primary x)
    (hax : a - r = 3*x) (har : IsCoprime a r) :
    cubicSymbol a 3 = cubicSymbol r 3 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicSymbol
lemma OAI.CubicFirstMoment.cubicSymbol_three_periodic line 52
Source documentation
The ramified supplementary factor depends only on the primary argument modulo nine.
```
lemma cubicSymbol_three_periodic {a b : Eisenstein} (ha : primary a) (hb : primary b)
    (hab : (9 : Eisenstein) ∣ a-b) : cubicSymbol a 3 = cubicSymbol b 3 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicSymbol
lemma OAI.CubicFirstMoment.cubicSymbol_lambda_periodic line 80
lemma OAI.CubicFirstMoment.normNat_int line 103
lemma OAI.CubicFirstMoment.primary_norm_third line 107
lemma OAI.CubicFirstMoment.symbol_omega_prime line 119
lemma OAI.CubicFirstMoment.cubicSymbol_omega_norm line 134
Source documentation
Euler's definition for the unit factor, with an integer exponent convenient for congruences.
```
lemma cubicSymbol_omega_norm {a : Eisenstein} (ha : primary a) :
    cubicSymbol a omegaE = omega ^ (((normNat a : ℤ)-1)/3) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.cubicSymbol, OAI.CubicFirstMoment.omegaE, OAI.CubicFirstMoment.omega, OAI.CubicFirstMoment.normNat
lemma OAI.CubicFirstMoment.cubicSymbol_omega_periodic line 154
lemma OAI.CubicFirstMoment.unit_eq_signed_omega line 178
lemma OAI.CubicFirstMoment.cubicSymbol_unit_periodic line 211
lemma OAI.CubicFirstMoment.unit_coprime_right line 220
lemma OAI.CubicFirstMoment.normNat_lambda line 225
lemma OAI.CubicFirstMoment.lambda_irreducible line 236
lemma OAI.CubicFirstMoment.eisenstein_unit_eq_signed_omega line 252
Source documentation
Explicit classification of the six Eisenstein units.
```
lemma eisenstein_unit_eq_signed_omega {u : Eisenstein} (hu : IsUnit u) :
    ∃ j : ℕ, u = omegaE^j ∨ u = -(omegaE^j) := unit_eq_signed_omega hu
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.omegaE, OAI.CubicFirstMoment.unit_eq_signed_omega
lemma OAI.CubicFirstMoment.lambdaE_prime line 255
Distinct definitions of this name: OAI/NumberTheory/CubicGauss/Cutoffs.lean:46 (same statement text; different proof or body). Qualify references as OAI.CubicFirstMoment.lambdaE_prime@path.
theorem OAI.CubicFirstMoment.cubicSupplementaryPeriodicity_proved line 258
Source documentation
All nonzero numerators, with the usual zero extension at common factors.
```
theorem cubicSupplementaryPeriodicity_proved : CubicSupplementaryPeriodicity := by
…
```
Mentions: OAI.CubicFirstMoment.CubicSupplementaryPeriodicity