LeanPool.ConnesRigidity.Paper.Section4.ChartSpan

source

@[reducible, inline]

abbrev Connes.PaperChartSpan.k :

Type

The k construction used in the Connes rigidity formalization.

Equations

Connes.PaperChartSpan.k = Connes.Construction.k

Instances For

source

@[reducible, inline]

abbrev Connes.PaperChartSpan.R :

Type

The R construction used in the Connes rigidity formalization.

Equations

Connes.PaperChartSpan.R = Connes.Construction.R

Instances For

source

@[reducible, inline]

abbrev Connes.PaperChartSpan.A :

Type

The A construction used in the Connes rigidity formalization.

Equations

Connes.PaperChartSpan.A = Connes.Construction.A

Instances For

source

@[reducible, inline]

abbrev Connes.PaperChartSpan.C :

Submodule Construction.k Construction.PaperKernel.TensorAA

The C construction used in the Connes rigidity formalization.

Equations

Connes.PaperChartSpan.C = Connes.Construction.PaperKernel.C

Instances For

source

theorem Connes.PaperChartSpan.diagonal_chartVector_mem_of_mem (N : ℕ) (s : Fin 3) (f h : R) (hf : f ∈ PaperFiniteCharts.polynomialChart N) (hh : h ∈ PaperFiniteCharts.polynomialChart N) :

Construction.PaperKernel.diagonal (PaperFiniteCharts.chartVector s f h) ∈ PaperFiniteCharts.chartSubmodule N

source

theorem Connes.PaperChartSpan.zero_mem_polynomialChart (N : ℕ) :

0 ∈ PaperFiniteCharts.polynomialChart N

The zero polynomial occurs at every finite chart level. Paper: §4.

source

theorem Connes.PaperChartSpan.one_mem_polynomialChart_one :

1 ∈ PaperFiniteCharts.polynomialChart 1

The constant polynomial is represented at the first positive chart level. Paper: §4.

source

theorem Connes.PaperChartSpan.one_mem_polynomialChart {N : ℕ} (hN : 0 < N) :

1 ∈ PaperFiniteCharts.polynomialChart N

The constant polynomial persists under chart enlargement. Paper: §4.

source

theorem Connes.PaperChartSpan.next_cycle (s : Fin 3) :

PaperFiniteCharts.next (PaperFiniteCharts.nextNext s) = s

The cyclic coordinate successor closes after two steps. Paper: §4.

source

theorem Connes.PaperChartSpan.nextNext_cycle (s : Fin 3) :

PaperFiniteCharts.nextNext (PaperFiniteCharts.nextNext s) = PaperFiniteCharts.next s

The second cyclic successor reduces to the remaining coordinate. Paper: §4.

source

A characteristic-two six-square identity isolates one diagonal coordinate. Paper: §4.

source

theorem Connes.PaperChartSpan.diagonal_smul_basis_mem (N : ℕ) (hN : 0 < N) (s : Fin 3) (f : R) (hf : f ∈ PaperFiniteCharts.polynomialChart N) :

Construction.PaperKernel.diagonal (f • PaperFiniteCharts.basisVector (PaperFiniteCharts.next s)) ∈ PaperFiniteCharts.chartSubmodule N

A bounded scalar multiple of a coordinate diagonal lies in a finite chart span. Paper: §4.

source

theorem Connes.PaperChartSpan.diagonal_smul_basis_any_mem (N : ℕ) (hN : 0 < N) (i : Fin 3) (f : R) (hf : f ∈ PaperFiniteCharts.polynomialChart N) :

Construction.PaperKernel.diagonal (f • PaperFiniteCharts.basisVector i) ∈ PaperFiniteCharts.chartSubmodule N

Every coordinate diagonal has the same finite-chart membership property. Paper: §4.

source

theorem Connes.PaperChartSpan.cross_distinct_identity (s : Fin 3) (f h : R) :

A cross term on two distinct coordinates expands into four chart squares. Paper: §4.

source

theorem Connes.PaperChartSpan.cross_distinct_mem (N : ℕ) (s : Fin 3) (f h : R) (hf : f ∈ PaperFiniteCharts.polynomialChart N) (hh : h ∈ PaperFiniteCharts.polynomialChart N) :

PaperChartDetector.cross (f • PaperFiniteCharts.basisVector (PaperFiniteCharts.next s)) (h • PaperFiniteCharts.basisVector (PaperFiniteCharts.nextNext s)) ∈ PaperFiniteCharts.chartSubmodule N

source

A same-coordinate cross term reduces to three diagonal squares. Paper: §4.

source

theorem Connes.PaperChartSpan.cross_same_mem (N : ℕ) (hN : 0 < N) (i : Fin 3) (f h : R) (hf : f ∈ PaperFiniteCharts.polynomialChart N) (hh : h ∈ PaperFiniteCharts.polynomialChart N) (hfh : f + h ∈ PaperFiniteCharts.polynomialChart N) :

PaperChartDetector.cross (f • PaperFiniteCharts.basisVector i) (h • PaperFiniteCharts.basisVector i) ∈ PaperFiniteCharts.chartSubmodule N

Same-coordinate cross terms with bounded coefficients lie in a finite chart span. Paper: §4.

source

theorem Connes.PaperChartSpan.cross_add_left (a b c : A) :

PaperChartDetector.cross (a + b) c = PaperChartDetector.cross a c + PaperChartDetector.cross b c

The symmetric cross term is additive in its left input. Paper: §4.

source

theorem Connes.PaperChartSpan.cross_add_right (a b c : A) :

PaperChartDetector.cross a (b + c) = PaperChartDetector.cross a b + PaperChartDetector.cross a c

The symmetric cross term is additive in its right input. Paper: §4.

source

A diagonal tensor decomposes into coordinate diagonals and pairwise cross terms. Paper: §4.

source

theorem Connes.PaperChartSpan.cross_comm (a b : A) :

PaperChartDetector.cross a b = PaperChartDetector.cross b a

The symmetric cross term is invariant under exchanging its inputs. Paper: §4.

source

theorem Connes.PaperChartSpan.cross_scalar_basis_ne_mem (N : ℕ) (i j : Fin 3) (hij : i ≠ j) (f h : R) (hf : f ∈ PaperFiniteCharts.polynomialChart N) (hh : h ∈ PaperFiniteCharts.polynomialChart N) :

PaperChartDetector.cross (f • PaperFiniteCharts.basisVector i) (h • PaperFiniteCharts.basisVector j) ∈ PaperFiniteCharts.chartSubmodule N

Every bounded cross term on distinct standard coordinates is chart-generated. Paper: §4.

source

theorem Connes.PaperChartSpan.diagonal_mem_chart_of_coeff (N : ℕ) (hN : 0 < N) (a : A) (h0 : a 0 ∈ PaperFiniteCharts.polynomialChart N) (h1 : a 1 ∈ PaperFiniteCharts.polynomialChart N) (h2 : a 2 ∈ PaperFiniteCharts.polynomialChart N) :

Construction.PaperKernel.diagonal a ∈ PaperFiniteCharts.chartSubmodule N

A vector with bounded coordinates has its diagonal in one finite chart span. Paper: §4.

source

theorem Connes.PaperChartSpan.polynomial_mem_chart_succ (p : R) :

p ∈ PaperFiniteCharts.polynomialChart (Polynomial.natDegree p + 1)

A polynomial is represented by a finite coefficient chart. Paper: §4.

source

theorem Connes.PaperChartSpan.diagonal_mem_some_chart (a : A) :

∃ (N : ℕ), Construction.PaperKernel.diagonal a ∈ PaperFiniteCharts.chartSubmodule N

Every vector diagonal is captured by a finite chart span. Paper: §4.

source

theorem Connes.PaperChartSpan.span_has_chart (x : Construction.PaperKernel.TensorAA) (hx : x ∈ Construction.PaperKernel.squareSpan) :

(TensorProduct.comm k A A) x = x ∧ ∃ (N : ℕ) (c : ↥C), ↑c = x ∧ c ∈ PaperFiniteCharts.chartSubmodule N

The square span has symmetry and finite-chart witnesses. Paper: §2 and §4.

source

theorem Connes.PaperChartSpan.diagonal_mem_chart_some_level (c : ↥C) :

∃ (N : ℕ), c ∈ PaperFiniteCharts.chartSubmodule N

Every fixed tensor-module element is captured by a finite chart span. Paper: §2 and §4.