Tristram--Levine signature under Seifert-matrix enlargement

The two elementary enlargements of a Seifert matrix preserve its Tristram--Levine signature. Together with congruence invariance, these are the algebraic identities needed for invariance under S-equivalence. The statements hold for every complex parameter, including ω = 1, where the form vanishes; no condition on the Alexander polynomial is needed.

The input remains a real matrix: this does not construct a Seifert surface or assert knot-concordance invariance at roots of the Alexander polynomial.

The calculation follows W. B. R. Lickorish, An Introduction to Knot Theory, GTM 175, Chapter 8, Theorem 8.9.

Formal source: TauCeti.KnotTheory.signature_enlargeColumn in TauCeti.KnotTheory.Signature.

@[simp]

theorem TauCeti.KnotTheory.tristramLevineForm_enlargeColumn {ι : Type u_1} (V : Matrix ι ι ℝ) (ξ : ι → ℝ) (ω : ℂ) : tristramLevineForm (enlargeColumn V ξ) ω = Matrix.fromBlocks (tristramLevineForm V ω) ((1 - ω) • (enlargeBlock ξ).map Complex.ofReal) ((1 - ω) • (enlargeBlock ξ).map Complex.ofReal).conjTranspose !![0, 1 - ω; 1 - (starRingEnd ℂ) ω, 0]

The Tristram--Levine form of a column enlargement: the original form is bordered by one weighted enlargement vector and a two-dimensional Hermitian zero-diagonal block.

@[simp]

theorem TauCeti.KnotTheory.tristramLevineForm_enlargeRow {ι : Type u_1} (V : Matrix ι ι ℝ) (η : ι → ℝ) (ω : ℂ) : tristramLevineForm (enlargeRow V η) ω = Matrix.fromBlocks (tristramLevineForm V ω) ((1 - (starRingEnd ℂ) ω) • (enlargeBlock η).map Complex.ofReal) ((1 - (starRingEnd ℂ) ω) • (enlargeBlock η).map Complex.ofReal).conjTranspose !![0, 1 - (starRingEnd ℂ) ω; 1 - ω, 0]

The Tristram--Levine form of a row enlargement: the transpose-symmetric counterpart of the column enlargement equation.

@[simp]

theorem TauCeti.KnotTheory.tristramLevineSignature_enlargeColumn {ι : Type u_1} [Fintype ι] (V : Matrix ι ι ℝ) (ξ : ι → ℝ) (ω : ℂ) : tristramLevineSignature (enlargeColumn V ξ) ω = tristramLevineSignature V ω

A column enlargement preserves the Tristram--Levine signature at every complex parameter.

@[simp]

theorem TauCeti.KnotTheory.tristramLevineSignature_enlargeRow {ι : Type u_1} [Fintype ι] (V : Matrix ι ι ℝ) (η : ι → ℝ) (ω : ℂ) : tristramLevineSignature (enlargeRow V η) ω = tristramLevineSignature V ω

A row enlargement preserves the Tristram--Levine signature at every complex parameter.