Mathematics · proofs · software

Paper IX · Lean source

PolynomialTowersAxiomAudit.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_towers/verification/PolynomialTowersAxiomAudit.lean146 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/polynomial_towers/verification/PolynomialTowersAxiomAudit.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 PadicTowerLimitContract
17 public import PolynomialPadicLiftContract
18 public import PolynomialTowerContract
19 @[expose] public section
20 #print axioms Komorebi.FiniteFiberCounts.Fiber
21 #print axioms Komorebi.FiniteFiberCounts.cokernel_card
22 #print axioms Komorebi.FiniteFiberCounts.cokernel_finrank
23 #print axioms Komorebi.FiniteFiberCounts.difference
24 #print axioms Komorebi.FiniteFiberCounts.difference_translate
25 #print axioms Komorebi.FiniteFiberCounts.fiberAddTorsor
26 #print axioms Komorebi.FiniteFiberCounts.fiberEquivKernel
27 #print axioms Komorebi.FiniteFiberCounts.fiber_card
28 #print axioms Komorebi.FiniteFiberCounts.fiber_card_eq_kernel
29 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_empty
30 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_nonempty
31 #print axioms Komorebi.FiniteFiberCounts.fiber_nonempty_iff_class_zero
32 #print axioms Komorebi.FiniteFiberCounts.kernel_card
33 #print axioms Komorebi.FiniteFiberCounts.kernel_finrank
34 #print axioms Komorebi.FiniteFiberCounts.rank
35 #print axioms Komorebi.FiniteFiberCounts.translate
36 #print axioms Komorebi.FiniteFiberCounts.translate_add
37 #print axioms Komorebi.FiniteFiberCounts.translate_difference
38 #print axioms Komorebi.FiniteFiberCounts.translate_exists_unique
39 #print axioms Komorebi.FiniteFiberCounts.translate_zero
40 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv
41 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_mk
42 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_obstruction
43 #print axioms Komorebi.IntegerFiniteCokernel.cokernel_card_eq
44 #print axioms Komorebi.IntegerFiniteCokernel.digit_range_eq_restrict
45 #print axioms Komorebi.IntegerFiniteCokernel.reduction_surjective
46 #print axioms Komorebi.NativeAffine.Obstruction
47 #print axioms Komorebi.NativeAffine.affine_lift_iff_obstruction_zero
48 #print axioms Komorebi.NativeAffine.affine_residual_transport
49 #print axioms Komorebi.NativeAffine.digitMap
50 #print axioms Komorebi.NativeAffine.finite_affine_obstruction
51 #print axioms Komorebi.NativeAffine.obstruction
52 #print axioms Komorebi.NativeAffine.obstruction_finite
53 #print axioms Komorebi.NativeAffine.obstruction_representative_independent
54 #print axioms Komorebi.NativeAffine.obstruction_zero_iff_correction
55 #print axioms Komorebi.NativeAffine.reduction
56 #print axioms Komorebi.NativeAffine.reduction_zero_iff
57 #print axioms Komorebi.NativeAffine.residual_exists
58 #print axioms Komorebi.NativeAffine.same_residue_iff
59 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_cauchy
60 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_limit
61 #print axioms Komorebi.PadicTowerLimit.compatible_int_tower_unique_limit
62 #print axioms Komorebi.PadicTowerLimit.compatible_vector_tower_limit
63 #print axioms Komorebi.PadicTowerLimit.divisible_int_tendsto_zero
64 #print axioms Komorebi.PadicTowerLimit.tower_pair_dvd
65 #print axioms Komorebi.PadicTowerLimitContract.explicit_vector_limit
66 #print axioms Komorebi.PolynomialDigitBridge.DigitSolutions
67 #print axioms Komorebi.PolynomialDigitBridge.digitJacobian
68 #print axioms Komorebi.PolynomialDigitBridge.digit_solution_iff
69 #print axioms Komorebi.PolynomialDigitBridge.digit_solutions_nonempty_iff
70 #print axioms Komorebi.PolynomialDigitBridge.integerLift
71 #print axioms Komorebi.PolynomialDigitBridge.reduction_integerLift
72 #print axioms Komorebi.PolynomialDigitBridge.reduction_jacobian
73 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower
74 #print axioms Komorebi.PolynomialIntegerTower.exists_compatible_tower_strong
75 #print axioms Komorebi.PolynomialIntegerTower.tower_digitJacobian_eq
76 #print axioms Komorebi.PolynomialIntegerTower.tower_initial_congruent
77 #print axioms Komorebi.PolynomialIntegerTower.tower_pairwise_congruent
78 #print axioms Komorebi.PolynomialLiftCounts.ActualLifts
79 #print axioms Komorebi.PolynomialLiftCounts.digitAddTorsor
80 #print axioms Komorebi.PolynomialLiftCounts.digitEquivLifts
81 #print axioms Komorebi.PolynomialLiftCounts.digit_residue_solution_iff
82 #print axioms Komorebi.PolynomialLiftCounts.finite_polynomial_lift_count
83 #print axioms Komorebi.PolynomialLiftCounts.liftEquivKernel
84 #print axioms Komorebi.PolynomialLiftCounts.lift_card
85 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv
86 #print axioms Komorebi.PolynomialLiftCounts.obstructionEquiv_class
87 #print axioms Komorebi.PolynomialLiftCounts.obstruction_card
88 #print axioms Komorebi.PolynomialObstruction.dvd_iff_of_dvd_sub
89 #print axioms Komorebi.PolynomialObstruction.evalSystem
90 #print axioms Komorebi.PolynomialObstruction.evalSystem_apply
91 #print axioms Komorebi.PolynomialObstruction.finite_polynomial_obstruction
92 #print axioms Komorebi.PolynomialObstruction.jacobian
93 #print axioms Komorebi.PolynomialObstruction.jacobian_apply
94 #print axioms Komorebi.PolynomialObstruction.next_level_iff_digit
95 #print axioms Komorebi.PolynomialObstruction.polynomial_lift_iff_obstruction_zero
96 #print axioms Komorebi.PolynomialObstruction.polynomial_same_residue_lift_iff
97 #print axioms Komorebi.PolynomialObstruction.residual_exists
98 #print axioms Komorebi.PolynomialObstruction.residual_unique
99 #print axioms Komorebi.PolynomialObstruction.taylor_residual_dvd
100 #print axioms Komorebi.PolynomialPadicLift.continuous_padicEval
101 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root
102 #print axioms Komorebi.PolynomialPadicLift.exists_padic_root_with_tower
103 #print axioms Komorebi.PolynomialPadicLift.padicEval
104 #print axioms Komorebi.PolynomialPadicLift.padicEval_intCast
105 #print axioms Komorebi.PolynomialPadicLift.polynomial_tower_limit_root
106 #print axioms Komorebi.PolynomialPadicLiftContract.explicit_padic_root
107 #print axioms Komorebi.PolynomialPadicLiftContract.explicit_padic_root_with_tower
108 #print axioms Komorebi.PolynomialSmoothCounts.exists_regular_tower
109 #print axioms Komorebi.PolynomialSmoothCounts.smooth_dimension
110 #print axioms Komorebi.PolynomialSmoothCounts.smooth_lift_card
111 #print axioms Komorebi.PolynomialSmoothCounts.smooth_obstruction_card
112 #print axioms Komorebi.PolynomialSmoothCounts.smooth_rank
113 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_eq
114 #print axioms Komorebi.PolynomialSurjectiveStep.digitJacobian_shift_eq
115 #print axioms Komorebi.PolynomialSurjectiveStep.one_step_lift
116 #print axioms Komorebi.PolynomialTaylor.directional
117 #print axioms Komorebi.PolynomialTaylor.directional_C
118 #print axioms Komorebi.PolynomialTaylor.directional_X
119 #print axioms Komorebi.PolynomialTaylor.directional_add
120 #print axioms Komorebi.PolynomialTaylor.directional_mul
121 #print axioms Komorebi.PolynomialTaylor.eval_dvd_of_dvd
122 #print axioms Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd
123 #print axioms Komorebi.PolynomialTaylor.taylor_dvd
124 #print axioms Komorebi.PolynomialTaylor.taylor_step_dvd
125 #print axioms Komorebi.PolynomialTowerContract.explicit_jacobian
126 #print axioms Komorebi.PolynomialTowerContract.explicit_polynomial_tower
127 #print axioms Komorebi.PolynomialTowerControls.linearMinusTwo
128 #print axioms Komorebi.PolynomialTowerControls.linear_shift_no_extra_precision
129 #print axioms Komorebi.PolynomialTowerControls.linear_shift_nonsingular_lower_root
130 #print axioms Komorebi.PolynomialTowerControls.projectionSystem
131 #print axioms Komorebi.PolynomialTowerControls.projection_jacobian_surjective
132 #print axioms Komorebi.PolynomialTowerControls.projection_two_padic_roots
133 #print axioms Komorebi.PolynomialTowerControls.squareMinusFive
134 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_lower_steps
135 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_mod_eight
136 #print axioms Komorebi.PolynomialTowerControls.square_minus_five_no_tower
137 #print axioms Komorebi.ResidueLiftDigits.ResidueFiber
138 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue
139 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue_apply
140 #print axioms Komorebi.ResidueLiftDigits.digitResidue
141 #print axioms Komorebi.ResidueLiftDigits.digitResidue_injective
142 #print axioms Komorebi.ResidueLiftDigits.digitResidue_mem
143 #print axioms Komorebi.ResidueLiftDigits.digitResidue_surjective
144 #print axioms Komorebi.ResidueLiftDigits.next_modulus_dvd_val_sub_shift
145 #print axioms Komorebi.ResidueLiftDigits.residueFiber_card
146 #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: d1cb33cc994012492d4c3992663ac21e59eb66aba60491b3a6aa4bb5d807bc1c

Original source on GitHub

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