KernelAudit.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiVerification.PaperII.NestedRefinement
7 import KomorebiVerification.PaperII.ResidueFourierCRT
8 import KomorebiVerification.PaperII.WeightedTransfer
9 import KomorebiVerification.PaperII.TransferZeta
10 import KomorebiVerification.PaperII.ResultantSeparation
11 import KomorebiVerification.PaperII.SmithDyadic
12 import KomorebiVerification.PaperII.LinearDefects
13 import KomorebiVerification.PaperII.TypedLinearDefects
14 import Mathlib.Util.AssertNoSorry
15 
16 /-!
17 # Paper II kernel audit
18 
19 Author: Komorebi P.
20 
21 This module imports every Paper II theorem module, reports the trusted
22 dependencies of representative public declarations, and then performs a
23 fail-closed namespace-wide audit.  The final audit inspects every imported
24 `Komorebi.*` declaration and rejects placeholders, project axioms, unsafe
25 declarations, or any axiom outside Lean's standard quotient/extensionality/
26 choice basis.
27 -/
28 
29 set_option autoImplicit false
30 
31 /-! ## Nested refinement and exact packet coordinates -/
32 
33 #print axioms Komorebi.PaperII.NestedRefinement.finitePacket_decomposition_unique
34 #print axioms Komorebi.PaperII.NestedRefinement.Refines.trans
35 #print axioms Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv
36 #print axioms Komorebi.PaperII.NestedRefinement.refineCoordinates_comp
37 #print axioms Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv_trans
38 #print axioms Komorebi.PaperII.NestedRefinement.coordinateOperator_comp
39 #print axioms Komorebi.PaperII.NestedRefinement.coordinateOperator_naturality
40 #print axioms Komorebi.PaperII.NestedRefinement.transferBlock_refinement_between
41 #print axioms Komorebi.PaperII.NestedRefinement.transferBlock_refinement_and_reconstruction
42 #print axioms Komorebi.PaperII.NestedRefinement.transferBlock_refinement
43 
44 /-! ## Residue, Fourier, and CRT packets -/
45 
46 #print axioms Komorebi.Residue.polyphase_refinement
47 #print axioms Komorebi.Residue.ringFourierAverage_eq_residueProj_of_certificate
48 #print axioms Komorebi.Residue.FiniteRingFourierOrthogonalityCertificate.toRingCertificate
49 #print axioms Komorebi.Residue.ringFourierAverage_eq_residueProj_of_finite_certificate
50 #print axioms Komorebi.Residue.fourierAverage_eq_residueProj_of_certificate
51 #print axioms Komorebi.Residue.fourierAverage_eq_residueProj_of_primitiveRoot
52 #print axioms Komorebi.Residue.residueProj_crt
53 #print axioms Komorebi.Residue.residueProj_dyadicOdd
54 
55 /-! ## Weighted transfer and finite-precision inversion -/
56 
57 #print axioms Komorebi.PaperII.WeightedTransfer.finiteGeometricInverse_spec_of_pow_eq_zero
58 #print axioms Komorebi.PaperII.WeightedTransfer.analyticDiagonalTransferInverse_spec
59 #print axioms Komorebi.PaperII.WeightedTransfer.map_eq_pruned_of_wordExpansion
60 #print axioms Komorebi.PaperII.WeightedTransfer.map_finiteGeometricInverse_eq_prunedWordInverse
61 #print axioms Komorebi.PaperII.WeightedTransfer.prunedWordInverse_spec_of_minWeight
62 #print axioms Komorebi.PaperII.WeightedTransfer.finitePrecisionPrunedInverse_of_weightedEdges
63 #print axioms Komorebi.PaperII.WeightedTransfer.finitePrecisionInverse_of_weightedEdges
64 #print axioms Komorebi.PaperII.WeightedTransfer.finitePrecisionPrunedDiagonalTransferInverse_of_minWeight
65 #print axioms Komorebi.PaperII.WeightedTransfer.finitePrecisionPrunedDiagonalTransferInverse_of_weightedEdges
66 #print axioms Komorebi.PaperII.WeightedTransfer.le_mul_ceilDiv
67 #print axioms Komorebi.PaperII.WeightedTransfer.finitePrecisionDiagonalTransferInverse_of_weightedEdges
68 
69 /-! ## Transfer-zeta coefficients and rationality certificates -/
70 
71 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.coefficientAlgorithm_correct
72 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.coefficientAlgorithm_eq_card_exactWalk
73 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.coefficientAlgorithm_firstEdge
74 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.weightedAdjacency_coeff
75 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.enumeratedPathZetaMatrix_eq_matrixPathZetaMatrix
76 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.pathZeta_eq_matrixPathZeta
77 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.transferDenominator_mul_pathZeta
78 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.finite_graph_constant_coefficient_recurrence
79 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.finite_graph_pathZeta_rationality
80 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.finite_graph_transferZeta_trace
81 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.pathZetaAlgorithm_trace
82 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.RationalCertificate.certificate_explicit_rationality
83 #print axioms Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.RationalCertificate.constant_coefficient_recurrence
84 
85 /-! ## Resultant-controlled separation -/
86 
87 #print axioms Komorebi.PaperII.ResultantSeparation.separatorNumerator_mul_self_of_bezout
88 #print axioms Komorebi.PaperII.ResultantSeparation.separator_idempotent_of_bezout
89 #print axioms Komorebi.PaperII.ResultantSeparation.separator_idempotent
90 #print axioms Komorebi.PaperII.ResultantSeparation.scalar_mul_separator_preservesLattice
91 #print axioms Komorebi.PaperII.ResultantSeparation.pow_smul_separator_eq_unit_inv_smul_separatorNumerator
92 #print axioms Komorebi.PaperII.ResultantSeparation.separationWeight_clears
93 #print axioms Komorebi.PaperII.ResultantSeparation.separationWeight_le_of_clears
94 #print axioms Komorebi.PaperII.ResultantSeparation.IsSeparationWeight.mono
95 #print axioms Komorebi.PaperII.ResultantSeparation.separator_isSeparationWeight_of_unit_mul_pow_eq_of_inv_preserves
96 #print axioms Komorebi.PaperII.ResultantSeparation.separator_separationWeight_le_of_unit_mul_pow_eq
97 #print axioms Komorebi.PaperII.ResultantSeparation.separator_isSeparationWeight_of_pow_eq
98 #print axioms Komorebi.PaperII.ResultantSeparation.separator_separationWeight_le_of_pow_eq
99 #print axioms Komorebi.PaperII.ResultantSeparation.projector_precision_delay
100 
101 /-! ## Smith fibres and dyadic separation -/
102 
103 #print axioms Komorebi.PaperII.SmithDyadic.smithZModFiber_nonempty_iff
104 #print axioms Komorebi.PaperII.SmithDyadic.smithZModFiber_card_of_admissible
105 #print axioms Komorebi.PaperII.SmithDyadic.smithZMod_global_solvable_iff
106 #print axioms Komorebi.PaperII.SmithDyadic.smithZMod_global_conditional_count
107 #print axioms Komorebi.PaperII.SmithDyadic.global_solvable_iff_coordinatewise
108 #print axioms Komorebi.PaperII.SmithDyadic.smith_conditional_product_count
109 #print axioms Komorebi.PaperII.SmithDyadic.positiveSignProjector_pIntegral_of_prime_ne_two
110 #print axioms Komorebi.PaperII.SmithDyadic.positiveSignProjector_exact_dyadic_weight
111 #print axioms Komorebi.PaperII.SmithDyadic.positiveSignProjector_exact_pLocal_weight_zero_of_prime_ne_two
112 #print axioms Komorebi.PaperII.SmithDyadic.signFactors_resultant
113 #print axioms Komorebi.PaperII.SmithDyadic.signProjectors_resultant_dyadic_weight_endpoint
114 #print axioms Komorebi.PaperII.SmithDyadic.oddAdicVersusDyadicSignBehavior_trace
115 #print axioms Komorebi.PaperII.SmithDyadic.padicValNat_two_at_odd_prime
116 #print axioms Komorebi.PaperII.SmithDyadic.smithPhase_neg_one_eq_inv
117 
118 /-! ## Linear refinement defects -/
119 
120 #print axioms Komorebi.PaperII.LinearDefects.power_defect_identity_all
121 #print axioms Komorebi.PaperII.LinearDefects.norm_power_defect_le
122 #print axioms Komorebi.PaperII.LinearDefects.inverse_sandwich_identity
123 #print axioms Komorebi.PaperII.LinearDefects.resolvent_defect_identity
124 
125 /-! ## Typed linear refinement defects -/
126 
127 #print axioms Komorebi.PaperII.TypedLinearDefects.power_defect_identity_all
128 #print axioms Komorebi.PaperII.TypedLinearDefects.powers_compatible_of_defect_eq_zero
129 #print axioms Komorebi.PaperII.TypedLinearDefects.polynomialAction_compatible_of_defect_eq_zero
130 #print axioms Komorebi.PaperII.TypedLinearDefects.continuous_norm_power_defect_le
131 #print axioms Komorebi.PaperII.TypedLinearDefects.continuous_norm_power_defect_le_geometric_majorant
132 #print axioms Komorebi.PaperII.TypedLinearDefects.scalarShift_resolvent_identity
133 #print axioms Komorebi.PaperII.TypedLinearDefects.resolvents_compatible_of_defect_eq_zero
134 #print axioms Komorebi.PaperII.TypedLinearDefects.continuous_scalarShift_resolvent_identity
135 #print axioms Komorebi.PaperII.TypedLinearDefects.continuous_norm_resolvent_defect_le
136 #print axioms Komorebi.PaperII.TypedLinearDefects.continuous_resolvents_compatible_of_defect_eq_zero
137 
138 /-! ## Fail-closed namespace audit -/
139 
140 open Lean Meta Elab Command
141 
142 /-
143 Audit every declaration in the imported `Komorebi` namespace.  Unlike the
144 human-readable `#print axioms` sample above, this command fails compilation if
145 any declaration depends on `sorryAx`, a project-specific axiom, or any axiom
146 outside the explicitly allowed Lean basis.  It also rejects unsafe
147 declarations.
148 -/
149 run_cmd do
150   let env ← getEnv
151   let mut audited : Nat := 0
152   for (name, info) in env.checked.get.constants.toList do
153     if Name.isPrefixOf `Komorebi name then
154       audited := audited + 1
155       if info.isUnsafe then
156         throwError "unsafe project declaration: {name}"
157       let axioms ← Lean.collectAxioms name
158       for axiomName in axioms do
159         unless axiomName == ``propext || axiomName == ``Classical.choice ||
160             axiomName == ``Quot.sound do
161           throwError "unexpected axiom {axiomName} in project declaration {name}"
162   if audited == 0 then
163     throwError "kernel audit found no Komorebi declarations"
164   logInfo m!"FAIL-CLOSED KERNEL AUDIT PASS: {audited} Komorebi declarations; allowed axioms only: propext, Classical.choice, Quot.sound"

Back to source controls