Algebraic finite-chart detector spine for Zhou's §4. Paper: §4.

@[reducible, inline]

abbrev Connes.PaperChartDetector.F : Type

The F construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetector.F = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperChartDetector.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetector.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperChartDetector.C : Submodule Construction.k Construction.PaperKernel.TensorAA

The C construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetector.C = Connes.Construction.PaperKernel.C

@[reducible, inline]

abbrev Connes.PaperChartDetector.TensorAA : Type

The TensorAA construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetector.TensorAA = Connes.Construction.PaperKernel.TensorAA

@[instance_reducible]

noncomputable instance Connes.PaperChartDetector.coeffIndexLinearOrder (N : ℕ) : LinearOrder (PaperFiniteCharts.CoeffIndex N)

Equations

• Connes.PaperChartDetector.coeffIndexLinearOrder N = LinearOrder.lift' ⇑finSumFinEquiv ⋯

noncomputable def Connes.PaperChartDetector.cross (a b : A) : ↥C

The symmetric cross term of two vectors. Paper: §4.

Equations

• Connes.PaperChartDetector.cross a b = ⟨a ⊗ₜ[Connes.Construction.k] b + b ⊗ₜ[Connes.Construction.k] a, ⋯⟩

@[simp]

theorem Connes.PaperChartDetector.cross_apply (a b : A) : ↑(cross a b) = a ⊗ₜ[Construction.k] b + b ⊗ₜ[Construction.k] a

theorem Connes.PaperChartDetector.diagonal_add (a b : A) : Construction.PaperKernel.diagonal (a + b) = Construction.PaperKernel.diagonal a + Construction.PaperKernel.diagonal b + cross a b

The square of a sum splits into squares and the symmetric cross term. Paper: §4.

def Connes.PaperChartDetector.upper {ι : Type u_1} [Fintype ι] [LinearOrder ι] (i : ι) : Finset ι

Expansion of a square over a finite affine coordinate family. Paper: §4.

Equations

• Connes.PaperChartDetector.upper i = {x : ι | i < x}

theorem Connes.PaperChartDetector.sum_pair_upper {ι : Type u_1} [Fintype ι] [LinearOrder ι] (T : ι → ι → TensorAA) : ∑ i : ι, ∑ j : ι, T i j = ∑ i : ι, T i i + ∑ i : ι, ∑ j ∈ upper i, (T i j + T j i)

theorem Connes.PaperChartDetector.diagonal_sum_expansion {ι : Type u_1} [Fintype ι] [LinearOrder ι] (b : A) (u : ι → A) : Construction.PaperKernel.diagonal (b + ∑ i : ι, u i) = Construction.PaperKernel.diagonal b + ∑ i : ι, cross b (u i) + ∑ i : ι, Construction.PaperKernel.diagonal (u i) + ∑ i : ι, ∑ j ∈ upper i, cross (u i) (u j)

def Connes.PaperChartDetector.chartIndexOfCoefficients (N : ℕ) (s : Fin 3) (x : PaperFiniteCharts.CoeffIndex N → F) : PaperFiniteCharts.ChartIndex N

The chartIndexOfCoefficients construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetector.chartIndexOfCoefficients N s x = (s, fun (i : Fin N) => x (Sum.inl i), fun (i : Fin N) => x (Sum.inr i))

theorem Connes.PaperChartDetector.chartPoint_ofCoefficients_eq_sum (N : ℕ) (s : Fin 3) (x : PaperFiniteCharts.CoeffIndex N → F) : PaperFiniteCharts.chartPoint N (chartIndexOfCoefficients N s x) = PaperFiniteCharts.basisVector s + ∑ i : PaperFiniteCharts.CoeffIndex N, x i • PaperFiniteCharts.coefficientVector N s i

@[simp]

theorem Connes.PaperChartDetector.cross_smul_left (r : F) (a b : A) : cross (r • a) b = r • cross a b

@[simp]

theorem Connes.PaperChartDetector.cross_smul_right (r : F) (a b : A) : cross a (r • b) = r • cross a b

@[simp]

theorem Connes.PaperChartDetector.diagonal_smul (r : F) (a : A) : Construction.PaperKernel.diagonal (r • a) = r • Construction.PaperKernel.diagonal a

noncomputable def Connes.PaperChartDetector.chartEvaluation (χ : ↥C →ₗ[Construction.k] Construction.k) (N : ℕ) (s : Fin 3) (x : PaperFiniteCharts.CoeffIndex N → F) : F

The chartEvaluation construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperChartDetector.chartQuadraticData (χ : ↥C →ₗ[Construction.k] Construction.k) (N : ℕ) (s : Fin 3) : BooleanPolynomial.QuadraticData (PaperFiniteCharts.CoeffIndex N)

The chartQuadraticData construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperChartDetector.upper_quadratic_sum {ι : Type u_1} [Fintype ι] [LinearOrder ι] (d : ι → F) (c : ι → ι → F) (x : ι → F) : ∑ i : ι, ∑ j : ι, (if i = j then d i else if i < j then c i j else 0) * x i * x j = ∑ i : ι, d i * x i + ∑ i : ι, ∑ j ∈ upper i, c i j * x i * x j

theorem Connes.PaperChartDetector.chartEvaluation_eq_quadraticData_eval (χ : ↥C →ₗ[Construction.k] Construction.k) (N : ℕ) (s : Fin 3) (x : PaperFiniteCharts.CoeffIndex N → F) : (chartQuadraticData χ N s).eval x = chartEvaluation χ N s x

theorem Connes.PaperChartDetector.chartEvaluation_isQuadratic (χ : ↥C →ₗ[Construction.k] Construction.k) (N : ℕ) (s : Fin 3) : BooleanPolynomial.IsQuadratic (chartEvaluation χ N s)

theorem Connes.PaperChartDetector.quadratic_support_card_bound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (P : (ι → F) → F) (hdeg : BooleanPolynomial.IsQuadratic P) (hP : P ≠ 0) : Fintype.card (ι → F) ≤ 4 * BooleanPolynomial.weightOn P

@[reducible, inline]

abbrev Connes.PaperChartDetector.ChartEvalIndex (N : ℕ) : Type

The ChartEvalIndex construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetector.ChartEvalIndex N = (Fin 3 × (Connes.PaperFiniteCharts.CoeffIndex N → Connes.PaperChartDetector.F))

noncomputable def Connes.PaperChartDetector.chartEvalValue (χ : ↥C →ₗ[Construction.k] Construction.k) (N : ℕ) (i : ChartEvalIndex N) : F

The chartEvalValue construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetector.chartEvalValue χ N i = Connes.PaperChartDetector.chartEvaluation χ N i.1 i.2

noncomputable def Connes.PaperChartDetector.chartEvalSupport (χ : ↥C →ₗ[Construction.k] Construction.k) (N : ℕ) : Finset (ChartEvalIndex N)

The chartEvalSupport construction used in the Connes rigidity formalization.

Equations

• Connes.PaperChartDetector.chartEvalSupport χ N = {i : Connes.PaperChartDetector.ChartEvalIndex N | Connes.PaperChartDetector.chartEvalValue χ N i ≠ 0}

theorem Connes.PaperChartDetector.chart_support_card_bound (χ : ↥C →ₗ[Construction.k] Construction.k) (N : ℕ) (hactive : (chartEvalSupport χ N).Nonempty) : Fintype.card (ChartEvalIndex N) ≤ 12 * (chartEvalSupport χ N).card