A.17 Complete active theorem inventory
On this page · Permalink · Source line 834
All names in the following table have prefix Komorebi.QuantumArithmetic. File and physical source line identify the exact declaration. The full literal statements and axiom lists are also available in Lean_Concordance.json and Lean_Concordance.csv.
A.17.1 QuantumArithmeticBridge: 22 theorems
On this page · Permalink · Source line 841
| Declaration | Line |
|---|---|
ramanujan12_length | 80 |
projector12_shape | 82 |
projector12_symmetric | 88 |
projector12_idempotent | 92 |
projector12_fixes_ramanujan | 97 |
projector12_kills_noise | 102 |
projector12_recovers_test_signal | 107 |
ramanujan12_energy | 112 |
noise12_energy | 116 |
testSignal12_energy | 120 |
energy_decomposition | 124 |
zeta12_order_certificate | 177 |
zeta12_inverse_certificate | 180 |
ramanujanC12_table | 190 |
ramanujan_dft_table | 205 |
abs_ramanujan_dft_table | 217 |
same_computational_basis_probabilities | 231 |
abs_ramanujan12_energy | 235 |
recovered_mode_probability | 243 |
recovered_total_probability | 248 |
phase_stripping_coprime_probability | 253 |
arithmetic_signal_quantum_bridge | 258 |
A.17.2 FiniteFourier: 17 theorems
On this page · Permalink · Source line 870
| Declaration | Line |
|---|---|
coprime_residues_exact | 59 |
root_exact_order | 63 |
normalized_fourier_left | 67 |
normalized_fourier_right | 71 |
exact_projector_transport | 79 |
exact_projector_matches_rational_table | 83 |
exact_state_preparation | 87 |
exact_state_recovery | 91 |
exact_unit_normalized | 95 |
exact_psi_normalized | 98 |
exact_chi_normalized | 101 |
exact_same_initial_probabilities | 104 |
exact_orthogonal_states | 108 |
exact_coprime_mass_psi | 112 |
exact_coprime_mass_chi | 116 |
exact_projector_fixes_psi | 120 |
exact_projector_kills_chi | 124 |
A.17.3 SemanticBridge: 30 theorems
On this page · Permalink · Source line 894
| Declaration | Line |
|---|---|
interpret_zero | 19 |
interpret_one | 22 |
interpret_rat | 25 |
interpret_add | 28 |
interpret_mul | 32 |
interpret_conj | 37 |
interpret_pow | 42 |
interpret_sum | 48 |
interpret_kSum | 54 |
complexMatrix_mul | 65 |
complexMatrix_adjoint | 70 |
complexMatrix_identity | 75 |
complexVector_mul | 80 |
fourier_unitary_left | 94 |
fourier_unitary_right | 99 |
projector_transport | 104 |
state_preparation | 112 |
state_recovery | 117 |
interpret_normSq | 122 |
interpret_mass | 133 |
interpret_coprimeMass | 137 |
psi_normalized | 145 |
chi_normalized | 149 |
unitState_normalized | 153 |
same_initial_probabilities | 157 |
states_orthogonal | 162 |
signed_state_recovers_arithmetic | 166 |
unsigned_state_erases_arithmetic | 171 |
projector_fixes_psi | 176 |
projector_kills_chi | 181 |
A.17.4 Conventions: 17 theorems
On this page · Permalink · Source line 931
| Declaration | Line |
|---|---|
root_is_exponential | 11 |
root_power_twelve | 18 |
rootPower_interpret | 21 |
sqrt_twelve | 26 |
sqrt_fortyeight | 34 |
fourierScale_interpret | 42 |
stateScale_interpret | 49 |
fourier_entry_formula | 57 |
psi_entry_formula | 67 |
chi_entry_formula | 71 |
unitState_entry_formula | 75 |
projector_entry_formula | 80 |
selector_idempotent | 84 |
selector_selfAdjoint | 91 |
projector_idempotent_complex | 98 |
projector_selfAdjoint_complex | 106 |
complete_phase_separation | 111 |
A.17.5 Publication: 10 theorems
On this page · Permalink · Source line 955
| Declaration | Line |
|---|---|
exact_phase_signal_lookup | 9 |
complex_ramanujan_signal | 14 |
absolute_signal_lookup | 22 |
retained_discarded_orthogonal | 27 |
signal_decomposition | 30 |
projector_residual_reconstructs | 34 |
no_reconstruction_from_initial_probabilities | 40 |
recovered_probability_at | 53 |
projector_not_injective | 60 |
publication_bridge | 68 |