Mathematics · proofs · software

Paper IX · Lean source

PolynomialAxiomAudit.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_lifting/verification/PolynomialAxiomAudit.lean106 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/polynomial_lifting/verification/PolynomialAxiomAudit.lean

Skip source text

1 module
2 public import AffineObstructionCore
3 public import PolynomialTaylor
4 public import SharedCorrection
5 public import AffinePairTransport
6 public import PolynomialObstruction
7 public import AffineSharedCorrection
8 public import PolynomialControls
9 public import PolynomialRepresentative
10 public import PolynomialShared
11 public import PolynomialObstructionContract
12 public import PolynomialRepresentativeContract
13 public import PolynomialSharedContract
14 public import PolynomialTaylorContract
15 @[expose] public section
16 #print axioms Komorebi.AffinePair.HasJointLift
17 #print axioms Komorebi.AffinePair.SharedObstruction
18 #print axioms Komorebi.AffinePair.digit_correction_iff_same_image
19 #print axioms Komorebi.AffinePair.finite_affine_pair_compatibility
20 #print axioms Komorebi.AffinePair.joint_lift_iff_class_eq
21 #print axioms Komorebi.AffinePair.joint_lift_iff_compatible_corrections
22 #print axioms Komorebi.AffinePair.joint_lift_iff_digit_correction
23 #print axioms Komorebi.AffinePair.left_class_independent
24 #print axioms Komorebi.AffinePair.next_level_iff_digit
25 #print axioms Komorebi.AffinePair.right_class_independent
26 #print axioms Komorebi.AffinePair.shared_obstruction_finite
27 #print axioms Komorebi.NativeAffine.Obstruction
28 #print axioms Komorebi.NativeAffine.affine_lift_iff_obstruction_zero
29 #print axioms Komorebi.NativeAffine.affine_residual_transport
30 #print axioms Komorebi.NativeAffine.digitMap
31 #print axioms Komorebi.NativeAffine.finite_affine_obstruction
32 #print axioms Komorebi.NativeAffine.obstruction
33 #print axioms Komorebi.NativeAffine.obstruction_finite
34 #print axioms Komorebi.NativeAffine.obstruction_representative_independent
35 #print axioms Komorebi.NativeAffine.obstruction_zero_iff_correction
36 #print axioms Komorebi.NativeAffine.reduction
37 #print axioms Komorebi.NativeAffine.reduction_zero_iff
38 #print axioms Komorebi.NativeAffine.residual_exists
39 #print axioms Komorebi.NativeAffine.same_residue_iff
40 #print axioms Komorebi.PolynomialControls.even_square_cannot_be_two_mod_four
41 #print axioms Komorebi.PolynomialControls.linearTwo
42 #print axioms Komorebi.PolynomialControls.linearZero
43 #print axioms Komorebi.PolynomialControls.no_common_polynomial_lift
44 #print axioms Komorebi.PolynomialControls.separate_polynomial_lifts
45 #print axioms Komorebi.PolynomialControls.singular_root_without_lift
46 #print axioms Komorebi.PolynomialControls.squareMinusTwo
47 #print axioms Komorebi.PolynomialControls.squarePolynomial
48 #print axioms Komorebi.PolynomialControls.zero_depth_taylor_failure
49 #print axioms Komorebi.PolynomialObstruction.dvd_iff_of_dvd_sub
50 #print axioms Komorebi.PolynomialObstruction.evalSystem
51 #print axioms Komorebi.PolynomialObstruction.evalSystem_apply
52 #print axioms Komorebi.PolynomialObstruction.finite_polynomial_obstruction
53 #print axioms Komorebi.PolynomialObstruction.jacobian
54 #print axioms Komorebi.PolynomialObstruction.jacobian_apply
55 #print axioms Komorebi.PolynomialObstruction.next_level_iff_digit
56 #print axioms Komorebi.PolynomialObstruction.polynomial_lift_iff_obstruction_zero
57 #print axioms Komorebi.PolynomialObstruction.polynomial_same_residue_lift_iff
58 #print axioms Komorebi.PolynomialObstruction.residual_exists
59 #print axioms Komorebi.PolynomialObstruction.residual_unique
60 #print axioms Komorebi.PolynomialObstruction.taylor_residual_dvd
61 #print axioms Komorebi.PolynomialObstructionContract.explicit_finite_polynomial_contract
62 #print axioms Komorebi.PolynomialRepresentative.digit_jacobian_eq
63 #print axioms Komorebi.PolynomialRepresentative.digit_jacobian_shift_eq
64 #print axioms Komorebi.PolynomialRepresentative.representative_independence
65 #print axioms Komorebi.PolynomialRepresentative.residual_class_independent
66 #print axioms Komorebi.PolynomialRepresentative.residual_digit_transport
67 #print axioms Komorebi.PolynomialRepresentativeContract.explicit_representative_contract
68 #print axioms Komorebi.PolynomialShared.HasJointLift
69 #print axioms Komorebi.PolynomialShared.SharedObstruction
70 #print axioms Komorebi.PolynomialShared.finite_polynomial_pair_compatibility
71 #print axioms Komorebi.PolynomialShared.joint_lift_iff_class_eq
72 #print axioms Komorebi.PolynomialShared.joint_lift_iff_compatible_corrections
73 #print axioms Komorebi.PolynomialShared.joint_lift_iff_digit_correction
74 #print axioms Komorebi.PolynomialShared.left_class_independent
75 #print axioms Komorebi.PolynomialShared.right_class_independent
76 #print axioms Komorebi.PolynomialShared.shared_obstruction_finite
77 #print axioms Komorebi.PolynomialSharedContract.explicit_shared_polynomial_contract
78 #print axioms Komorebi.PolynomialTaylor.directional
79 #print axioms Komorebi.PolynomialTaylor.directional_C
80 #print axioms Komorebi.PolynomialTaylor.directional_X
81 #print axioms Komorebi.PolynomialTaylor.directional_add
82 #print axioms Komorebi.PolynomialTaylor.directional_mul
83 #print axioms Komorebi.PolynomialTaylor.eval_dvd_of_dvd
84 #print axioms Komorebi.PolynomialTaylor.pderiv_eval_dvd_of_dvd
85 #print axioms Komorebi.PolynomialTaylor.taylor_dvd
86 #print axioms Komorebi.PolynomialTaylor.taylor_step_dvd
87 #print axioms Komorebi.PolynomialTaylorContract.explicit_integral_taylor_contract
88 #print axioms Komorebi.SharedCorrection.Common
89 #print axioms Komorebi.SharedCorrection.commonKernel
90 #print axioms Komorebi.SharedCorrection.common_finite_of_left
91 #print axioms Komorebi.SharedCorrection.common_finite_of_right
92 #print axioms Komorebi.SharedCorrection.common_paired_universal
93 #print axioms Komorebi.SharedCorrection.common_universal
94 #print axioms Komorebi.SharedCorrection.fiber
95 #print axioms Komorebi.SharedCorrection.joint
96 #print axioms Komorebi.SharedCorrection.jointImageEquivFiber
97 #print axioms Komorebi.SharedCorrection.joint_range_eq_fiber
98 #print axioms Komorebi.SharedCorrection.labelJ
99 #print axioms Komorebi.SharedCorrection.labelJ_image
100 #print axioms Komorebi.SharedCorrection.labelJ_surjective
101 #print axioms Komorebi.SharedCorrection.labelK
102 #print axioms Komorebi.SharedCorrection.labelK_image
103 #print axioms Komorebi.SharedCorrection.labelK_surjective
104 #print axioms Komorebi.SharedCorrection.labels_eq_iff_common
105 #print axioms Komorebi.SharedCorrection.mem_fiber
106 #print axioms Komorebi.SharedCorrection.quotient_mk_eq_iff_common

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: 2cd9c1f282d2df67967982ac5372256dfdeb6378b63bf54e00348399ed6ea7ee

Original source on GitHub

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