StarkDescent.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Odd-index descent of a simple zero

Cyclic Hecke factorizations supply the real characters used by Stark's odd-degree argument. The zero order on any fixed field is an average of signs and is therefore at most one. A positive order at an odd-index subgroup is incompatible with a nonvanishing rational zeta function.

theorem OAI.DukePrimeDegree.fixedFieldMultiplicity_le_one_of_cyclic_characters line 26

Source documentation

The cyclic character data bounds every actual fixed-field order.

theorem fixedFieldMultiplicity_le_one_of_cyclic_characters
    {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)
    (hcyclic : ∀ C : Subgroup (E ≃ₐ[ℚ] E), IsCyclic C → ∃ χ : C →* ℝˣ,
      (∀ x : C, fixedFieldMultiplicity β (Subgroup.zpowers (x : E ≃ₐ[ℚ] E)) =
        if χ x = 1 then 1 else 0) ∧
      fixedFieldMultiplicity β C = if χ = 1 then 1 else 0)
    (H : Subgroup (E ≃ₐ[ℚ] E)) : fixedFieldMultiplicity β H ≤ 1 := by
…

Mentions: OAI.DukePrimeDegree.fixedFieldMultiplicity

theorem OAI.DukePrimeDegree.no_odd_index_positive_zero_of_cyclic_characters line 51
def OAI.DukePrimeDegree.HasCyclicRayRealizations line 65
Source documentation
Even ray realizations of each cyclic subgroup's Frobenius characters.
```
def HasCyclicRayRealizations (E : Type*) [Field E] [NumberField E] [IsGalois ℚ E] : Prop :=
…
```
theorem OAI.DukePrimeDegree.extension_multiplicity_pos_of_ray_realizations line 74
Source documentation
Propagation to the extension is obtained from actual cyclic factors.
```
theorem extension_multiplicity_pos_of_ray_realizations
    (hray : HasCyclicRayRealizations E)
    {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)
    (H : Subgroup (E ≃ₐ[ℚ] E)) (hH : 0 < fixedFieldMultiplicity β H) :
    0 < zetaMultiplicity E β := by
…
```
Mentions: OAI.DukePrimeDegree.HasCyclicRayRealizations, OAI.DukePrimeDegree.fixedFieldMultiplicity, OAI.DukePrimeDegree.zetaMultiplicity
theorem OAI.DukePrimeDegree.cyclic_character_of_ray_realizations line 86

theorem OAI.DukePrimeDegree.no_odd_index_zero_of_ray_realizations line 110

Source documentation

The final finite Galois descent, before choosing a normal closure.

theorem no_odd_index_zero_of_ray_realizations
    (hray : HasCyclicRayRealizations E)
    {β : ℝ} (hβ0 : 0 < β) (hβ1 : β < 1)
    (hsimple : zetaMultiplicity E β = 1)
    (H : Subgroup (E ≃ₐ[ℚ] E)) (hodd : Odd H.index)
    (hH : 0 < fixedFieldMultiplicity β H) (hQ : zetaMultiplicity ℚ β = 0) : False := by
…

Mentions: OAI.DukePrimeDegree.HasCyclicRayRealizations, OAI.DukePrimeDegree.zetaMultiplicity, OAI.DukePrimeDegree.fixedFieldMultiplicity