Concrete §4 A-coordinate detector transport and invariant-measure bound for Zhou's dual kernel. Paper: §4.

@[reducible, inline]

abbrev Connes.PaperAChartDetectorMeasure.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperAChartDetectorMeasure.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperAChartDetectorMeasure.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperAChartDetectorMeasure.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.CharacterSpace = Connes.PaperDualTopology.CharacterSpace

noncomputable def Connes.PaperAChartDetectorMeasure.aCoordinateEmbedding (v : OpenAIPort.SymplecticIndex) : A →ₗ[k] D

The A-coordinate embedding into the first kernel summand. Paper: §4.

Equations

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

noncomputable def Connes.PaperAChartDetectorMeasure.aChartLinear (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) : A →ₗ[k] k

The character's A-coordinate linear functional at one finite dual index. Paper: §4.

Equations

• Connes.PaperAChartDetectorMeasure.aChartLinear χ v = Connes.BinaryPontryaginDual.characterLinear (Additive.toMul χ) ∘ₗ Connes.PaperAChartDetectorMeasure.aCoordinateEmbedding v

noncomputable def Connes.PaperAChartDetectorMeasure.aChartEvaluation (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (s : Fin 3) (x : PaperFiniteCharts.CoeffIndex N → k) : k

The finite polynomial-chart evaluation of an A-coordinate functional. Paper: §4.

Equations

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

noncomputable def Connes.PaperAChartDetectorMeasure.aChartQuadraticData (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (s : Fin 3) : BooleanPolynomial.QuadraticData (PaperFiniteCharts.CoeffIndex N)

The affine coefficient data witnessing the chart evaluation is quadratic. Paper: §4.

Equations

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

theorem Connes.PaperAChartDetectorMeasure.aChartEvaluation_eq_quadraticData_eval (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (s : Fin 3) (x : PaperFiniteCharts.CoeffIndex N → k) : (aChartQuadraticData χ v N s).eval x = aChartEvaluation χ v N s x

The finite A-chart evaluation agrees with its coefficient data. Paper: §4.

theorem Connes.PaperAChartDetectorMeasure.aChartEvaluation_isQuadratic (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (s : Fin 3) : BooleanPolynomial.IsQuadratic (aChartEvaluation χ v N s)

@[reducible, inline]

abbrev Connes.PaperAChartDetectorMeasure.AChartEvalIndex (N : ℕ) : Type

The AChartEvalIndex construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.AChartEvalIndex N = Connes.PaperChartDetector.ChartEvalIndex N

noncomputable def Connes.PaperAChartDetectorMeasure.aChartEvalValue (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (i : AChartEvalIndex N) : k

The value of an A-coordinate functional on an evaluation index. Paper: §4.

Equations

• Connes.PaperAChartDetectorMeasure.aChartEvalValue χ v N i = Connes.PaperAChartDetectorMeasure.aChartEvaluation χ v N i.1 i.2

noncomputable def Connes.PaperAChartDetectorMeasure.aChartEvalSupport (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) : Finset (AChartEvalIndex N)

The nonzero support of one finite A-coordinate evaluation. Paper: §4.

Equations

• Connes.PaperAChartDetectorMeasure.aChartEvalSupport χ v N = {i : Connes.PaperAChartDetectorMeasure.AChartEvalIndex N | Connes.PaperAChartDetectorMeasure.aChartEvalValue χ v N i ≠ 0}

theorem Connes.PaperAChartDetectorMeasure.aChart_support_card_bound (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (hactive : (aChartEvalSupport χ v N).Nonempty) : Fintype.card (AChartEvalIndex N) ≤ 12 * (aChartEvalSupport χ v N).card

The finite A-chart support satisfies the twelve-detector bound. Paper: §4.

def Connes.PaperAChartDetectorMeasure.aDetector (v : OpenAIPort.SymplecticIndex) (a : A) : Set CharacterSpace

The aDetector construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.aDetector v a = Connes.PaperChartMeasure.linearDetector ((Connes.PaperAChartDetectorMeasure.aCoordinateEmbedding v) a)

theorem Connes.PaperAChartDetectorMeasure.mem_aDetector_iff (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (a : A) : χ ∈ aDetector v a ↔ (aChartLinear χ v) a = 1

A-coordinate detector membership is its binary linear value. Paper: §4.

noncomputable def Connes.PaperAChartDetectorMeasure.aChartPoint (N : ℕ) (i : AChartEvalIndex N) : A

The aChartPoint construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.aChartPoint N i = Connes.PaperFiniteCharts.chartPoint N (Connes.PaperChartDetector.chartIndexOfCoefficients N i.1 i.2)

noncomputable def Connes.PaperAChartDetectorMeasure.aDetectorSupport (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) : Finset (AChartEvalIndex N)

The active A-coordinate detector support at one finite level. Paper: §4.

Equations

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

theorem Connes.PaperAChartDetectorMeasure.aDetectorSupport_mem_iff (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (i : AChartEvalIndex N) : i ∈ aDetectorSupport χ v N ↔ i ∈ aChartEvalSupport χ v N

A-coordinate detector support matches chart-evaluation support. Paper: §4.

theorem Connes.PaperAChartDetectorMeasure.aDetectorSupport_card_eq (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) : (aDetectorSupport χ v N).card = (aChartEvalSupport χ v N).card

theorem Connes.PaperAChartDetectorMeasure.aDetectorSupport_card_bound (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (hactive : (aDetectorSupport χ v N).Nonempty) : Fintype.card (AChartEvalIndex N) ≤ 12 * (aDetectorSupport χ v N).card

theorem Connes.PaperAChartDetectorMeasure.paperThetaOne_A_inverse_transport (g : SpecialLinear.SL3) (a : A) (v : OpenAIPort.SymplecticIndex) (he : (Construction.PaperKernel.sl3AAction g) (PaperFiniteCharts.basisVector 0) = a) : (Multiplicative.toAdd (PaperChartDetectorMeasure.paperThetaOneAddAction (g, 1)⁻¹)) (a ⊗ₜ[k] LinearMap.proj v, 0) = (PaperFiniteCharts.basisVector 0 ⊗ₜ[k] LinearMap.proj v, 0)

theorem Connes.PaperAChartDetectorMeasure.aChartDetector_measure_eq_base (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure μ) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (i : PaperFiniteCharts.ChartIndex N) : ↑μ (aDetector v (PaperFiniteCharts.chartPoint N i)) = ↑μ (aDetector v (PaperFiniteCharts.basisVector 0))

noncomputable def Connes.PaperAChartDetectorMeasure.aChartDetectorSupport (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) : Finset (PaperFiniteCharts.ChartIndex N)

The aChartDetectorSupport construction used in the Connes rigidity formalization.

Equations

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

theorem Connes.PaperAChartDetectorMeasure.aChartDetectorSupport_mem_iff (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (i : PaperFiniteCharts.ChartIndex N) : i ∈ aChartDetectorSupport χ v N ↔ (PaperChartDetectorMeasure.chartEvalIndexEquiv N) i ∈ aChartEvalSupport χ v N

Original chart detectors correspond to evaluation supports. Paper: §4.

theorem Connes.PaperAChartDetectorMeasure.aChartDetectorSupport_card_eq (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) : (aChartDetectorSupport χ v N).card = (aChartEvalSupport χ v N).card

theorem Connes.PaperAChartDetectorMeasure.aChartDetectorSupport_card_bound (χ : CharacterSpace) (v : OpenAIPort.SymplecticIndex) (N : ℕ) (hactive : (aChartDetectorSupport χ v N).Nonempty) : Fintype.card (PaperFiniteCharts.ChartIndex N) ≤ 12 * (aChartDetectorSupport χ v N).card

def Connes.PaperAChartDetectorMeasure.aDetectorUnion (v : OpenAIPort.SymplecticIndex) (N : ℕ) : Set CharacterSpace

The aDetectorUnion construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.aDetectorUnion v N = ⋃ (i : Connes.PaperFiniteCharts.ChartIndex N), Connes.PaperAChartDetectorMeasure.aDetector v (Connes.PaperFiniteCharts.chartPoint N i)

theorem Connes.PaperAChartDetectorMeasure.measurableSet_aDetectorUnion (v : OpenAIPort.SymplecticIndex) (N : ℕ) : MeasurableSet (aDetectorUnion v N)

Each finite A-coordinate detector union is measurable. Paper: §4.

theorem Connes.PaperAChartDetectorMeasure.aDetectorUnion_measure_le_twelve (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure μ) (v : OpenAIPort.SymplecticIndex) (N : ℕ) : ↑μ (aDetectorUnion v N) ≤ 12 * ↑μ (aDetector v (PaperFiniteCharts.basisVector 0))

theorem Connes.PaperAChartDetectorMeasure.aChartPoint_extend {N M : ℕ} (hNM : N ≤ M) (i : PaperFiniteCharts.ChartIndex N) : PaperFiniteCharts.chartPoint M (i.1, PaperFiniteCharts.extendCoefficients hNM i.2.1, PaperFiniteCharts.extendCoefficients hNM i.2.2) = PaperFiniteCharts.chartPoint N i

theorem Connes.PaperAChartDetectorMeasure.aDetectorUnion_mono {N M : ℕ} (hNM : N ≤ M) (v : OpenAIPort.SymplecticIndex) : aDetectorUnion v N ⊆ aDetectorUnion v M

noncomputable def Connes.PaperAChartDetectorMeasure.aChartSubmodule (N : ℕ) : Submodule k A

The aChartSubmodule construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.aChartSubmodule N = Submodule.span Connes.PaperAChartDetectorMeasure.k (Set.range (Connes.PaperFiniteCharts.chartPoint N))

theorem Connes.PaperAChartDetectorMeasure.delta_mem_aChartSubmodule {N : ℕ} {c : ↥Construction.PaperKernel.C} (hc : c ∈ PaperFiniteCharts.chartSubmodule N) : Construction.PaperKernel.delta c ∈ aChartSubmodule N

The retraction sends each finite square span into the A-chart span. Paper: §2 and §4.

theorem Connes.PaperAChartDetectorMeasure.aChartVector_mem_some_chart (a : A) : ∃ (N : ℕ), a ∈ aChartSubmodule N

def Connes.PaperAChartDetectorMeasure.aNonzeroLocus (v : OpenAIPort.SymplecticIndex) : Set CharacterSpace

The aNonzeroLocus construction used in the Connes rigidity formalization.

Equations

• Connes.PaperAChartDetectorMeasure.aNonzeroLocus v = {χ : Connes.PaperAChartDetectorMeasure.CharacterSpace | Connes.PaperAChartDetectorMeasure.aChartLinear χ v ≠ 0}

theorem Connes.PaperAChartDetectorMeasure.iUnion_aDetectorUnion_eq_aNonzeroLocus (v : OpenAIPort.SymplecticIndex) : ⋃ (N : ℕ), aDetectorUnion v N = aNonzeroLocus v

theorem Connes.PaperAChartDetectorMeasure.aNonzeroLocus_measureReal_le_twelve (μ : MeasureTheory.ProbabilityMeasure CharacterSpace) (hinv : PaperChartDetectorMeasure.IsInvariantPaperSL3SpectralMeasure μ) (v : OpenAIPort.SymplecticIndex) : (↑μ).real (aNonzeroLocus v) ≤ 12 * (↑μ).real (aDetector v (PaperFiniteCharts.basisVector 0))