Mathematics · proofs · software

Paper IX · Lean source

SharedAxiomAudit.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.

shared_correction/verification/SharedAxiomAudit.lean70 lines

Original source pathpreserved/PRSC_IX_Consolidated_Manuscript/shared_correction/verification/SharedAxiomAudit.lean

Skip source text

1 module
2 public import SharedCorrection
3 public import AffineObstructionCore
4 public import AffinePairTransport
5 public import AffineSharedCorrection
6 public import SharedCorrectionControls
7 public import AffinePairControls
8 public import SharedCorrectionContract
9 public import AffinePairContract
10 @[expose] public section
11 #print axioms Komorebi.AffinePair.HasJointLift
12 #print axioms Komorebi.AffinePair.SharedObstruction
13 #print axioms Komorebi.AffinePair.digit_correction_iff_same_image
14 #print axioms Komorebi.AffinePair.finite_affine_pair_compatibility
15 #print axioms Komorebi.AffinePair.joint_lift_iff_class_eq
16 #print axioms Komorebi.AffinePair.joint_lift_iff_compatible_corrections
17 #print axioms Komorebi.AffinePair.joint_lift_iff_digit_correction
18 #print axioms Komorebi.AffinePair.left_class_independent
19 #print axioms Komorebi.AffinePair.next_level_iff_digit
20 #print axioms Komorebi.AffinePair.right_class_independent
21 #print axioms Komorebi.AffinePair.shared_obstruction_finite
22 #print axioms Komorebi.AffinePairControls.composite_level_zero
23 #print axioms Komorebi.AffinePairControls.incompatible_mod_four
24 #print axioms Komorebi.AffinePairControls.modulus_one
25 #print axioms Komorebi.AffinePairControls.oneId
26 #print axioms Komorebi.AffinePairControls.two_individual_lifts
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.SharedCorrection.Common
41 #print axioms Komorebi.SharedCorrection.commonKernel
42 #print axioms Komorebi.SharedCorrection.common_finite_of_left
43 #print axioms Komorebi.SharedCorrection.common_finite_of_right
44 #print axioms Komorebi.SharedCorrection.common_paired_universal
45 #print axioms Komorebi.SharedCorrection.common_universal
46 #print axioms Komorebi.SharedCorrection.fiber
47 #print axioms Komorebi.SharedCorrection.joint
48 #print axioms Komorebi.SharedCorrection.jointImageEquivFiber
49 #print axioms Komorebi.SharedCorrection.joint_range_eq_fiber
50 #print axioms Komorebi.SharedCorrection.labelJ
51 #print axioms Komorebi.SharedCorrection.labelJ_image
52 #print axioms Komorebi.SharedCorrection.labelJ_surjective
53 #print axioms Komorebi.SharedCorrection.labelK
54 #print axioms Komorebi.SharedCorrection.labelK_image
55 #print axioms Komorebi.SharedCorrection.labelK_surjective
56 #print axioms Komorebi.SharedCorrection.labels_eq_iff_common
57 #print axioms Komorebi.SharedCorrection.mem_fiber
58 #print axioms Komorebi.SharedCorrection.quotient_mk_eq_iff_common
59 #print axioms Komorebi.SharedCorrectionContract.explicit_quotient_contract
60 #print axioms Komorebi.SharedCorrectionControls.Two
61 #print axioms Komorebi.SharedCorrectionControls.evaluateCoordinate
62 #print axioms Komorebi.SharedCorrectionControls.identical_maps_distinguish_targets
63 #print axioms Komorebi.SharedCorrectionControls.identity
64 #print axioms Komorebi.SharedCorrectionControls.independent_joint_range_top
65 #print axioms Komorebi.SharedCorrectionControls.independent_targets_have_equal_labels
66 #print axioms Komorebi.SharedCorrectionControls.leftCoordinate
67 #print axioms Komorebi.SharedCorrectionControls.rightCoordinate
68 #print axioms Komorebi.SharedCorrectionControls.separately_solvable_but_incompatible
69 #print axioms Komorebi.SharedCorrectionControls.sequence_domain_common_finite
70 #print axioms Komorebi.SharedCorrectionControls.zero_left_identifies_all

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: 6abef285160a23f53fc1247376b9a92d560703a1a675843ba067354bed9b1d8c

Original source on GitHub

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