MatrixBridge.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

From real sign matrices to integer cyclic autocorrelation

The Gram entry is reindexed using translation in Fin n. The real/integer bridge uses the injective coefficient map ℤ → ℝ; it does not assume any classification or any group-ring norm statement.

def OAI.CirculantHadamard.IsIntegerSignRow line 22
Source documentation
An integer sign row with the full Hadamard Gram equation.
```
def IsIntegerSignRow (h : Fin n → ℤ) : Prop :=
…
```

theorem OAI.CirculantHadamard.rowCirculant_gram_apply line 28

Source documentation

The Gram entry at (i,a) is the cyclic autocorrelation at a-i.

theorem rowCirculant_gram_apply [NeZero n] {R : Type uR} [CommRing R]
    (h : Fin n → R) (i a : Fin n) :
    (rowCirculant h * (rowCirculant h).transpose) i a =
      ∑ j, h j * h (j - (a - i)) := by
…

Mentions: OAI.CirculantHadamard.rowCirculant

theorem OAI.CirculantHadamard.gram_eq_iff_autocorrelation line 45

Source documentation

The full Gram equation is exactly the cyclic autocorrelation system.

theorem gram_eq_iff_autocorrelation [NeZero n] {R : Type uR} [CommRing R]
    (h : Fin n → R) :
    rowCirculant h * (rowCirculant h).transpose =
        (n : R) • (1 : Matrix (Fin n) (Fin n) R) ↔
      ∀ a : Fin n, ∑ j, h j * h (j - a) = if a = 0 then (n : R) else 0 := by
…

Mentions: OAI.CirculantHadamard.rowCirculant

theorem OAI.CirculantHadamard.intCast_gram_apply line 67

Source documentation

Casting the integer Gram matrix agrees entry by entry with taking the Gram matrix after casting the row.

theorem intCast_gram_apply (h : Fin n → ℤ) (i j : Fin n) :
    ((rowCirculant h * (rowCirculant h).transpose) i j : ℝ) =
      (rowCirculant (fun a => (h a : ℝ)) *
        (rowCirculant (fun a => (h a : ℝ))).transpose) i j := by
…

Mentions: OAI.CirculantHadamard.rowCirculant

theorem OAI.CirculantHadamard.intCast_scaled_identity_apply line 74

theorem OAI.CirculantHadamard.gram_intCast_iff line 81

Source documentation

The real coefficient embedding preserves and reflects the entire Gram identity, including the diagonal value.

theorem gram_intCast_iff (h : Fin n → ℤ) :
    rowCirculant (fun a => (h a : ℝ)) *
        (rowCirculant (fun a => (h a : ℝ))).transpose =
        (n : ℝ) • (1 : Matrix (Fin n) (Fin n) ℝ) ↔
      rowCirculant h * (rowCirculant h).transpose =
        (n : ℤ) • (1 : Matrix (Fin n) (Fin n) ℤ) := by
…

Mentions: OAI.CirculantHadamard.rowCirculant

theorem OAI.CirculantHadamard.IsIntegerSignRow.exists_real line 99
Source documentation
Every integer sign row gives the actual real circulant Hadamard matrix.
```
theorem IsIntegerSignRow.exists_real {h : Fin n → ℤ} (hh : IsIntegerSignRow h) :
    ExistsRealCirculantHadamard n := by
…
```
Mentions: OAI.CirculantHadamard.IsIntegerSignRow, OAI.CirculantHadamard.ExistsRealCirculantHadamard
theorem OAI.CirculantHadamard.ExistsRealCirculantHadamard.exists_integerSignRow line 111
Source documentation
A real sign matrix determines an integer sign row without approximation.
```
theorem ExistsRealCirculantHadamard.exists_integerSignRow [NeZero n]
    (hH : ExistsRealCirculantHadamard n) : ∃ h : Fin n → ℤ, IsIntegerSignRow h := by
…
```
Mentions: OAI.CirculantHadamard.ExistsRealCirculantHadamard, OAI.CirculantHadamard.IsIntegerSignRow
theorem OAI.CirculantHadamard.integerSignRow_iff_real line 136
Source documentation
Equivalence between the public real matrix problem and integer sign rows.
```
theorem integerSignRow_iff_real [NeZero n] :
    (∃ h : Fin n → ℤ, IsIntegerSignRow h) ↔ ExistsRealCirculantHadamard n := by
…
```
Mentions: OAI.CirculantHadamard.IsIntegerSignRow, OAI.CirculantHadamard.ExistsRealCirculantHadamard
theorem OAI.CirculantHadamard.existsReal_iff_integer_autocorrelation line 144
Source documentation
A direct integer autocorrelation presentation of the real matrix problem.
```
theorem existsReal_iff_integer_autocorrelation [NeZero n] :
    ExistsRealCirculantHadamard n ↔
      ∃ h : Fin n → ℤ, (∀ j, IsSign (h j)) ∧
        ∀ a : Fin n, ∑ j, h j * h (j - a) = if a = 0 then (n : ℤ) else 0 := by
…
```
Mentions: OAI.CirculantHadamard.ExistsRealCirculantHadamard, OAI.CirculantHadamard.IsSign