Gram row-span invariant for no-pivot Bareiss

structure Hex.GramSchmidt.Int.BareissGramRowInvariant {n m : Nat} (b : Matrix Int n m) (state : Matrix.BareissState n) : Type

Row-vector interpretation of the trailing block during a no-pivot Bareiss pass over a Gram matrix. Each active trailing row carries an explicit integer coefficient vector coeff i such that the represented row is Matrix.vecMul (coeff i) b, supported at coordinates ≤ i.val, and each matrix entry in that trailing row is its inner product against the corresponding original row.

• coeff : Fin n → Vector Int n
• coeff_supp (i k : Fin n) : state.step ≤ ↑i → ↑i < ↑k → (self.coeff i)[k] = 0
• entry_eq_dot (i j : Fin n) : state.step ≤ ↑i → state.matrix[i][j] = (Matrix.vecMul (self.coeff i) b).dotProduct (b.row j)

def Hex.GramSchmidt.Int.bareissGramRowInvariant_initial {n m : Nat} (b : Matrix Int n m) : BareissGramRowInvariant b b.gramMatrix.noPivotInitialState

The initial no-pivot Gram state satisfies the row-coefficient invariant with each row represented by the standard basis vector eᵢ.

Equations

• Hex.GramSchmidt.Int.bareissGramRowInvariant_initial b = { coeff := fun (i : Fin n) => Vector.ofFn fun (k : Fin n) => if i = k then 1 else 0, coeff_supp := ⋯, entry_eq_dot := ⋯ }

def Hex.GramSchmidt.Int.bareissGramRowInvariantStepCoeff {n m : Nat} {b : Matrix Int n m} {state : Matrix.BareissState n} (hinv : BareissGramRowInvariant b state) (hnext : state.step + 1 < n) (i : Fin n) (_hi : state.step + 1 ≤ ↑i) : Vector Int n

Coefficient witness produced by one regular Bareiss step on the row at index i. The functional shape mirrors the row update on the matrix side.

Equations

• One or more equations did not get rendered due to their size.

structure Hex.GramSchmidt.Int.BareissGramRegularStepQuotient {n m : Nat} {b : Matrix Int n m} {state : Matrix.BareissState n} (hinv : BareissGramRowInvariant b state) (hnext : state.step + 1 < n) (i : Fin n) (_hi : state.step + 1 ≤ ↑i) : Type

Coefficient-level exact-division provenance for one regular Gram-row Bareiss step. The quotient vector is kept separate from bareissGramRowInvariantStepCoeff so later row-entry proofs can consume the integer divisibility witness before projecting back to the existing exact-div coefficient API.

• q : Fin n → Int
• coeff_num_eq_mul : let k := ⟨state.step, ⋯⟩; ∀ (a : Fin n), state.matrix[(k, k)] * (hinv.coeff i)[a] - state.matrix[(i, k)] * (hinv.coeff k)[a] = self.q a * state.prevPivot

theorem Hex.GramSchmidt.Int.bareissGramRowInvariantStepCoeff_support {n m : Nat} {b : Matrix Int n m} {state : Matrix.BareissState n} (hinv : BareissGramRowInvariant b state) (hnext : state.step + 1 < n) (i : Fin n) (hi : state.step + 1 ≤ ↑i) (a : Fin n) : ↑i < ↑a → (bareissGramRowInvariantStepCoeff hinv hnext i hi)[a] = 0

Canonical coefficient vector and canonicity predicate

def Hex.GramSchmidt.Int.bareissGramCanonicalCoeff {n m : Nat} (b : Matrix Int n m) : Nat → Fin n → Vector Int n

Canonical row-coefficient vector for the initial no-pivot Gram trajectory.

Base case: each row carries the standard basis vector e_i. Inductive step (regular branch, active row): apply the fraction-free Bareiss row update via exactDiv. Processed rows, singular branches, and done branches preserve the previous vector unchanged — mirroring the row-invariant evolution in bareissGramRowInvariant_noPivotLoop_initialAux.

Defined as a pure function of b and fuel (no BareissGramRowInvariant argument), so the canonical coefficient is fixed by the matrix and step count alone. Non-canonical row-coefficient witnesses are ruled out by the IsCanonicalAt predicate consumed by StepWitness.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GramSchmidt.Int.bareissGramCanonicalCoeff b 0 x✝ = Vector.ofFn fun (k : Fin n) => if x✝ = k then 1 else 0

@[simp]

theorem Hex.GramSchmidt.Int.bareissGramCanonicalCoeff_zero {n m : Nat} (b : Matrix Int n m) (i : Fin n) : bareissGramCanonicalCoeff b 0 i = Vector.ofFn fun (k : Fin n) => if i = k then 1 else 0

The canonical coefficient at fuel = 0 is the standard basis vector.

@[simp]

theorem Hex.GramSchmidt.Int.bareissGramCanonicalCoeff_succ_regular {n m : Nat} (b : Matrix Int n m) (fuel : Nat) (i : Fin n) (hnext : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step + 1 < n) (hp : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).matrix[(Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step][(Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step] ≠ 0) (hi : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step + 1 ≤ ↑i) : bareissGramCanonicalCoeff b (fuel + 1) i = let state := Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState; let k := ⟨state.step, ⋯⟩; Vector.ofFn fun (a : Fin n) => Matrix.exactDiv (state.matrix[k][k] * (bareissGramCanonicalCoeff b fuel i)[a] - state.matrix[i][k] * (bareissGramCanonicalCoeff b fuel k)[a]) state.prevPivot

Recursion equation: regular-branch active-row case. With the branch hypotheses in context, simp [*]/simp_all rewrites bareissGramCanonicalCoeff at fuel + 1 to its explicit Bareiss exact-division update.

@[simp]

theorem Hex.GramSchmidt.Int.bareissGramCanonicalCoeff_succ_processed {n m : Nat} (b : Matrix Int n m) (fuel : Nat) (i : Fin n) (hnext : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step + 1 < n) (_hp : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).matrix[(Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step][(Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step] ≠ 0) (hi : ¬(Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step + 1 ≤ ↑i) : bareissGramCanonicalCoeff b (fuel + 1) i = bareissGramCanonicalCoeff b fuel i

Recursion equation: regular-branch processed-row case. An already-processed row (i ≤ step) keeps its previous coefficient vector, so the canonical coefficient at fuel + 1 collapses to the one at fuel.

@[simp]

theorem Hex.GramSchmidt.Int.bareissGramCanonicalCoeff_succ_singular {n m : Nat} (b : Matrix Int n m) (fuel : Nat) (i : Fin n) (hnext : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step + 1 < n) (hp : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).matrix[(Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step][(Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step] = 0) : bareissGramCanonicalCoeff b (fuel + 1) i = bareissGramCanonicalCoeff b fuel i

Recursion equation: singular branch (zero diagonal). A zero pivot skips the update, so the canonical coefficient at fuel + 1 collapses to the one at fuel.

@[simp]

theorem Hex.GramSchmidt.Int.bareissGramCanonicalCoeff_succ_done {n m : Nat} (b : Matrix Int n m) (fuel : Nat) (i : Fin n) (hDone : ¬(Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step + 1 < n) : bareissGramCanonicalCoeff b (fuel + 1) i = bareissGramCanonicalCoeff b fuel i

Recursion equation: done branch (no further work possible). Once the loop can take no further step (¬ step + 1 < n), the canonical coefficient at fuel + 1 collapses to the one at fuel.

def Hex.GramSchmidt.Int.IsCanonicalAt {n m : Nat} (b : Matrix Int n m) (fuel : Nat) (hinv : BareissGramRowInvariant b (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState)) : Prop

A BareissGramRowInvariant on noPivotLoop fuel (noPivotInitialState …) is canonical at fuel when every row's coefficient vector matches bareissGramCanonicalCoeff. This is the soundness gate consumed by StepWitness: non-canonical witnesses (which can shift coefficients by a kernel vector while keeping entry_eq_dot satisfied) cannot invoke the witness's quotient identity.

The SPEC counterexample at rows (1,1), (1,0), (-1,-1) (#6505) produces two distinct BareissGramRowInvariant instances at the same loop state whose coefficient vectors differ by the kernel vector. Both satisfy entry_eq_dot, but only one (the canonical one) yields an integer Bareiss-step quotient.

Equations

• Hex.GramSchmidt.Int.IsCanonicalAt b fuel hinv = ∀ (i : Fin n), hinv.coeff i = Hex.GramSchmidt.Int.bareissGramCanonicalCoeff b fuel i

theorem Hex.GramSchmidt.Int.isCanonicalAt_initial {n m : Nat} (b : Matrix Int n m) : IsCanonicalAt b 0 (bareissGramRowInvariant_initial b)

The base-case row invariant at fuel = 0 carries the standard basis vectors and is therefore canonical.

theorem Hex.GramSchmidt.Int.bareissGramRowInvariant_coeff_transport {n m : Nat} {b : Matrix Int n m} {st1 st2 : Matrix.BareissState n} (h : st1 = st2) (x : BareissGramRowInvariant b st2) (i : Fin n) : (⋯ ▸ x).coeff i = x.coeff i

Transport along an equation of BareissStates preserves the coeff field of a BareissGramRowInvariant. The field's type Fin n → Vector Int n does not depend on the state index, so transport is the identity at that projection. Used to discharge canonicity proofs after transporting an explicit intermediate state back to the noPivotLoop fuel initial form.

def Hex.GramSchmidt.Int.bareissGramRowInvariant_regular_step {n m : Nat} {b : Matrix Int n m} {state : Matrix.BareissState n} (hnext : state.step + 1 < n) (_hp : state.matrix[state.step][state.step] ≠ 0) (hinv : BareissGramRowInvariant b state) (hentry : ∀ (i j : Fin n) (hi : state.step + 1 ≤ ↑i), (state.matrix.stepMatrix state.step state.matrix[state.step][state.step] state.prevPivot)[i][j] = (Matrix.vecMul (bareissGramRowInvariantStepCoeff hinv hnext i hi) b).dotProduct (b.row j)) : BareissGramRowInvariant b { step := state.step + 1, matrix := state.matrix.stepMatrix state.step state.matrix[state.step][state.step] state.prevPivot, prevPivot := state.matrix[state.step][state.step], rowSwaps := state.rowSwaps, singularStep := none }

One regular no-pivot Bareiss step preserves the Gram row-coefficient invariant, provided the later loop proof supplies the exact-division entry relation for the fraction-free updated row combinations.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GramSchmidt.Int.bareissGramRowInvariant_regular_step_coeff_canonical {n m : Nat} (b : Matrix Int n m) (elapsed : Nat) (hinv : BareissGramRowInvariant b (Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState)) (h_canon : IsCanonicalAt b elapsed hinv) (hnext : (Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).step + 1 < n) (hp : (Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).matrix[(Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).step][(Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).step] ≠ 0) (hentry : ∀ (i j : Fin n) (hi : (Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).step + 1 ≤ ↑i), ((Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).matrix.stepMatrix (Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).step (Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).matrix[(Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).step][(Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).step] (Matrix.noPivotLoop elapsed b.gramMatrix.noPivotInitialState).prevPivot)[i][j] = (Matrix.vecMul (bareissGramRowInvariantStepCoeff hinv hnext i hi) b).dotProduct (b.row j)) (i : Fin n) : (bareissGramRowInvariant_regular_step hnext hp hinv hentry).coeff i = bareissGramCanonicalCoeff b (elapsed + 1) i

The coefficient vectors produced by bareissGramRowInvariant_regular_step from a canonical input invariant match bareissGramCanonicalCoeff at the next-step fuel index. Used to propagate canonicity through one regular Bareiss step inside bareissGramRowInvariant_noPivotLoop_initialAux.

@[reducible, inline]

abbrev Hex.GramSchmidt.Int.StepWitness.Cell {n m : Nat} (b : Matrix Int n m) (fuel : Nat) (hinv : BareissGramRowInvariant b (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState)) (_h_canon : IsCanonicalAt b fuel hinv) (hnext : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step + 1 < n) (i : Fin n) (hi : (Matrix.noPivotLoop fuel b.gramMatrix.noPivotInitialState).step + 1 ≤ ↑i) : Type

Per-step quotient package for the initial no-pivot Gram trajectory, restricted to canonical row-coefficient witnesses via IsCanonicalAt.

StepWitness.Cell is an alias for BareissGramRegularStepQuotient whose canonicity gate (h_canon) prevents non-canonical BareissGramRowInvariant witnesses — which can shift coefficients by a kernel vector while still satisfying entry_eq_dot — from supplying integer quotients. The kernel-shift counterexample (SPEC #6505: rows (1,1), (1,0), (-1,-1) at row 2 step 1) shows the restriction is necessary: distinct non-canonical witnesses produce numerators differing by 1, which is not divisible by prevPivot = 2.

Equations

• Hex.GramSchmidt.Int.StepWitness.Cell b fuel hinv _h_canon hnext i hi = Hex.GramSchmidt.Int.BareissGramRegularStepQuotient hinv hnext i hi

@[reducible, inline]

abbrev Hex.GramSchmidt.Int.StepWitness {n m : Nat} (b : Matrix Int n m) : Type

Quotient provenance for the initial no-pivot Gram trajectory, restricted to canonical BareissGramRowInvariant witnesses via IsCanonicalAt. The provider supplies, at every reachable regular Bareiss step, an integer quotient q : Fin n → Int realising the Bareiss-row-update divisibility on the canonical coefficient vectors.

Concrete providers are constructed in HexGramSchmidtMathlib, where the Bareiss-Desnanot proof infrastructure on PSD Gram minors is available; the Mathlib-free layer only consumes this abstraction.

Equations

• One or more equations did not get rendered due to their size.