Algebra.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Exact-certificate algebra

These lemmas interpret finite rational coefficient lists over real moment vectors. They do not assert that any particular list is a true Hadamard or MUB relation. Such relations must be proved from the mathematical moment definitions.

abbrev OAI.MUB6.Certificate.Sparse line 21
def OAI.MUB6.Certificate.Sparse.eval line 28
Source documentation
Evaluate a sparse rational linear form on a real vector. Repeated keys add.
```
noncomputable def eval (v : Sparse ι) (x : ι → ℝ) : ℝ :=
…
```
Mentions: OAI.MUB6.Certificate.Sparse
def OAI.MUB6.Certificate.Sparse.coeff line 32
Source documentation
The exact coefficient at one key, including all repeated occurrences.
```
def coeff [DecidableEq ι] (v : Sparse ι) (i : ι) : ℚ :=
…
```
Mentions: OAI.MUB6.Certificate.Sparse
def OAI.MUB6.Certificate.Sparse.scale line 35
theorem OAI.MUB6.Certificate.Sparse.eval_nil line 38
theorem OAI.MUB6.Certificate.Sparse.eval_cons line 40
theorem OAI.MUB6.Certificate.Sparse.eval_append line 43
theorem OAI.MUB6.Certificate.Sparse.eval_scale line 47
theorem OAI.MUB6.Certificate.Sparse.coeff_nil line 57
theorem OAI.MUB6.Certificate.Sparse.coeff_cons line 59
theorem OAI.MUB6.Certificate.Sparse.eval_eq_sum_coeff line 63
Source documentation
Coefficient collection is valid for arbitrary real values of the variables.
```
theorem eval_eq_sum_coeff [Fintype ι] [DecidableEq ι]
    (v : Sparse ι) (x : ι → ℝ) :
    eval v x = ∑ i, (coeff v i : ℝ) * x i := by
…
```
Mentions: OAI.MUB6.Certificate.Sparse, OAI.MUB6.Certificate.Sparse.eval, OAI.MUB6.Certificate.Sparse.coeff
theorem OAI.MUB6.Certificate.Sparse.eval_eq_of_coeff_eq line 76
Source documentation
A kernel-checked coefficient comparison transports the interpretation.
```
theorem eval_eq_of_coeff_eq [Fintype ι] [DecidableEq ι]
    (v w : Sparse ι) (h : ∀ i, coeff v i = coeff w i) (x : ι → ℝ) :
    eval v x = eval w x := by
…
```
Mentions: OAI.MUB6.Certificate.Sparse, OAI.MUB6.Certificate.Sparse.coeff, OAI.MUB6.Certificate.Sparse.eval
def OAI.MUB6.Certificate.Sparse.combine line 82
Source documentation
Assemble a proposed linear-combination witness.
```
def combine {κ : Type*} (rows : κ → Sparse ι) (w : Sparse κ) : Sparse ι :=
…
```
Mentions: OAI.MUB6.Certificate.Sparse
theorem OAI.MUB6.Certificate.Sparse.eval_combine line 85

theorem OAI.MUB6.Certificate.Sparse.consequence line 95

Source documentation

Soundness of an exact rational linear consequence certificate.

theorem consequence [Fintype ι] [DecidableEq ι] {κ : Type*}
    (rows : κ → Sparse ι) (w : Sparse κ) (target : Sparse ι)
    (hcoeff : ∀ i, coeff target i = coeff (combine rows w) i)
    (x : ι → ℝ) (hrows : ∀ j, eval (rows j) x = 0) :
    eval target x = 0 := by
…

Mentions: OAI.MUB6.Certificate.Sparse, OAI.MUB6.Certificate.Sparse.coeff, OAI.MUB6.Certificate.Sparse.combine, OAI.MUB6.Certificate.Sparse.eval

theorem OAI.MUB6.Certificate.Sparse.eval_le_abs_sum line 105
Source documentation
A residual coefficient list is bounded by its absolute coefficient sum.
```
theorem eval_le_abs_sum (v : Sparse ι) (x : ι → ℝ)
    (hx : ∀ i, |x i| ≤ 1) :
    eval v x ≤ (v.map fun p => |(p.2 : ℝ)|).sum := by
…
```
Mentions: OAI.MUB6.Certificate.Sparse, OAI.MUB6.Certificate.Sparse.eval
theorem OAI.MUB6.Certificate.residual_arithmetic line 123
Source documentation
The exact final constant and residual norm from the manuscript are separated from any claim that a particular form has these coefficients.
```
theorem residual_arithmetic :
    (-613302797399911 + 179721388988719 : ℚ) / 6480 =
      -2007321335237 / 30 := by norm_num
```
theorem OAI.MUB6.Certificate.residual_strictly_negative line 127

theorem OAI.MUB6.Certificate.contradiction_of_residual line 131

Source documentation

The last step of the mixed certificate, once its interpreted residual identity and coefficient norm have both been proved.

theorem contradiction_of_residual {ι : Type*} (v : Sparse ι) (x : ι → ℝ)
    (Q : ℝ) (hx : ∀ i, |x i| ≤ 1)
    (hQ : Q = -613302797399911 / 6480 + Sparse.eval v x)
    (hnorm : (v.map fun p => |(p.2 : ℝ)|).sum = 179721388988719 / 6480)
    (hpos : 0 ≤ Q) : False := by
…

Mentions: OAI.MUB6.Certificate.Sparse, OAI.MUB6.Certificate.Sparse.eval

inductive OAI.MUB6.Certificate.Combination line 142
Source documentation
A balanced tree of linear combinations avoids a long flattened list during kernel reduction. Each leaf refers to one independently justified equation.
```
inductive Combination (κ : Type*) where
…
```
def OAI.MUB6.Certificate.Combination.eval line 151
def OAI.MUB6.Certificate.Combination.coeff line 156
theorem OAI.MUB6.Certificate.Combination.eval_eq_sum_coeff line 161
theorem OAI.MUB6.Certificate.Combination.eval_zero_of_rows line 171
theorem OAI.MUB6.Certificate.Combination.consequence line 180
Source documentation
Pointwise checks of a balanced combination certify a real linear consequence.
```
theorem consequence [Fintype ι] [DecidableEq ι]
    (rows : κ → Sparse ι) (c : Combination κ) (target : Sparse ι)
    (hcoeff : ∀ i, Sparse.coeff target i = coeff rows i c)
    (x : ι → ℝ) (hrows : ∀ k, Sparse.eval (rows k) x = 0) :
    Sparse.eval target x = 0 := by
…
```
Mentions: OAI.MUB6.Certificate.Sparse, OAI.MUB6.Certificate.Combination, OAI.MUB6.Certificate.Sparse.coeff, OAI.MUB6.Certificate.Combination.coeff, OAI.MUB6.Certificate.Sparse.eval