Mathematics · proofs · software

Paper IX · Lean source

PolynomialDeformationAxiomAudit.lean

Selected results recorded Coverage and evidence

Compiler/replay evidence is reported for a subset or bounded block. No whole-work coverage is implied.

This viewer reads the retained source; it does not run Lean or assign new claim mappings.

polynomial_deformation/verification/PolynomialDeformationAxiomAudit.lean182 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/polynomial_deformation/verification/PolynomialDeformationAxiomAudit.lean

Skip source text

1 module
2 public import AffineObstructionCore
3 public import FiniteFiberCounts
4 public import PadicTowerLimit
5 public import PolynomialTaylor
6 public import ResidueLiftDigits
7 public import IntegerFiniteCokernel
8 public import PolynomialObstruction
9 public import PolynomialDigitBridge
10 public import PolynomialLiftCounts
11 public import PolynomialSurjectiveStep
12 public import PolynomialIntegerTower
13 public import PolynomialSmoothCounts
14 public import PolynomialTowerControls
15 public import PolynomialPadicLift
16 public import PolynomialCoefficientPerturbation
17 public import PolynomialPadicUnique
18 public import PolynomialRootStability
19 public import PolynomialDeformationControls
20 public import PolynomialCoefficientPerturbationContract
21 public import PolynomialPadicUniqueContract
22 public import PolynomialRootStabilityContract
23 @[expose] public section
24 #print axioms Komorebi.FiniteFiberCounts.Fiber
25 #print axioms Komorebi.FiniteFiberCounts.cokernel_card
26 #print axioms Komorebi.FiniteFiberCounts.cokernel_finrank
27 #print axioms Komorebi.FiniteFiberCounts.difference
28 #print axioms Komorebi.FiniteFiberCounts.difference_translate
29 #print axioms Komorebi.FiniteFiberCounts.fiberAddTorsor
30 #print axioms Komorebi.FiniteFiberCounts.fiberEquivKernel
31 #print axioms Komorebi.FiniteFiberCounts.fiber_card
32 #print axioms Komorebi.FiniteFiberCounts.fiber_card_eq_kernel
33 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_empty
34 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_nonempty
35 #print axioms Komorebi.FiniteFiberCounts.fiber_nonempty_iff_class_zero
36 #print axioms Komorebi.FiniteFiberCounts.kernel_card
37 #print axioms Komorebi.FiniteFiberCounts.kernel_finrank
38 #print axioms Komorebi.FiniteFiberCounts.rank
39 #print axioms Komorebi.FiniteFiberCounts.translate
40 #print axioms Komorebi.FiniteFiberCounts.translate_add
41 #print axioms Komorebi.FiniteFiberCounts.translate_difference
42 #print axioms Komorebi.FiniteFiberCounts.translate_exists_unique
43 #print axioms Komorebi.FiniteFiberCounts.translate_zero
44 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv
45 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_mk
46 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_obstruction
47 #print axioms Komorebi.IntegerFiniteCokernel.cokernel_card_eq
48 #print axioms Komorebi.IntegerFiniteCokernel.digit_range_eq_restrict
49 #print axioms Komorebi.IntegerFiniteCokernel.reduction_surjective
50 #print axioms Komorebi.NativeAffine.Obstruction
51 #print axioms Komorebi.NativeAffine.affine_lift_iff_obstruction_zero
52 #print axioms Komorebi.NativeAffine.affine_residual_transport
53 #print axioms Komorebi.NativeAffine.digitMap
54 #print axioms Komorebi.NativeAffine.finite_affine_obstruction
55 #print axioms Komorebi.NativeAffine.obstruction
56 #print axioms Komorebi.NativeAffine.obstruction_finite
57 #print axioms Komorebi.NativeAffine.obstruction_representative_independent
58 #print axioms Komorebi.NativeAffine.obstruction_zero_iff_correction
59 #print axioms Komorebi.NativeAffine.reduction
60 #print axioms Komorebi.NativeAffine.reduction_zero_iff
61 #print axioms Komorebi.NativeAffine.residual_exists
62 #print axioms Komorebi.NativeAffine.same_residue_iff
63 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_cauchy
64 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_limit
65 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_unique_limit
66 #print axioms Komorebi.PadicTowerLimit.compatible_vector_tower_limit
67 #print axioms Komorebi.PadicTowerLimit.divisible_int_tendsto_zero
68 #print axioms Komorebi.PadicTowerLimit.tower_pair_dvd
69 #print axioms Komorebi.PolynomialCoefficientPerturbation.digitJacobian_perturb_eq
70 #print axioms Komorebi.PolynomialCoefficientPerturbation.digitJacobian_perturb_point_eq
71 #print axioms Komorebi.PolynomialCoefficientPerturbation.evalSystem_perturb
72 #print axioms Komorebi.PolynomialCoefficientPerturbation.exists_padic_root_perturb
73 #print axioms Komorebi.PolynomialCoefficientPerturbation.exists_padic_root_power_perturb
74 #print axioms Komorebi.PolynomialCoefficientPerturbation.lower_root_perturb
75 #print axioms Komorebi.PolynomialCoefficientPerturbation.padicEval_perturb
76 #print axioms Komorebi.PolynomialCoefficientPerturbation.pderiv_perturb
77 #print axioms Komorebi.PolynomialCoefficientPerturbation.perturb
78 #print axioms Komorebi.PolynomialCoefficientPerturbationContract.explicit_perturbed_jacobian
79 #print axioms Komorebi.PolynomialCoefficientPerturbationContract.explicit_power_perturbation_root
80 #print axioms Komorebi.PolynomialDeformationControls.linear_shift_coefficient_perturbation
81 #print axioms Komorebi.PolynomialDeformationControls.linear_shift_no_extra_padic_precision
82 #print axioms Komorebi.PolynomialDeformationControls.squareMinusOne
83 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_jacobian_bijective
84 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_not_global_unique
85 #print axioms Komorebi.PolynomialDeformationControls.square_minus_one_two_padic_roots
86 #print axioms Komorebi.PolynomialDigitBridge.DigitSolutions
87 #print axioms Komorebi.PolynomialDigitBridge.digitJacobian
88 #print axioms Komorebi.PolynomialDigitBridge.digit_solution_iff
89 #print axioms Komorebi.PolynomialDigitBridge.digit_solutions_nonempty_iff
90 #print axioms Komorebi.PolynomialDigitBridge.integerLift
91 #print axioms Komorebi.PolynomialDigitBridge.reduction_integerLift
92 #print axioms Komorebi.PolynomialDigitBridge.reduction_jacobian
93 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower
94 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower_strong
95 #print axioms Komorebi.PolynomialIntegerTower.tower_digitJacobian_eq
96 #print axioms Komorebi.PolynomialIntegerTower.tower_initial_congruent
97 #print axioms Komorebi.PolynomialIntegerTower.tower_pairwise_congruent
98 #print axioms Komorebi.PolynomialLiftCounts.ActualLifts
99 #print axioms Komorebi.PolynomialLiftCounts.digitAddTorsor
100 #print axioms Komorebi.PolynomialLiftCounts.digitEquivLifts
101 #print axioms Komorebi.PolynomialLiftCounts.digit_residue_solution_iff
102 #print axioms Komorebi.PolynomialLiftCounts.finite_polynomial_lift_count
103 #print axioms Komorebi.PolynomialLiftCounts.liftEquivKernel
104 #print axioms Komorebi.PolynomialLiftCounts.lift_card
105 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv
106 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv_class
107 #print axioms Komorebi.PolynomialLiftCounts.obstruction_card
108 #print axioms Komorebi.PolynomialObstruction.dvd_iff_of_dvd_sub
109 #print axioms Komorebi.PolynomialObstruction.evalSystem
110 #print axioms Komorebi.PolynomialObstruction.evalSystem_apply
111 #print axioms Komorebi.PolynomialObstruction.finite_polynomial_obstruction
112 #print axioms Komorebi.PolynomialObstruction.jacobian
113 #print axioms Komorebi.PolynomialObstruction.jacobian_apply
114 #print axioms Komorebi.PolynomialObstruction.next_level_iff_digit
115 #print axioms Komorebi.PolynomialObstruction.polynomial_lift_iff_obstruction_zero
116 #print axioms Komorebi.PolynomialObstruction.polynomial_same_residue_lift_iff
117 #print axioms Komorebi.PolynomialObstruction.residual_exists
118 #print axioms Komorebi.PolynomialObstruction.residual_unique
119 #print axioms Komorebi.PolynomialObstruction.taylor_residual_dvd
120 #print axioms Komorebi.PolynomialPadicLift.continuous_padicEval
121 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root
122 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root_with_tower
123 #print axioms Komorebi.PolynomialPadicLift.padicEval
124 #print axioms Komorebi.PolynomialPadicLift.padicEval_intCast
125 #print axioms Komorebi.PolynomialPadicLift.polynomial_tower_limit_root
126 #print axioms Komorebi.PolynomialPadicUnique.exists_unique_padic_root
127 #print axioms Komorebi.PolynomialPadicUnique.int_pow_dvd_iff
128 #print axioms Komorebi.PolynomialPadicUnique.padic_root_unique
129 #print axioms Komorebi.PolynomialPadicUnique.rootResidueLift
130 #print axioms Komorebi.PolynomialPadicUnique.root_next_residue_eq
131 #print axioms Komorebi.PolynomialPadicUnique.toZModPow_eq_iff_dvd_sub
132 #print axioms Komorebi.PolynomialPadicUnique.truncInt
133 #print axioms Komorebi.PolynomialPadicUnique.truncInt_eval_residue
134 #print axioms Komorebi.PolynomialPadicUnique.truncInt_precision
135 #print axioms Komorebi.PolynomialPadicUnique.truncInt_root
136 #print axioms Komorebi.PolynomialPadicUniqueContract.explicit_arbitrary_root_uniqueness
137 #print axioms Komorebi.PolynomialPadicUniqueContract.explicit_unique_padic_root
138 #print axioms Komorebi.PolynomialRootStability.exists_nearby_perturbed_root
139 #print axioms Komorebi.PolynomialRootStability.exists_root_and_unique_perturbation
140 #print axioms Komorebi.PolynomialRootStability.exists_unique_nearby_perturbed_root
141 #print axioms Komorebi.PolynomialRootStability.integer_congruent_of_common_padic
142 #print axioms Komorebi.PolynomialRootStability.perturbed_roots_congruent
143 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_lower_root_and_unique_perturbation
144 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_rectangular_nearby_root
145 #print axioms Komorebi.PolynomialRootStabilityContract.explicit_square_root_displacement
146 #print axioms Komorebi.PolynomialSmoothCounts.exists_regular_tower
147 #print axioms Komorebi.PolynomialSmoothCounts.smooth_dimension
148 #print axioms Komorebi.PolynomialSmoothCounts.smooth_lift_card
149 #print axioms Komorebi.PolynomialSmoothCounts.smooth_obstruction_card
150 #print axioms Komorebi.PolynomialSmoothCounts.smooth_rank
151 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_eq
152 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_shift_eq
153 #print axioms Komorebi.PolynomialSurjectiveStep.one_step_lift
154 #print axioms Komorebi.PolynomialTaylor.directional
155 #print axioms Komorebi.PolynomialTaylor.directional_C
156 #print axioms Komorebi.PolynomialTaylor.directional_X
157 #print axioms Komorebi.PolynomialTaylor.directional_add
158 #print axioms Komorebi.PolynomialTaylor.directional_mul
159 #print axioms Komorebi.PolynomialTaylor.eval_dvd_of_dvd
160 #print axioms Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd
161 #print axioms Komorebi.PolynomialTaylor.taylor_dvd
162 #print axioms Komorebi.PolynomialTaylor.taylor_step_dvd
163 #print axioms Komorebi.PolynomialTowerControls.linearMinusTwo
164 #print axioms Komorebi.PolynomialTowerControls.linear_shift_no_extra_precision
165 #print axioms Komorebi.PolynomialTowerControls.linear_shift_nonsingular_lower_root
166 #print axioms Komorebi.PolynomialTowerControls.projectionSystem
167 #print axioms Komorebi.PolynomialTowerControls.projection_jacobian_surjective
168 #print axioms Komorebi.PolynomialTowerControls.projection_two_padic_roots
169 #print axioms Komorebi.PolynomialTowerControls.squareMinusFive
170 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_lower_steps
171 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_mod_eight
172 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_tower
173 #print axioms Komorebi.ResidueLiftDigits.ResidueFiber
174 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue
175 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue_apply
176 #print axioms Komorebi.ResidueLiftDigits.digitResidue
177 #print axioms Komorebi.ResidueLiftDigits.digitResidue_injective
178 #print axioms Komorebi.ResidueLiftDigits.digitResidue_mem
179 #print axioms Komorebi.ResidueLiftDigits.digitResidue_surjective
180 #print axioms Komorebi.ResidueLiftDigits.next_modulus_dvd_val_sub_shift
181 #print axioms Komorebi.ResidueLiftDigits.residueFiber_card
182 #print axioms Komorebi.ResidueLiftDigits.shift_cast_eq_iff

Back to source controls

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: 88d8d69efd005f2e439f46ad85a7c2e1329568b1d2bc6f223fc40e05d9e92bf0

Original source on GitHub

Back to Paper IX: Arithmetic Packets, Dyadic Towers, and Local Polynomial Deformation