Finite detector sets for the raw Zhou split extensions. Paper: §4.

@[reducible, inline]

abbrev Connes.PaperSpectralFiniteDetection.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralFiniteDetection.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperSpectralFiniteDetection.A : Type

The A construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralFiniteDetection.A = Connes.Construction.A

@[reducible, inline]

abbrev Connes.PaperSpectralFiniteDetection.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralFiniteDetection.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperSpectralFiniteDetection.VStar : Type

The VStar construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralFiniteDetection.VStar = Connes.Construction.PaperKernel.VStar

@[reducible, inline]

abbrev Connes.PaperSpectralFiniteDetection.SymplecticIndex : Type

The SymplecticIndex construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralFiniteDetection.SymplecticIndex = Connes.OpenAIPort.SymplecticIndex

def Connes.PaperSpectralFiniteDetection.aZeroCoeff : A →ₗ[k] k

The aZeroCoeff construction used in the Connes rigidity formalization.

Equations

• Connes.PaperSpectralFiniteDetection.aZeroCoeff = { toFun := fun (a : Connes.PaperSpectralFiniteDetection.A) => Polynomial.constantCoeff (a 0), map_add' := ⋯, map_smul' := ⋯ }

theorem Connes.PaperSpectralFiniteDetection.aZeroCoeff_basisVector_zero : aZeroCoeff (PaperFiniteCharts.basisVector 0) = 1

The coefficient functional takes the base chart vector to one. Paper: §4.

theorem Connes.PaperSpectralFiniteDetection.aCoordinateEmbedding_injective : Function.Injective fun (v : SymplecticIndex) => (PaperAChartDetectorMeasure.aCoordinateEmbedding v) (PaperFiniteCharts.basisVector 0)

noncomputable def Connes.PaperSpectralFiniteDetection.aDetectorEmbedding : SymplecticIndex ↪ D

The aDetectorEmbedding construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperSpectralFiniteDetection.cDetector : D

The C-coordinate detector singled out by the paper's five-detector bound. Paper: §4.

Equations

• Connes.PaperSpectralFiniteDetection.cDetector = (0, Connes.Construction.PaperKernel.diagonal (Connes.PaperFiniteCharts.basisVector 0))

noncomputable def Connes.PaperSpectralFiniteDetection.aDetectorImage : Finset D

The finite A-detector image used by the five-detector set. Paper: §4.

Equations

• Connes.PaperSpectralFiniteDetection.aDetectorImage = Finset.image (⇑Connes.PaperSpectralFiniteDetection.aDetectorEmbedding) Finset.univ

noncomputable def Connes.PaperSpectralFiniteDetection.detectorFinset : Finset D

The explicit finite detector set for both raw split extensions. Paper: §4.

Equations

• Connes.PaperSpectralFiniteDetection.detectorFinset = insert Connes.PaperSpectralFiniteDetection.cDetector Connes.PaperSpectralFiniteDetection.aDetectorImage

theorem Connes.PaperSpectralFiniteDetection.basisVector_zero_ne_zero : PaperFiniteCharts.basisVector 0 ≠ 0

The standard A chart vector is nonzero. Paper: §4.

theorem Connes.PaperSpectralFiniteDetection.diagonal_basisVector_zero_ne_zero : Construction.PaperKernel.diagonal (PaperFiniteCharts.basisVector 0) ≠ 0

theorem Connes.PaperSpectralFiniteDetection.cDetector_not_mem_image : cDetector ∉ aDetectorImage

theorem Connes.PaperSpectralFiniteDetection.detectorFinset_sum_eq (f : D → ℝ) : ∑ d ∈ detectorFinset, f d = ∑ v : SymplecticIndex, f ((PaperAChartDetectorMeasure.aCoordinateEmbedding v) (PaperFiniteCharts.basisVector 0)) + f cDetector

theorem Connes.PaperSpectralFiniteDetection.spectralDetectionEnergy_nonneg (μ : MeasureTheory.ProbabilityMeasure (DiscreteCharacterSpace Construction.PaperKernel.D)) (d : D) : 0 ≤ spectralDetectionEnergy μ d

theorem Connes.PaperSpectralFiniteDetection.lambda_one_hasFiniteSpectralDetection : HasFiniteSpectralDetection PaperSpectralPropertyT.lambdaOneExtension detectorFinset (1 / 3)

theorem Connes.PaperSpectralFiniteDetection.lambda_two_hasFiniteSpectralDetection : HasFiniteSpectralDetection PaperSpectralPropertyT.lambdaTwoExtension detectorFinset (1 / 3)

noncomputable def Connes.PaperSpectralFiniteDetection.lambdaOneSpectralData : PaperSpectralPropertyT.SpectralData Construction.PaperKernel.paperThetaOneHom

The lambdaOneSpectralData construction used in the Connes rigidity formalization.

Equations

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

noncomputable def Connes.PaperSpectralFiniteDetection.lambdaTwoSpectralData : PaperSpectralPropertyT.SpectralData Construction.PaperKernel.paperThetaTwoHom

Package the proved detector set for the second split extension. Paper: §4.

Equations

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