Paper X · Lean source
IdealClassQuantitativeGeometry.lean
Declared contract recorded Coverage and evidence
The cited release explicitly reports completion of its registered formal contract, under its exact hypotheses.
This viewer reads the retained source; it does not run Lean or assign new claim mappings.
Local imports (3)
PaperX/IdealClassQuantitativeGeometry.lean48 lines
Original source path
current_continuation/lean/PaperX/IdealClassQuantitativeGeometry.leanSkip declarations and read code
1 import PaperX.IdealClassQuantitativeTransfer
2 import PaperX.LatticeCountingTransport
3 import PaperX.CountingBoundaryTransport
4
5 /-! Actual geometric hypotheses for counting the lattice of a nonzero integral ideal. -/
6 set_option autoImplicit false
7 noncomputable section
8
9 open Ideal MeasureTheory Module
10 open scoped nonZeroDivisors Real Classical
11 open NumberField NumberField.InfinitePlace NumberField.mixedEmbedding
12 open NumberField.mixedEmbedding.euclidean NumberField.mixedEmbedding.fundamentalCone
13
14 namespace PaperX.IdealClassQuantitative
15
16 variable (K : Type*) [Field K] [NumberField K]
17
18 /-- The actual Euclidean norm cone is bounded. -/
19 theorem coneRegion_one_bounded : Bornology.IsBounded (coneRegion K 1) := by
20 rw [coneRegion_one]
21 exact (toMixed K).antilipschitz.isBounded_preimage (isBounded_normLeOne K)
22
23 /-- The actual Euclidean norm cone is measurable. -/
24 theorem coneRegion_one_measurable : MeasurableSet (coneRegion K 1) := by
25 rw [coneRegion_one]
26 exact (toMixed K).continuous.measurable (measurableSet_normLeOne K)
27
28 /-- An integral ideal lattice has exactly the number-field degree many basis vectors. -/
29 theorem ideal_basis_card {J : (Ideal (𝓞 K))⁰} {ι : Type*} [Fintype ι]
30 (b : Basis ι ℤ (idealEuclideanLattice K J)) :
31 Fintype.card ι = Module.finrank ℚ K := by
32 rw [← Module.finrank_eq_card_basis b, ZLattice.rank ℝ, euclidean.finrank]
33
34 /-- The actual cone admits a dimension-correct finite boundary atlas in coordinates
35 of any integral basis of the actual ideal lattice. -/
36 theorem ideal_cone_boundaryAtlas (J : (Ideal (𝓞 K))⁰) {ι : Type*} [Fintype ι]
37 (b : Basis ι ℤ (idealEuclideanLattice K J)) :
38 Nonempty (PaperX.LatticeCounting.LipschitzBoundaryAtlas ι
39 (PaperX.LatticeCountingTransport.coordinates (idealEuclideanLattice K J) b ''
40 coneRegion K 1)) := by
41 let e := (toMixed K).symm.trans
42 (PaperX.LatticeCountingTransport.coordinates (idealEuclideanLattice K J) b)
43 have h := PaperX.CountingBoundaryPolar.nonempty_boundaryAtlas_image K e (ideal_basis_card K b)
44 convert h using 1
45 rw [coneRegion_one, ← (toMixed K).image_symm_eq_preimage, ← Set.image_comp]
46 rfl
47
48 end PaperX.IdealClassQuantitative
Original file and source record
This copy matches the recorded source file. Its publication here does not change the work’s review status.
SHA-256: 53a504fbf697e9eff949d0709e75ed2f28e96514a29e54309d6a74023daad91a
Back to Paper X: Universal Residual Seeds and Conditional Occupied-System Completion