Mathematics · proofs · software

Paper IX · Lean source

PolynomialCountsAxiomAudit.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_counts/verification/PolynomialCountsAxiomAudit.lean120 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/polynomial_counts/verification/PolynomialCountsAxiomAudit.lean

Skip source text

1 module
2 public import AffineObstructionCore
3 public import FiniteFiberCounts
4 public import PolynomialTaylor
5 public import ResidueLiftDigits
6 public import IntegerFiniteCokernel
7 public import PolynomialObstruction
8 public import PolynomialDigitBridge
9 public import PolynomialLiftCounts
10 public import PolynomialCountControls
11 public import FiniteFiberCountsContract
12 public import PolynomialLiftCountContract
13 public import ResidueDigitsContract
14 @[expose] public section
15 #print axioms Komorebi.FiniteFiberCounts.Fiber
16 #print axioms Komorebi.FiniteFiberCounts.cokernel_card
17 #print axioms Komorebi.FiniteFiberCounts.cokernel_finrank
18 #print axioms Komorebi.FiniteFiberCounts.difference
19 #print axioms Komorebi.FiniteFiberCounts.difference_translate
20 #print axioms Komorebi.FiniteFiberCounts.fiberAddTorsor
21 #print axioms Komorebi.FiniteFiberCounts.fiberEquivKernel
22 #print axioms Komorebi.FiniteFiberCounts.fiber_card
23 #print axioms Komorebi.FiniteFiberCounts.fiber_card_eq_kernel
24 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_empty
25 #print axioms Komorebi.FiniteFiberCounts.fiber_card_of_nonempty
26 #print axioms Komorebi.FiniteFiberCounts.fiber_nonempty_iff_class_zero
27 #print axioms Komorebi.FiniteFiberCounts.kernel_card
28 #print axioms Komorebi.FiniteFiberCounts.kernel_finrank
29 #print axioms Komorebi.FiniteFiberCounts.rank
30 #print axioms Komorebi.FiniteFiberCounts.translate
31 #print axioms Komorebi.FiniteFiberCounts.translate_add
32 #print axioms Komorebi.FiniteFiberCounts.translate_difference
33 #print axioms Komorebi.FiniteFiberCounts.translate_exists_unique
34 #print axioms Komorebi.FiniteFiberCounts.translate_zero
35 #print axioms Komorebi.FiniteFiberCountsContract.explicit_fiber_and_obstruction_counts
36 #print axioms Komorebi.FiniteFiberCountsContract.explicit_free_transitive
37 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv
38 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_mk
39 #print axioms Komorebi.IntegerFiniteCokernel.cokernelEquiv_obstruction
40 #print axioms Komorebi.IntegerFiniteCokernel.cokernel_card_eq
41 #print axioms Komorebi.IntegerFiniteCokernel.digit_range_eq_restrict
42 #print axioms Komorebi.IntegerFiniteCokernel.reduction_surjective
43 #print axioms Komorebi.NativeAffine.Obstruction
44 #print axioms Komorebi.NativeAffine.affine_lift_iff_obstruction_zero
45 #print axioms Komorebi.NativeAffine.affine_residual_transport
46 #print axioms Komorebi.NativeAffine.digitMap
47 #print axioms Komorebi.NativeAffine.finite_affine_obstruction
48 #print axioms Komorebi.NativeAffine.obstruction
49 #print axioms Komorebi.NativeAffine.obstruction_finite
50 #print axioms Komorebi.NativeAffine.obstruction_representative_independent
51 #print axioms Komorebi.NativeAffine.obstruction_zero_iff_correction
52 #print axioms Komorebi.NativeAffine.reduction
53 #print axioms Komorebi.NativeAffine.reduction_zero_iff
54 #print axioms Komorebi.NativeAffine.residual_exists
55 #print axioms Komorebi.NativeAffine.same_residue_iff
56 #print axioms Komorebi.PolynomialCountControls.linearSystem
57 #print axioms Komorebi.PolynomialCountControls.linear_digit_count
58 #print axioms Komorebi.PolynomialCountControls.linear_lift_count
59 #print axioms Komorebi.PolynomialCountControls.obstructed_square_digit_count
60 #print axioms Komorebi.PolynomialCountControls.obstructed_square_lift_count
61 #print axioms Komorebi.PolynomialCountControls.singular_square_digit_count
62 #print axioms Komorebi.PolynomialCountControls.singular_square_lift_count
63 #print axioms Komorebi.PolynomialCountControls.squareMinusTwo
64 #print axioms Komorebi.PolynomialCountControls.squareSystem
65 #print axioms Komorebi.PolynomialCountControls.unrestricted_zero_root_count
66 #print axioms Komorebi.PolynomialCountControls.zeroSystem
67 #print axioms Komorebi.PolynomialCountControls.zero_digit_count
68 #print axioms Komorebi.PolynomialCountControls.zero_lift_count
69 #print axioms Komorebi.PolynomialDigitBridge.DigitSolutions
70 #print axioms Komorebi.PolynomialDigitBridge.digitJacobian
71 #print axioms Komorebi.PolynomialDigitBridge.digit_solution_iff
72 #print axioms Komorebi.PolynomialDigitBridge.digit_solutions_nonempty_iff
73 #print axioms Komorebi.PolynomialDigitBridge.integerLift
74 #print axioms Komorebi.PolynomialDigitBridge.reduction_integerLift
75 #print axioms Komorebi.PolynomialDigitBridge.reduction_jacobian
76 #print axioms Komorebi.PolynomialLiftCountContract.explicit_actual_polynomial_count
77 #print axioms Komorebi.PolynomialLiftCountContract.explicit_jacobian_formula
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.PolynomialTaylor.directional
101 #print axioms Komorebi.PolynomialTaylor.directional_C
102 #print axioms Komorebi.PolynomialTaylor.directional_X
103 #print axioms Komorebi.PolynomialTaylor.directional_add
104 #print axioms Komorebi.PolynomialTaylor.directional_mul
105 #print axioms Komorebi.PolynomialTaylor.eval_dvd_of_dvd
106 #print axioms Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd
107 #print axioms Komorebi.PolynomialTaylor.taylor_dvd
108 #print axioms Komorebi.PolynomialTaylor.taylor_step_dvd
109 #print axioms Komorebi.ResidueDigitsContract.explicit_residue_digit_equivalence
110 #print axioms Komorebi.ResidueDigitsContract.explicit_residue_digit_formula
111 #print axioms Komorebi.ResidueLiftDigits.ResidueFiber
112 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue
113 #print axioms Komorebi.ResidueLiftDigits.digitEquivResidue_apply
114 #print axioms Komorebi.ResidueLiftDigits.digitResidue
115 #print axioms Komorebi.ResidueLiftDigits.digitResidue_injective
116 #print axioms Komorebi.ResidueLiftDigits.digitResidue_mem
117 #print axioms Komorebi.ResidueLiftDigits.digitResidue_surjective
118 #print axioms Komorebi.ResidueLiftDigits.next_modulus_dvd_val_sub_shift
119 #print axioms Komorebi.ResidueLiftDigits.residueFiber_card
120 #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: bb67daf4bbb8fd8fe56e7d5b0a5b2757b08d4525a4ba38cab6f097bac8949f6a

Original source on GitHub

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