Quantum and Circuits · Lean source
AxiomAudit.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.
quantum_fresh_20261026/fresh/AxiomAudit.lean193 lines
Original source path
verification/quantum_fresh_20261026/fresh/AxiomAudit.lean
1 import Publication
2 #print axioms Komorebi.QuantumArithmetic.ramanujan12_length
3 #check Komorebi.QuantumArithmetic.ramanujan12_length
4 #print axioms Komorebi.QuantumArithmetic.projector12_shape
5 #check Komorebi.QuantumArithmetic.projector12_shape
6 #print axioms Komorebi.QuantumArithmetic.projector12_symmetric
7 #check Komorebi.QuantumArithmetic.projector12_symmetric
8 #print axioms Komorebi.QuantumArithmetic.projector12_idempotent
9 #check Komorebi.QuantumArithmetic.projector12_idempotent
10 #print axioms Komorebi.QuantumArithmetic.projector12_fixes_ramanujan
11 #check Komorebi.QuantumArithmetic.projector12_fixes_ramanujan
12 #print axioms Komorebi.QuantumArithmetic.projector12_kills_noise
13 #check Komorebi.QuantumArithmetic.projector12_kills_noise
14 #print axioms Komorebi.QuantumArithmetic.projector12_recovers_test_signal
15 #check Komorebi.QuantumArithmetic.projector12_recovers_test_signal
16 #print axioms Komorebi.QuantumArithmetic.ramanujan12_energy
17 #check Komorebi.QuantumArithmetic.ramanujan12_energy
18 #print axioms Komorebi.QuantumArithmetic.noise12_energy
19 #check Komorebi.QuantumArithmetic.noise12_energy
20 #print axioms Komorebi.QuantumArithmetic.testSignal12_energy
21 #check Komorebi.QuantumArithmetic.testSignal12_energy
22 #print axioms Komorebi.QuantumArithmetic.energy_decomposition
23 #check Komorebi.QuantumArithmetic.energy_decomposition
24 #print axioms Komorebi.QuantumArithmetic.zeta12_order_certificate
25 #check Komorebi.QuantumArithmetic.zeta12_order_certificate
26 #print axioms Komorebi.QuantumArithmetic.zeta12_inverse_certificate
27 #check Komorebi.QuantumArithmetic.zeta12_inverse_certificate
28 #print axioms Komorebi.QuantumArithmetic.ramanujanC12_table
29 #check Komorebi.QuantumArithmetic.ramanujanC12_table
30 #print axioms Komorebi.QuantumArithmetic.ramanujan_dft_table
31 #check Komorebi.QuantumArithmetic.ramanujan_dft_table
32 #print axioms Komorebi.QuantumArithmetic.abs_ramanujan_dft_table
33 #check Komorebi.QuantumArithmetic.abs_ramanujan_dft_table
34 #print axioms Komorebi.QuantumArithmetic.same_computational_basis_probabilities
35 #check Komorebi.QuantumArithmetic.same_computational_basis_probabilities
36 #print axioms Komorebi.QuantumArithmetic.abs_ramanujan12_energy
37 #check Komorebi.QuantumArithmetic.abs_ramanujan12_energy
38 #print axioms Komorebi.QuantumArithmetic.recovered_mode_probability
39 #check Komorebi.QuantumArithmetic.recovered_mode_probability
40 #print axioms Komorebi.QuantumArithmetic.recovered_total_probability
41 #check Komorebi.QuantumArithmetic.recovered_total_probability
42 #print axioms Komorebi.QuantumArithmetic.phase_stripping_coprime_probability
43 #check Komorebi.QuantumArithmetic.phase_stripping_coprime_probability
44 #print axioms Komorebi.QuantumArithmetic.arithmetic_signal_quantum_bridge
45 #check Komorebi.QuantumArithmetic.arithmetic_signal_quantum_bridge
46 #print axioms Komorebi.QuantumArithmetic.coprime_residues_exact
47 #check Komorebi.QuantumArithmetic.coprime_residues_exact
48 #print axioms Komorebi.QuantumArithmetic.root_exact_order
49 #check Komorebi.QuantumArithmetic.root_exact_order
50 #print axioms Komorebi.QuantumArithmetic.normalized_fourier_left
51 #check Komorebi.QuantumArithmetic.normalized_fourier_left
52 #print axioms Komorebi.QuantumArithmetic.normalized_fourier_right
53 #check Komorebi.QuantumArithmetic.normalized_fourier_right
54 #print axioms Komorebi.QuantumArithmetic.exact_projector_transport
55 #check Komorebi.QuantumArithmetic.exact_projector_transport
56 #print axioms Komorebi.QuantumArithmetic.exact_projector_matches_rational_table
57 #check Komorebi.QuantumArithmetic.exact_projector_matches_rational_table
58 #print axioms Komorebi.QuantumArithmetic.exact_state_preparation
59 #check Komorebi.QuantumArithmetic.exact_state_preparation
60 #print axioms Komorebi.QuantumArithmetic.exact_state_recovery
61 #check Komorebi.QuantumArithmetic.exact_state_recovery
62 #print axioms Komorebi.QuantumArithmetic.exact_unit_normalized
63 #check Komorebi.QuantumArithmetic.exact_unit_normalized
64 #print axioms Komorebi.QuantumArithmetic.exact_psi_normalized
65 #check Komorebi.QuantumArithmetic.exact_psi_normalized
66 #print axioms Komorebi.QuantumArithmetic.exact_chi_normalized
67 #check Komorebi.QuantumArithmetic.exact_chi_normalized
68 #print axioms Komorebi.QuantumArithmetic.exact_same_initial_probabilities
69 #check Komorebi.QuantumArithmetic.exact_same_initial_probabilities
70 #print axioms Komorebi.QuantumArithmetic.exact_orthogonal_states
71 #check Komorebi.QuantumArithmetic.exact_orthogonal_states
72 #print axioms Komorebi.QuantumArithmetic.exact_coprime_mass_psi
73 #check Komorebi.QuantumArithmetic.exact_coprime_mass_psi
74 #print axioms Komorebi.QuantumArithmetic.exact_coprime_mass_chi
75 #check Komorebi.QuantumArithmetic.exact_coprime_mass_chi
76 #print axioms Komorebi.QuantumArithmetic.exact_projector_fixes_psi
77 #check Komorebi.QuantumArithmetic.exact_projector_fixes_psi
78 #print axioms Komorebi.QuantumArithmetic.exact_projector_kills_chi
79 #check Komorebi.QuantumArithmetic.exact_projector_kills_chi
80 #print axioms Komorebi.QuantumArithmetic.interpret_zero
81 #check Komorebi.QuantumArithmetic.interpret_zero
82 #print axioms Komorebi.QuantumArithmetic.interpret_one
83 #check Komorebi.QuantumArithmetic.interpret_one
84 #print axioms Komorebi.QuantumArithmetic.interpret_rat
85 #check Komorebi.QuantumArithmetic.interpret_rat
86 #print axioms Komorebi.QuantumArithmetic.interpret_add
87 #check Komorebi.QuantumArithmetic.interpret_add
88 #print axioms Komorebi.QuantumArithmetic.interpret_mul
89 #check Komorebi.QuantumArithmetic.interpret_mul
90 #print axioms Komorebi.QuantumArithmetic.interpret_conj
91 #check Komorebi.QuantumArithmetic.interpret_conj
92 #print axioms Komorebi.QuantumArithmetic.interpret_pow
93 #check Komorebi.QuantumArithmetic.interpret_pow
94 #print axioms Komorebi.QuantumArithmetic.interpret_sum
95 #check Komorebi.QuantumArithmetic.interpret_sum
96 #print axioms Komorebi.QuantumArithmetic.interpret_kSum
97 #check Komorebi.QuantumArithmetic.interpret_kSum
98 #print axioms Komorebi.QuantumArithmetic.complexMatrix_mul
99 #check Komorebi.QuantumArithmetic.complexMatrix_mul
100 #print axioms Komorebi.QuantumArithmetic.complexMatrix_adjoint
101 #check Komorebi.QuantumArithmetic.complexMatrix_adjoint
102 #print axioms Komorebi.QuantumArithmetic.complexMatrix_identity
103 #check Komorebi.QuantumArithmetic.complexMatrix_identity
104 #print axioms Komorebi.QuantumArithmetic.complexVector_mul
105 #check Komorebi.QuantumArithmetic.complexVector_mul
106 #print axioms Komorebi.QuantumArithmetic.fourier_unitary_left
107 #check Komorebi.QuantumArithmetic.fourier_unitary_left
108 #print axioms Komorebi.QuantumArithmetic.fourier_unitary_right
109 #check Komorebi.QuantumArithmetic.fourier_unitary_right
110 #print axioms Komorebi.QuantumArithmetic.projector_transport
111 #check Komorebi.QuantumArithmetic.projector_transport
112 #print axioms Komorebi.QuantumArithmetic.state_preparation
113 #check Komorebi.QuantumArithmetic.state_preparation
114 #print axioms Komorebi.QuantumArithmetic.state_recovery
115 #check Komorebi.QuantumArithmetic.state_recovery
116 #print axioms Komorebi.QuantumArithmetic.interpret_normSq
117 #check Komorebi.QuantumArithmetic.interpret_normSq
118 #print axioms Komorebi.QuantumArithmetic.interpret_mass
119 #check Komorebi.QuantumArithmetic.interpret_mass
120 #print axioms Komorebi.QuantumArithmetic.interpret_coprimeMass
121 #check Komorebi.QuantumArithmetic.interpret_coprimeMass
122 #print axioms Komorebi.QuantumArithmetic.psi_normalized
123 #check Komorebi.QuantumArithmetic.psi_normalized
124 #print axioms Komorebi.QuantumArithmetic.chi_normalized
125 #check Komorebi.QuantumArithmetic.chi_normalized
126 #print axioms Komorebi.QuantumArithmetic.unitState_normalized
127 #check Komorebi.QuantumArithmetic.unitState_normalized
128 #print axioms Komorebi.QuantumArithmetic.same_initial_probabilities
129 #check Komorebi.QuantumArithmetic.same_initial_probabilities
130 #print axioms Komorebi.QuantumArithmetic.states_orthogonal
131 #check Komorebi.QuantumArithmetic.states_orthogonal
132 #print axioms Komorebi.QuantumArithmetic.signed_state_recovers_arithmetic
133 #check Komorebi.QuantumArithmetic.signed_state_recovers_arithmetic
134 #print axioms Komorebi.QuantumArithmetic.unsigned_state_erases_arithmetic
135 #check Komorebi.QuantumArithmetic.unsigned_state_erases_arithmetic
136 #print axioms Komorebi.QuantumArithmetic.projector_fixes_psi
137 #check Komorebi.QuantumArithmetic.projector_fixes_psi
138 #print axioms Komorebi.QuantumArithmetic.projector_kills_chi
139 #check Komorebi.QuantumArithmetic.projector_kills_chi
140 #print axioms Komorebi.QuantumArithmetic.root_is_exponential
141 #check Komorebi.QuantumArithmetic.root_is_exponential
142 #print axioms Komorebi.QuantumArithmetic.root_power_twelve
143 #check Komorebi.QuantumArithmetic.root_power_twelve
144 #print axioms Komorebi.QuantumArithmetic.rootPower_interpret
145 #check Komorebi.QuantumArithmetic.rootPower_interpret
146 #print axioms Komorebi.QuantumArithmetic.sqrt_twelve
147 #check Komorebi.QuantumArithmetic.sqrt_twelve
148 #print axioms Komorebi.QuantumArithmetic.sqrt_fortyeight
149 #check Komorebi.QuantumArithmetic.sqrt_fortyeight
150 #print axioms Komorebi.QuantumArithmetic.fourierScale_interpret
151 #check Komorebi.QuantumArithmetic.fourierScale_interpret
152 #print axioms Komorebi.QuantumArithmetic.stateScale_interpret
153 #check Komorebi.QuantumArithmetic.stateScale_interpret
154 #print axioms Komorebi.QuantumArithmetic.fourier_entry_formula
155 #check Komorebi.QuantumArithmetic.fourier_entry_formula
156 #print axioms Komorebi.QuantumArithmetic.psi_entry_formula
157 #check Komorebi.QuantumArithmetic.psi_entry_formula
158 #print axioms Komorebi.QuantumArithmetic.chi_entry_formula
159 #check Komorebi.QuantumArithmetic.chi_entry_formula
160 #print axioms Komorebi.QuantumArithmetic.unitState_entry_formula
161 #check Komorebi.QuantumArithmetic.unitState_entry_formula
162 #print axioms Komorebi.QuantumArithmetic.projector_entry_formula
163 #check Komorebi.QuantumArithmetic.projector_entry_formula
164 #print axioms Komorebi.QuantumArithmetic.selector_idempotent
165 #check Komorebi.QuantumArithmetic.selector_idempotent
166 #print axioms Komorebi.QuantumArithmetic.selector_selfAdjoint
167 #check Komorebi.QuantumArithmetic.selector_selfAdjoint
168 #print axioms Komorebi.QuantumArithmetic.projector_idempotent_complex
169 #check Komorebi.QuantumArithmetic.projector_idempotent_complex
170 #print axioms Komorebi.QuantumArithmetic.projector_selfAdjoint_complex
171 #check Komorebi.QuantumArithmetic.projector_selfAdjoint_complex
172 #print axioms Komorebi.QuantumArithmetic.complete_phase_separation
173 #check Komorebi.QuantumArithmetic.complete_phase_separation
174 #print axioms Komorebi.QuantumArithmetic.exact_phase_signal_lookup
175 #check Komorebi.QuantumArithmetic.exact_phase_signal_lookup
176 #print axioms Komorebi.QuantumArithmetic.complex_ramanujan_signal
177 #check Komorebi.QuantumArithmetic.complex_ramanujan_signal
178 #print axioms Komorebi.QuantumArithmetic.absolute_signal_lookup
179 #check Komorebi.QuantumArithmetic.absolute_signal_lookup
180 #print axioms Komorebi.QuantumArithmetic.retained_discarded_orthogonal
181 #check Komorebi.QuantumArithmetic.retained_discarded_orthogonal
182 #print axioms Komorebi.QuantumArithmetic.signal_decomposition
183 #check Komorebi.QuantumArithmetic.signal_decomposition
184 #print axioms Komorebi.QuantumArithmetic.projector_residual_reconstructs
185 #check Komorebi.QuantumArithmetic.projector_residual_reconstructs
186 #print axioms Komorebi.QuantumArithmetic.no_reconstruction_from_initial_probabilities
187 #check Komorebi.QuantumArithmetic.no_reconstruction_from_initial_probabilities
188 #print axioms Komorebi.QuantumArithmetic.recovered_probability_at
189 #check Komorebi.QuantumArithmetic.recovered_probability_at
190 #print axioms Komorebi.QuantumArithmetic.projector_not_injective
191 #check Komorebi.QuantumArithmetic.projector_not_injective
192 #print axioms Komorebi.QuantumArithmetic.publication_bridge
193 #check Komorebi.QuantumArithmetic.publication_bridge
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: 812b8a723d0c3c5a707909188a733b540361019c4466c3e9f0d38e47d9319da2
Original source on GitHub
Back to Quantum and Circuits