BinaryProductTransport.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Odd-power products in the concrete binary local ring

The local units are supplied with their actual coefficient-ring values. Their alternating product maps to the fixed alternating product in the fraction field. Injectivity transports each exact power identity back to the local units, with the same exponent.

theorem OAI.CirculantHadamard.BinaryProductTransport.odd_power_mul_inv line 26

Source documentation

Odd-power torsion is closed under taking a quotient in a commutative group. The product of the two supplied exponents is an explicit witness.

theorem odd_power_mul_inv {G : Type uG} [CommGroup G] (x y : G)
    (hx : ∃ m : ℕ, 0 < m ∧ Odd m ∧ x ^ m = 1)
    (hy : ∃ n : ℕ, 0 < n ∧ Odd n ∧ y ^ n = 1) :
    ∃ r : ℕ, 0 < r ∧ Odd r ∧ (x * y⁻¹) ^ r = 1 := by
…

def OAI.CirculantHadamard.BinaryProductTransport.localUnitToFraction line 38
Source documentation
The actual map from local units to the fraction field of B u.
```
def localUnitToFraction (u : ℕ) : (O u)ˣ →* FractionRing (B u) :=
…
```
theorem OAI.CirculantHadamard.BinaryProductTransport.localUnitToFraction_apply line 41
theorem OAI.CirculantHadamard.BinaryProductTransport.localUnitToFraction_injective line 44
theorem OAI.CirculantHadamard.BinaryProductTransport.local_alternatingProduct_toFraction line 52
Source documentation
Transport of the literal signed subset product, using the supplied value equality only for subsets that occur in the product.
```
theorem local_alternatingProduct_toFraction {I : Type uI} (u : ℕ) (t : Finset I)
    (x : Finset I → B u) (X : Finset I → (O u)ˣ)
    (hX : ∀ S ⊆ t, (X S : O u) = toLocal u (x S)) :
    localUnitToFraction u (alternatingProduct t X) =
      alternatingProduct t (fun S => algebraMap (B u) (FractionRing (B u)) (x S)) := by
…
```
Mentions: OAI.CirculantHadamard.BinaryProductTransport.localUnitToFraction, OAI.CirculantHadamard.alternatingProduct

theorem OAI.CirculantHadamard.BinaryProductTransport.local_alternatingProduct_pow_eq_one line 65

Source documentation

An exact fraction-field power identity holds for the actual local alternating product with precisely the same exponent.

theorem local_alternatingProduct_pow_eq_one {I : Type uI} (u : ℕ) (t : Finset I)
    (x : Finset I → B u) (X : Finset I → (O u)ˣ)
    (hX : ∀ S ⊆ t, (X S : O u) = toLocal u (x S)) (m : ℕ)
    (hpow : (alternatingProduct t
      (fun S => algebraMap (B u) (FractionRing (B u)) (x S))) ^ m = 1) :
    (alternatingProduct t X) ^ m = 1 := by
…

Mentions: OAI.CirculantHadamard.alternatingProduct

theorem OAI.CirculantHadamard.BinaryProductTransport.local_alternatingProduct_has_odd_power line 75

theorem OAI.CirculantHadamard.BinaryProductTransport.local_alternatingProduct_ratio_has_odd_power line 87

Source documentation

The two concrete unit families produce an odd-power quotient family. No torsion of individual factors is assumed or inferred.

theorem local_alternatingProduct_ratio_has_odd_power {I : Type uI}
    (u : ℕ) (t : Finset I) (x y : Finset I → B u)
    (X Y : Finset I → (O u)ˣ)
    (hX : ∀ S ⊆ t, (X S : O u) = toLocal u (x S))
    (hY : ∀ S ⊆ t, (Y S : O u) = toLocal u (y S))
    (hx : ∃ m : ℕ, 0 < m ∧ Odd m ∧
      (alternatingProduct t
        (fun S => algebraMap (B u) (FractionRing (B u)) (x S))) ^ m = 1)
    (hy : ∃ m : ℕ, 0 < m ∧ Odd m ∧
      (alternatingProduct t
        (fun S => algebraMap (B u) (FractionRing (B u)) (y S))) ^ m = 1) :
    ∃ m : ℕ, 0 < m ∧ Odd m ∧
…

Mentions: OAI.CirculantHadamard.alternatingProduct