BinaryLocalization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The characteristic-two local ring for the binary contradiction

The maximal ideal is constructed from an actual finite characteristic-zero integer algebra. Unit denominators follow from the odd norm identity, not from an assumed extension of complex conjugation to a localization.

theorem OAI.CirculantHadamard.BinaryLocalization.exists_maximal_two_mem line 23
Source documentation
A finite characteristic-zero integer algebra has a maximal ideal over two.
```
theorem exists_maximal_two_mem (B : Type uB) [CommRing B] [CharZero B]
    [Module.Finite ℤ B] :
    ∃ m : Ideal B, m.IsMaximal ∧ (2 : B) ∈ m := by
…
```

theorem OAI.CirculantHadamard.BinaryLocalization.residue_char_two line 32

Source documentation

The one residue field used by both first-order maps has characteristic two.

theorem residue_char_two {B : Type uB} [CommRing B] (m : Ideal B) [m.IsPrime]
    (htwo : (2 : B) ∈ m) :
    CharP (IsLocalRing.ResidueField (Localization.AtPrime m)) 2 := by
…

theorem OAI.CirculantHadamard.BinaryLocalization.map_i_eq_one line 44
Source documentation
A square root of minus one reduces to one in a field of characteristic two.
```
theorem map_i_eq_one {O : Type uO} {k : Type uk} [CommRing O] [Field k] [CharP k 2]
    (φ : O →+* k) (i : O) (hi : i ^ 2 = -1) : φ i = 1 := by
…
```
theorem OAI.CirculantHadamard.BinaryLocalization.map_odd_nat_eq_one line 56
Source documentation
An odd scalar is one in the common characteristic-two residue field.
```
theorem map_odd_nat_eq_one {O : Type uO} {k : Type uk} [CommRing O] [Field k] [CharP k 2]
    (φ : O →+* k) {u : ℕ} (hu : Odd u) : φ (u : O) = 1 := by
…
```
theorem OAI.CirculantHadamard.BinaryLocalization.isUnit_of_mul_eq_odd_square line 63
Source documentation
The odd norm supplies a unit without requiring the second factor to be a conjugation operation on the local ring.
```
theorem isUnit_of_mul_eq_odd_square {O : Type uO} [CommRing O] [IsLocalRing O]
    [CharP (IsLocalRing.ResidueField O) 2] {x y : O} {u : ℕ}
    (hu : Odd u) (hxy : x * y = (u : O) ^ 2) : IsUnit x := by
…
```

theorem OAI.CirculantHadamard.BinaryLocalization.odd_power_of_map line 75

Source documentation

A faithful ring embedding reflects the odd-power witness for an actual unit.

theorem odd_power_of_map {O : Type uO} {F : Type uF} [CommRing O] [CommRing F]
    (f : O →+* F) (hf : Function.Injective f) (u : Oˣ)
    (h : ∃ m : ℕ, 0 < m ∧ Odd m ∧ (f (u : O)) ^ m = 1) :
    ∃ m : ℕ, 0 < m ∧ Odd m ∧ u ^ m = 1 := by
…