Research proof index

The basis formed out of our basisa vectors. -/ noncomputable def basisaAsBasis : Basis (Fin n.succ ⊕ Fin n.succ) ℚ (PureU1 (2 * n.succ + 1)).LinSols := basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card /-! ## F. Every Lienar solution is the sum of a point from each plane

The basis formed out of our basisa vectors. -/ noncomputable def basisaAsBasis : Basis (Fin n.succ ⊕ Fin n.succ) ℚ (PureU1 (2 * n.succ + 1)).LinSols := basisOfLinearIndependentOfCardEqFinrank (@basisa_linear_independent n) basisa_card /-! ## F. Every Lienar solution is the sum of a point from each plane -/ lemma span_basis (S : (PureU1 (2 * n.succ + 1)).L...

Swapping the elements oddShiftFst j and oddShiftSnd j is equivalent to adding a vector basis!AsCharges j.

When a quadratic form is equivalent to a weighted sum of squares, negative weights correspond to vectors where the form takes negative values. This is a concrete realization of a 1-dimensional negative definite subspace, contributing to O'Neill's index ν (Definition 18, p. 47).

For a positive definite quadratic form, the negative dimension (index) is zero. O'Neill states (p. 47) that "ν = 0 if and only if b is positive semidefinite." Since positive definite implies positive semidefinite (Definitions 17 (1) and (2), p. 46), a positive definite form must have index ν = 0.

The canonical commutation relations: [xᵢ, pⱼ] = iℏ δᵢⱼ𝟙. -/ lemma position_commutation_momentum : ⁅𝐱 i, 𝐩 j⁆ = (I * ℏ) • δ[i,j] • ContinuousLinearMap.id ℂ 𝓢(Space d, ℂ) := by ext ψ x show 𝐱 i (𝐩 j ψ) x - 𝐩 j (𝐱 i ψ) x = _ trans (I * ℏ) * (-x i * ∂[j] ψ x + ∂[j] ((fun x : Space d ↦ x i) • ⇑ψ) x) · simp only [positionCLM_apply, momentumCLM_apply,...