ReleaseAudit.lean

1 import KomorebiVerification.PaperII.CommonRefinementConsumers
2 import KomorebiVerification.PaperII
3 
4 section ReleaseAudit
5 open Lean Meta Elab Command
6 set_option maxHeartbeats 8000000
7 run_cmd do
8   let env ← getEnv
9   let targets : Array Name := #[
10     `Komorebi.Foundation.LinearProjectorFamily.exactPacketCoordinates,
11     `Komorebi.Foundation.LinearProjectorFamily.rangeAnalysis_rangeSynthesis,
12     `Komorebi.Foundation.LinearProjectorFamily.rangeSynthesis_rangeAnalysis,
13     `Komorebi.PaperII.LinearDefects.norm_power_defect_le,
14     `Komorebi.PaperII.LinearDefects.norm_power_defect_le_raw,
15     `Komorebi.PaperII.LinearDefects.power_defect_identity_all,
16     `Komorebi.PaperII.LinearDefects.resolvent_defect_identity,
17     `Komorebi.PaperII.NestedRefinement.Refines,
18     `Komorebi.PaperII.NestedRefinement.Refines.child_decomposition_unique,
19     `Komorebi.PaperII.NestedRefinement.Refines.coarse_comp_fine_eq_self,
20     `Komorebi.PaperII.NestedRefinement.Refines.coarse_comp_fine_eq_zero,
21     `Komorebi.PaperII.NestedRefinement.Refines.coarse_packet_reconstruction,
22     `Komorebi.PaperII.NestedRefinement.Refines.coarsenCoordinates_component,
23     `Komorebi.PaperII.NestedRefinement.Refines.fine_comp_coarse_eq_self,
24     `Komorebi.PaperII.NestedRefinement.Refines.fine_comp_coarse_eq_zero,
25     `Komorebi.PaperII.NestedRefinement.Refines.refineCoordinates_component,
26     `Komorebi.PaperII.NestedRefinement.Refines.trans,
27     `Komorebi.PaperII.NestedRefinement.children,
28     `Komorebi.PaperII.NestedRefinement.coarsenCoordinates,
29     `Komorebi.PaperII.NestedRefinement.coarsenCoordinates_refineCoordinates,
30     `Komorebi.PaperII.NestedRefinement.coordinateOperator,
31     `Komorebi.PaperII.NestedRefinement.coordinateOperator_comp,
32     `Komorebi.PaperII.NestedRefinement.coordinateOperator_naturality,
33     `Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv,
34     `Komorebi.PaperII.NestedRefinement.coordinateRefinementEquiv_trans,
35     `Komorebi.PaperII.NestedRefinement.finitePacket_decomposition_ext,
36     `Komorebi.PaperII.NestedRefinement.finitePacket_decomposition_unique,
37     `Komorebi.PaperII.NestedRefinement.mem_children,
38     `Komorebi.PaperII.NestedRefinement.refineCoordinates,
39     `Komorebi.PaperII.NestedRefinement.refineCoordinates_coarsenCoordinates,
40     `Komorebi.PaperII.NestedRefinement.refineCoordinates_comp,
41     `Komorebi.PaperII.NestedRefinement.refineCoordinates_self,
42     `Komorebi.PaperII.NestedRefinement.transferBlock_refinement,
43     `Komorebi.PaperII.NestedRefinement.transferBlock_refinement_and_reconstruction,
44     `Komorebi.PaperII.NestedRefinement.transferBlock_refinement_between,
45     `Komorebi.PaperII.ResultantSeparation.CongruentModLattice,
46     `Komorebi.PaperII.ResultantSeparation.EvaluatedBezoutCertificate,
47     `Komorebi.PaperII.ResultantSeparation.IsLatticeUnit,
48     `Komorebi.PaperII.ResultantSeparation.IsSeparationWeight,
49     `Komorebi.PaperII.ResultantSeparation.IsSeparationWeight.mono,
50     `Komorebi.PaperII.ResultantSeparation.ScalarPreservesLattice,
51     `Komorebi.PaperII.ResultantSeparation.pow_smul_separator_eq_unit_inv_smul_separatorNumerator,
52     `Komorebi.PaperII.ResultantSeparation.projector_precision_delay,
53     `Komorebi.PaperII.ResultantSeparation.scalar_mul_separator_of_ne_zero,
54     `Komorebi.PaperII.ResultantSeparation.scalar_mul_separator_preservesLattice_of_ne_zero,
55     `Komorebi.PaperII.ResultantSeparation.separationWeight,
56     `Komorebi.PaperII.ResultantSeparation.separationWeight_clears,
57     `Komorebi.PaperII.ResultantSeparation.separationWeight_le_of_clears,
58     `Komorebi.PaperII.ResultantSeparation.separatorNumerator_apply_of_mem_ker_F_of_bezout,
59     `Komorebi.PaperII.ResultantSeparation.separatorNumerator_eq_scalar_sub_of_bezout,
60     `Komorebi.PaperII.ResultantSeparation.separatorNumerator_mul_self_of_bezout,
61     `Komorebi.PaperII.ResultantSeparation.separator_apply_of_mem_ker_F_of_bezout,
62     `Komorebi.PaperII.ResultantSeparation.separator_apply_of_mem_ker_G,
63     `Komorebi.PaperII.ResultantSeparation.separator_hasFiniteSeparationWeight_of_eq_unit_mul_pow,
64     `Komorebi.PaperII.ResultantSeparation.separator_idempotent_of_bezout,
65     `Komorebi.PaperII.ResultantSeparation.separator_isSeparationWeight_of_unit_mul_pow_eq_of_inv_preserves,
66     `Komorebi.PaperII.ResultantSeparation.separator_separationWeight_le_of_eq_unit_mul_pow,
67     `Komorebi.PaperII.SmithDyadic.HasExactPLocalDenominatorWeight,
68     `Komorebi.PaperII.SmithDyadic.SmithCardinalityCertificate,
69     `Komorebi.PaperII.SmithDyadic.SmithSolvabilityCertificate,
70     `Komorebi.PaperII.SmithDyadic.SmithZModAdmissible,
71     `Komorebi.PaperII.SmithDyadic.negativeSignProjector_exact_pLocal_weight_zero_of_prime_ne_two,
72     `Komorebi.PaperII.SmithDyadic.negativeSignProjector_idempotent,
73     `Komorebi.PaperII.SmithDyadic.oddAdicVersusDyadicSignBehavior_trace,
74     `Komorebi.PaperII.SmithDyadic.padicValNat_two_at_odd_prime,
75     `Komorebi.PaperII.SmithDyadic.positiveSignProjector_exact_pLocal_weight_zero_of_prime_ne_two,
76     `Komorebi.PaperII.SmithDyadic.positiveSignProjector_idempotent,
77     `Komorebi.PaperII.SmithDyadic.signFactors_resultant,
78     `Komorebi.PaperII.SmithDyadic.signInvolution_mul_self,
79     `Komorebi.PaperII.SmithDyadic.signProjectors_complete,
80     `Komorebi.PaperII.SmithDyadic.signProjectors_resultant_dyadic_weight_endpoint,
81     `Komorebi.PaperII.SmithDyadic.smithPhase,
82     `Komorebi.PaperII.SmithDyadic.smithPhase_neg_one_eq_inv,
83     `Komorebi.PaperII.SmithDyadic.smithZModCoordinateCertificate,
84     `Komorebi.PaperII.SmithDyadic.smithZModFiber_card_of_admissible,
85     `Komorebi.PaperII.SmithDyadic.smithZModFiber_nonempty_iff,
86     `Komorebi.PaperII.SmithDyadic.smithZModMulHom,
87     `Komorebi.PaperII.SmithDyadic.smithZMod_global_conditional_count,
88     `Komorebi.PaperII.SmithDyadic.smithZMod_global_solvable_iff,
89     `Komorebi.PaperII.SmithDyadic.smith_conditional_product_count,
90     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.RationalCertificate.certificate_explicit_rationality,
91     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.RationalCertificate.constant_coefficient_recurrence,
92     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.coefficientAlgorithm,
93     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.coefficientAlgorithm_correct,
94     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.coefficientAlgorithm_firstEdge,
95     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.enumeratedPathZetaMatrix_eq_matrixPathZetaMatrix,
96     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.exactWalkFirstEdgeEquiv,
97     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.finite_graph_constant_coefficient_recurrence,
98     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.finite_graph_pathZeta_rationality,
99     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.finite_graph_transferZeta_trace,
100     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.mem_walkTuplesAtWeight_iff,
101     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.pathZetaAlgorithm_trace,
102     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.pathZeta_eq_inverse_mul_transferNumerator,
103     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.pathZeta_eq_matrixPathZeta,
104     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.transferDenominator,
105     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.transferDenominator_coeff_zero,
106     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.transferDenominator_mul_pathZeta,
107     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.transferMatrix,
108     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.transferNumerator,
109     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.tuple_captured_iff,
110     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.walkTuplesAtWeight,
111     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.weightedAdjacency,
112     `Komorebi.PaperII.TransferZeta.PositiveWeightedMultigraph.weightedAdjacency_coeff,
113     `Komorebi.PaperII.TypedLinearDefects.TwoSidedInverse,
114     `Komorebi.PaperII.TypedLinearDefects.continuousDefect,
115     `Komorebi.PaperII.TypedLinearDefects.continuousPolynomialAction_compatible_of_defect_eq_zero,
116     `Komorebi.PaperII.TypedLinearDefects.continuousScalarShift,
117     `Komorebi.PaperII.TypedLinearDefects.continuous_end_pow_norm_le,
118     `Komorebi.PaperII.TypedLinearDefects.continuous_norm_power_defect_le,
119     `Komorebi.PaperII.TypedLinearDefects.continuous_norm_power_defect_le_geometric_majorant,
120     `Komorebi.PaperII.TypedLinearDefects.continuous_norm_resolvent_defect_le,
121     `Komorebi.PaperII.TypedLinearDefects.continuous_power_defect_identity_all,
122     `Komorebi.PaperII.TypedLinearDefects.continuous_resolvents_compatible_of_defect_eq_zero,
123     `Komorebi.PaperII.TypedLinearDefects.continuous_scalarShift_resolvent_identity,
124     `Komorebi.PaperII.TypedLinearDefects.defect,
125     `Komorebi.PaperII.TypedLinearDefects.polynomialAction,
126     `Komorebi.PaperII.TypedLinearDefects.polynomialAction_compatible_of_defect_eq_zero,
127     `Komorebi.PaperII.TypedLinearDefects.power_defect_identity,
128     `Komorebi.PaperII.TypedLinearDefects.power_defect_identity_all,
129     `Komorebi.PaperII.TypedLinearDefects.powers_compatible_of_defect_eq_zero,
130     `Komorebi.PaperII.TypedLinearDefects.resolvents_compatible_of_defect_eq_zero,
131     `Komorebi.PaperII.TypedLinearDefects.scalarShift_resolvent_identity,
132     `Komorebi.PaperII.WeightedTransfer.MultiplicativeFiltration,
133     `Komorebi.PaperII.WeightedTransfer.PrecisionCertificate,
134     `Komorebi.PaperII.WeightedTransfer.TwoSidedInverse,
135     `Komorebi.PaperII.WeightedTransfer.analyticDiagonalTransferInverse_spec,
136     `Komorebi.PaperII.WeightedTransfer.analyticGeometricInverse_spec,
137     `Komorebi.PaperII.WeightedTransfer.diagonalTransferInverse_spec,
138     `Komorebi.PaperII.WeightedTransfer.finiteGeometricInverse,
139     `Komorebi.PaperII.WeightedTransfer.finiteGeometricInverse_spec_of_pow_eq_zero,
140     `Komorebi.PaperII.WeightedTransfer.finitePrecisionPrunedDiagonalTransferInverse_of_minWeight,
141     `Komorebi.PaperII.WeightedTransfer.finitePrecisionPrunedDiagonalTransferInverse_of_weightedEdges,
142     `Komorebi.PaperII.WeightedTransfer.finitePrecisionPrunedInverse_of_weightedEdges,
143     `Komorebi.PaperII.WeightedTransfer.le_mul_ceilDiv,
144     `Komorebi.PaperII.WeightedTransfer.map_finiteGeometricInverse_eq_prunedWordInverse,
145     `Komorebi.PaperII.WeightedTransfer.map_sum_pow_eq_zero_at_scaled_cutoff,
146     `Komorebi.PaperII.WeightedTransfer.minWeight_mul_length_le_wordWeight,
147     `Komorebi.PaperII.WeightedTransfer.prunedDiagonalTransferInverse,
148     `Komorebi.PaperII.WeightedTransfer.prunedWordInverse,
149     `Komorebi.PaperII.WeightedTransfer.prunedWordInverse_spec_of_minWeight,
150     `Komorebi.PaperII.WeightedTransfer.retainedFixedWordSum,
151     `Komorebi.Residue.FiniteRingFourierOrthogonalityCertificate,
152     `Komorebi.Residue.FiniteRingFourierOrthogonalityCertificate.toRingCertificate,
153     `Komorebi.Residue.crtComponents_bijective,
154     `Komorebi.Residue.crtEquiv,
155     `Komorebi.Residue.dyadicOddComponents_bijective,
156     `Komorebi.Residue.dyadicOddEquiv,
157     `Komorebi.Residue.fourierAverage_eq_residueProj_of_primitiveRoot,
158     `Komorebi.Residue.polyphase_refinement,
159     `Komorebi.Residue.primitiveRoot_fourierOrthogonalityCertificate,
160     `Komorebi.Residue.residueProj_complete,
161     `Komorebi.Residue.residueProj_crt,
162     `Komorebi.Residue.residueProj_crt_comm,
163     `Komorebi.Residue.residueProj_dyadicOdd,
164     `Komorebi.Residue.residueProj_idempotent,
165     `Komorebi.Residue.residueProj_orthogonal,
166     `Komorebi.Residue.ringFourierAverage,
167     `Komorebi.Residue.ringFourierAverage_eq_residueProj_of_finite_certificate,
168     `Komorebi.Residue.ringFourierKernel_eq_residueKernel,
169     `Komorebi.Residue.ringFourierResidueKernel,
170   ]
171   for name in targets do
172     unless env.contains name do
173       throwError "MISSING_FROZEN_TARGET: {name}"
174   logInfo m!"FROZEN_MAP_PASS rows=25 unique_compiled_declarations={targets.size}"
175 
176 run_cmd do
177   let env ← getEnv
178   let mut audited : Nat := 0
179   for (name, info) in env.checked.get.constants.toList do
180     if Name.isPrefixOf `Komorebi name then
181       audited := audited + 1
182       if info.isUnsafe then
183         throwError "unsafe project declaration: {name}"
184       let axioms ← Lean.collectAxioms name
185       for axiomName in axioms do
186         unless axiomName == ``propext || axiomName == ``Classical.choice ||
187             axiomName == ``Quot.sound do
188           throwError "unexpected axiom {axiomName} in project declaration {name}"
189   if audited == 0 then
190     throwError "kernel audit found no Komorebi declarations"
191   logInfo m!"EXTENDED FAIL-CLOSED KERNEL AUDIT PASS: {audited} Komorebi declarations; allowed axioms only: propext, Classical.choice, Quot.sound"
192 
193 run_cmd do
194   let env ← getEnv
195   let endpoints : Array Name := #[
196     `Komorebi.PaperII.CommonRefinement.manuscript_common_refinement,
197     `Komorebi.PaperII.CommonRefinement.manuscript_coarsest_unique,
198     `Komorebi.PaperII.CommonRefinement.manuscript_finite_common,
199     `Komorebi.PaperII.CommonRefinement.exists_common_iff,
200     `Komorebi.PaperII.CommonRefinement.supported_index_empty_on_zero_module,
201     `Komorebi.PaperII.CommonRefinement.noncommuting_product_not_idempotent,
202   ]
203   for name in endpoints do
204     let some info := env.find? name | throwError "MISSING_CONSUMER: {name}"
205     let some val := info.value? (allowOpaque := true) | throwError "MISSING_BODY: {name}"
206     match Lean.Kernel.check env {} val with
207     | .error _ => throwError "BODY_RECHECK_FAILED: {name}"
208     | .ok inferred =>
209       unless Lean.Kernel.isDefEqGuarded env {} inferred info.type do
210         throwError "BODY_TYPE_MISMATCH: {name}"
211     let axioms ← Lean.collectAxioms name
212     logInfo m!"ENDPOINT_RECHECK_PASS {name} AXIOMS {axioms}"
213   logInfo m!"ENDPOINT_BODY_RECHECK_PASS count={endpoints.size}"
214 open Lean Meta Elab Command in
215 run_cmd do
216   let env ← getEnv
217   let mut count : Nat := 0
218   let mut bodies : Nat := 0
219   for (name, info) in env.checked.get.constants.toList do
220     if Name.isPrefixOf `Komorebi.PaperII.CommonRefinement name then
221       count := count + 1
222       let axs ← Lean.collectAxioms name
223       for ax in axs do
224         unless ax == ``propext || ax == ``Classical.choice || ax == ``Quot.sound do
225           throwError m!"NEW_BODY_POLICY_REJECT {name} {ax}"
226       if info.isUnsafe then throwError m!"UNSAFE_NEW_BODY {name}"
227       match info.value? (allowOpaque := true) with
228       | none => logInfo m!"NEW_DECL_STRUCTURAL {name}"
229       | some value =>
230         let inferred ← Lean.ofExceptKernelException (Lean.Kernel.check env {} value)
231         unless Lean.Kernel.isDefEqGuarded env {} inferred info.type do
232           throwError m!"NEW_BODY_TYPE_MISMATCH {name}"
233         bodies := bodies + 1
234         logInfo m!"NEW_DECL_BODY_CHECKED {name} AXIOMS {axs}"
235   if count == 0 then throwError "NEW_EMPTY_NAMESPACE"
236   logInfo m!"NEW_DECLARATION_BODY_AUDIT_PASS entries={count} bodies={bodies}"
237 
238 #print Komorebi.PaperII.CommonRefinement.manuscript_common_refinement
239 #print Komorebi.PaperII.CommonRefinement.manuscript_coarsest_unique
240 #print Komorebi.PaperII.CommonRefinement.manuscript_finite_common
241 #print Komorebi.PaperII.CommonRefinement.exists_common_iff
242 #print Komorebi.PaperII.CommonRefinement.supported_index_empty_on_zero_module
243 #print Komorebi.PaperII.CommonRefinement.noncommuting_product_not_idempotent
244 
245 #eval "PAPER_II_SUPPORTED_COMMON_REFINEMENT_RELEASE_PASS"
246 end ReleaseAudit

Back to source controls