KernelAudit.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 
6 import KomorebiPaperIII
7 
8 /-!
9 # Paper III v1.0.1 kernel audit
10 
11 This file prints the dependency surface of all 143 declarations in the final
12 Paper III theorem map: 88 theorem declarations and 55 constructions.  The
13 fail-closed namespace gate then checks all 468 compiled declarations under
14 `Komorebi.PaperIII`, including generated declarations, and freezes the exact
15 namespace and theorem counts.  Any unsafe, axiom, opaque, unexpected-axiom, or
16 unreviewed new namespace declaration is a release blocker.
17 -/
18 
19 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph
20 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.packetMatrix
21 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.packetMatrix_apply
22 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem
23 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp
24 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_apply
25 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp
26 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_eq_zero_off_support
27 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.packetMatrix_mul_packetMatrix
28 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_mul_edgeOp_eq_zero
29 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.edgeOp_mul_edgeOp_of_composable
30 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Composable
31 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp
32 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_nil
33 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_singleton
34 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_append
35 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_eq_zero_of_first_break
36 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_eq_zero_of_not_composable
37 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordExpansion
38 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.tupleWordOp
39 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.explicitWordExpansion
40 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.walkExpansion
41 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.tupleWordOp_snoc
42 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.explicitWordExpansion_succ
43 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordExpansion_eq_explicitWordExpansion
44 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.explicitWordExpansion_eq_walkExpansion
45 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_eq_wordExpansion
46 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_eq_explicitWordExpansion
47 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_eq_walkExpansion
48 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.reverseCoefficient
49 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.terminalTarget
50 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Connects
51 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_eq_packetMatrix_of_composable
52 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.wordOp_apply_eq_if_connects
53 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.endpointWalkCoefficientSum
54 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_apply_eq_sum_walks
55 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_apply_eq_zero_of_no_walk
56 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.Reachable
57 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_apply_eq_zero_of_not_reachable
58 #print axioms Komorebi.PaperIII.EdgeOperators.PacketGraph.EdgeSystem.transferOp_pow_mulVec_apply_eq_zero_of_unreachable_support
59 #print axioms Komorebi.PaperIII.EdgeOperators.heterogeneousPacketPathExpansion_two
60 #print axioms Komorebi.PaperIII.EdgeOperators.heterogeneousPacketPathExpansion_three
61 #print axioms Komorebi.PaperIII.EdgeOperators.heterogeneousProduct
62 #print axioms Komorebi.PaperIII.EdgeOperators.heterogeneousPathSum
63 #print axioms Komorebi.PaperIII.EdgeOperators.heterogeneousPacketPathExpansion
64 #print axioms Komorebi.PaperIII.EdgeOperators.SupportedStep
65 #print axioms Komorebi.PaperIII.EdgeOperators.SupportedPath
66 #print axioms Komorebi.PaperIII.EdgeOperators.heterogeneousPathSum_eq_zero_of_no_supportedPath
67 #print axioms Komorebi.PaperIII.EdgeOperators.supportedHeterogeneousPacketPathExpansion
68 #print axioms Komorebi.PaperIII.EdgeOperators.heterogeneousProduct_apply_eq_zero_of_no_supportedPath
69 #print axioms Komorebi.PaperIII.Transport.exactTransport
70 #print axioms Komorebi.PaperIII.Transport.exactTransport_apply
71 #print axioms Komorebi.PaperIII.Transport.exactTransport_self
72 #print axioms Komorebi.PaperIII.Transport.exactTransport_cocycle
73 #print axioms Komorebi.PaperIII.Transport.exactTransport_roundTrip
74 #print axioms Komorebi.PaperIII.Transport.exactTransport_triangleLoop
75 #print axioms Komorebi.PaperIII.Transport.pathEndpoint
76 #print axioms Komorebi.PaperIII.Transport.exactPathTransport
77 #print axioms Komorebi.PaperIII.Transport.exactPathTransport_eq_endpoint
78 #print axioms Komorebi.PaperIII.Transport.exactPathTransport_loop
79 #print axioms Komorebi.PaperIII.Transport.exactCoordinateTransport
80 #print axioms Komorebi.PaperIII.Transport.exactCoordinateTransport_apply
81 #print axioms Komorebi.PaperIII.Transport.exactCoordinateTransport_self
82 #print axioms Komorebi.PaperIII.Transport.exactCoordinateTransport_symm
83 #print axioms Komorebi.PaperIII.Transport.exactCoordinateTransport_cocycle
84 #print axioms Komorebi.PaperIII.Transport.exactCoordinateTransport_triangle
85 #print axioms Komorebi.PaperIII.Transport.exactCoordinateMap
86 #print axioms Komorebi.PaperIII.Transport.exactCoordinateMap_apply
87 #print axioms Komorebi.PaperIII.Transport.exactCoordinateMap_id
88 #print axioms Komorebi.PaperIII.Transport.exactCoordinateMap_comp
89 #print axioms Komorebi.PaperIII.Transport.exactCoordinateMap_naturality
90 #print axioms Komorebi.PaperIII.Transport.Connection
91 #print axioms Komorebi.PaperIII.Transport.Connection.CocycleAt
92 #print axioms Komorebi.PaperIII.Transport.Connection.Flat
93 #print axioms Komorebi.PaperIII.Transport.Connection.cocycleDefect
94 #print axioms Komorebi.PaperIII.Transport.Connection.triangleHolonomy
95 #print axioms Komorebi.PaperIII.Transport.Connection.triangleHolonomy_eq_refl_of_flat
96 #print axioms Komorebi.PaperIII.Transport.Connection.cocycleDefect_eq_refl_of_flat
97 #print axioms Komorebi.PaperIII.Transport.doubleEquiv
98 #print axioms Komorebi.PaperIII.Transport.doubleEquiv_apply
99 #print axioms Komorebi.PaperIII.Transport.twistedThreePointConnection
100 #print axioms Komorebi.PaperIII.Transport.twisted_triangleHolonomy_apply_one
101 #print axioms Komorebi.PaperIII.Transport.twisted_triangleHolonomy_ne_refl
102 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection
103 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.Gauge
104 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.CocycleAt
105 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.Flat
106 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.cocycleDefect
107 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.triangleHolonomy
108 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.triangleObstruction
109 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.cocycleDefect_eq_zero_iff_cocycleAt
110 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.triangleHolonomy_sub_id
111 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.triangleObstruction_eq_zero_iff_cocycleDefect_eq_zero
112 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.triangleObstruction_eq_zero_iff_triangleHolonomy_eq_refl
113 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.cocycleDefect_eq_zero_iff_triangleHolonomy_eq_refl
114 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.flat_iff_triangleHolonomy_eq_refl
115 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.canonicalTransport
116 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.canonicalConnection
117 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.canonicalConnection_flat
118 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.canonicalTransport_zero_connectionDefect
119 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.canonicalTransport_triangleHolonomy_eq_refl
120 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.flatGauge
121 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.flat_isGaugeOfCanonical
122 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.pathTransport
123 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.pathTransport_eq_direct_of_flat
124 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.VertexPath
125 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.indexedPathTransport
126 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.indexedPathTransport_eq_direct_of_flat
127 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.indexedLoopTransport_eq_refl_of_flat
128 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.gauge
129 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.gauge_cocycleDefect
130 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.gauge_triangleHolonomy
131 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.gauge_cocycleAt_iff
132 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.gauge_flat_iff
133 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.gauge_triangleHolonomy_eq_refl_iff
134 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution
135 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.block
136 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.sum_blocks
137 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.blocks_zero_iff
138 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.exists_packetWitness_of_block_ne_zero
139 #print axioms Komorebi.PaperIII.HolonomyBlocks.obstruction_sum_blocks
140 #print axioms Komorebi.PaperIII.HolonomyBlocks.obstructionBlocks_zero_iff
141 #print axioms Komorebi.PaperIII.HolonomyBlocks.obstructionDetection_equivalences
142 #print axioms Komorebi.PaperIII.HolonomyBlocks.exists_packetWitness_of_obstructionBlock_ne_zero
143 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.gaugeConjugate
144 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.PacketPreserving
145 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.symm_commutes_of_packetPreserving
146 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.block_gauge_of_commutes
147 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.gaugeConjugate_eq_zero_iff
148 #print axioms Komorebi.PaperIII.HolonomyBlocks.PacketResolution.block_gauge_eq_zero_iff
149 #print axioms Komorebi.PaperIII.Transport.ReversibleConnection.gauge_triangleObstruction
150 #print axioms Komorebi.PaperIII.HolonomyBlocks.obstructionBlock_gauge_of_commutes
151 #print axioms Komorebi.PaperIII.HolonomyBlocks.obstructionBlock_gauge_eq_zero_iff
152 #print axioms Komorebi.PaperIII.NonlinearObstructions.OperationTree
153 #print axioms Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval
154 #print axioms Komorebi.PaperIII.NonlinearObstructions.OperationTree.inputs
155 #print axioms Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval_congr_on_inputs
156 #print axioms Komorebi.PaperIII.NonlinearObstructions.OperationTree.eval_eq_of_inputs_eq_empty
157 #print axioms Komorebi.PaperIII.NonlinearObstructions.IsSolution
158 #print axioms Komorebi.PaperIII.NonlinearObstructions.ObstructionPacket
159 #print axioms Komorebi.PaperIII.NonlinearObstructions.ObstructionPacket.not_isSolution
160 #print axioms Komorebi.PaperIII.NonlinearObstructions.obstructionPacket_of_not_isSolution
161 #print axioms Komorebi.PaperIII.NonlinearObstructions.not_isSolution_iff_nonempty_obstructionPacket
162 
163 /-! ## Fail-closed full-namespace audit -/
164 
165 open Lean Meta Elab Command
166 
167 run_cmd do
168   let env ← getEnv
169   let mut audited : Nat := 0
170   let mut theorems : Nat := 0
171   for (name, info) in env.checked.get.constants.toList do
172     if Name.isPrefixOf `Komorebi.PaperIII name then
173       audited := audited + 1
174       match info with
175       | .thmInfo _ => theorems := theorems + 1
176       | _ => pure ()
177       if info.isUnsafe then
178         throwError "unsafe Paper III declaration: {name}"
179       match info with
180       | .axiomInfo _ =>
181           throwError "Paper III axiom declaration: {name}"
182       | .opaqueInfo _ =>
183           throwError "opaque Paper III declaration: {name}"
184       | _ => pure ()
185       let axioms ← Lean.collectAxioms name
186       for axiomName in axioms do
187         unless axiomName == ``propext || axiomName == ``Classical.choice ||
188             axiomName == ``Quot.sound do
189           throwError "unexpected axiom {axiomName} in Paper III declaration {name}"
190   if audited != 468 then
191     throwError "Paper III namespace declaration count changed: expected 468, found {audited}"
192   if theorems != 229 then
193     throwError "Paper III namespace theorem count changed: expected 229, found {theorems}"
194   logInfo m!"FAIL-CLOSED PAPER III v1.0.1 KERNEL AUDIT PASS: {audited} declarations ({theorems} theoremInfo); 143 explicit mapped targets; allowed axioms only: propext, Classical.choice, Quot.sound"

Back to source controls