A.19 The original finite bridge and its extension
On this page · Permalink · Source line 981
A.20 Formal coverage, lineage, and reproducibility
On this page · Permalink · Source line 983
A.20.1 Two inherited checkpoints and the expanded boundary
On this page · Permalink · Source line 987
The earlier checked package has four mathematical production modules and fifty-nine named theorem declarations. Its first module preserves twenty-two original statements. Its proof-boundary document correctly says that explicit matrix transport between independently defined representations and normalized state-action identities are not supplied as additional theorems in that package. Those limitations must not be erased when describing the earlier evidence.
The later checked package has five production modules and ninety-six named theorem declarations:
| Module | Named theorems | Principal role |
|---|---|---|
QuantumArithmeticBridge | 22 | Literal rational projector and cyclotomic tables |
FiniteFourier | 17 | Indexed exact Fourier and normalized state identities |
SemanticBridge | 30 | Sound complex interpretation and transported identities |
Conventions | 17 | Exponential entries, scales, and complex projector laws |
Publication | 10 | Phase lookup, residual reconstruction, nonreconstruction, and central bundle |
| Total | 96 | Finite modulus-twelve proof chain, including helpers |
The later source explicitly supplies \(FDF^\dagger=P\), both normalized state-action identities, the conventional exponential formula for \(F\), identical initial probabilities, orthogonality, exact selected probability one versus zero, histogram nonreconstruction, and projector noninjectivity. It therefore closes the representation-transport obligations that the earlier package leaves outside its formal boundary.
The ninety-six count includes helper lemmas and bundled propositions. It is not a count of ninety-six independent discoveries. Nor should the earlier fifty-nine and later ninety-six counts be added as if their shared declarations were disjoint.
A.20.2 Current and inherited checks
On this page · Permalink · Source line 1044
This edition preserves the source, theorem index, verification records, and compiled-artifact lineage of the checked checkpoints. The archived records provide the earlier compiler and kernel-checking evidence. Current static audits and independent Python replay provide current bounded evidence about the downloaded files and the example implementation. These are disclosed separately in the release records.
The pinned runtime was restored for this completion pass. Fresh source compilation, axiom inspection, and replay of all five modules passed. The separate historical failures are preserved in the source records.
The exact source uses kernel-reduction decision proofs for finite identities and ordinary proof terms for the transport lemmas. The declaration audit rejects admitted proofs and unapproved project-specific axioms. Standard foundational dependencies are reported in the formal guide. Compiled artifact checking reuses Lean's kernel; it is not an independently implemented proof assistant.
The later checkpoint preserves three negative controls with distinct meanings. The false-sign claim is a directly false finite statement. The false-mode case is an operational rejection whose failure mechanism must be read alongside its diagnostic and the positive checked transform table. The admitted-proof case tests the verification policy for incomplete proof evidence. These controls are not combined with the four controls of the earlier checkpoint into an artificial total.
A.20.3 Independent arithmetic evidence
On this page · Permalink · Source line 1072
The original reproducibility package records 3,003 exact Python assertions, separately from floating-point checks. Its exact verifier represents the twelfth root in a cyclotomic quotient, checks the signal and transform tables, the rational projector identities, the test-signal decomposition, divisor-shell completeness, and the phase-sensitive example. Its arithmetic regression range is bounded to moduli two through sixty-four.
The release also includes the current replay and any added finite checks with their own records. Exact rational or cyclotomic arithmetic and numerical residuals are reported separately. A small floating-point residual verifies the implementation at its declared tolerance; it does not replace the exact proof of the general formula. Likewise, a finite modulus sweep does not prove the arbitrary-modulus theorem. QA01 through QA09 provide the general proofs needed here.
A.20.4 The twenty-two preserved original statements
On this page · Permalink · Source line 1092
The original bridge module's statements remain available under their original names. The following list records their substantive content rather than treating each source helper as a separate main theorem.
| Original declaration | Preserved statement |
|---|---|
ramanujan12_length | The rational signal list has length twelve |
projector12_shape | The literal matrix has twelve rows and twelve columns |
projector12_symmetric | The rational matrix equals its transpose |
projector12_idempotent | Exact rational multiplication gives \(P^2=P\) |
projector12_fixes_ramanujan | The matrix fixes the signal \(c\) |
projector12_kills_noise | The matrix sends the displayed perturbation \(b\) to zero |
projector12_recovers_test_signal | Applying it to \(x\) returns \(c\) |
ramanujan12_energy | \(\|c\|^2=48\) |
noise12_energy | \(\|b\|^2=102\) |
testSignal12_energy | \(\|x\|^2=150\) |
energy_decomposition | The exact energy balance is \(150=48+102\) |
zeta12_order_certificate | The coordinate root raised to the twelfth power is one |
zeta12_inverse_certificate | The coordinate root times its conjugate is one |
ramanujanC12_table | Four primitive phase sums give the exact twelve-entry signal table |
ramanujan_dft_table | The negative-sign DFT gives twelve exactly at \(1,5,7,11\) |
abs_ramanujan_dft_table | The unsigned DFT gives the exact even-support table |
same_computational_basis_probabilities | Signed and unsigned rational entries have the same squares |
abs_ramanujan12_energy | The unsigned signal also has squared energy forty-eight |
recovered_mode_probability | The scalar normalization gives \(12^2/(48\cdot12)=1/4\) |
recovered_total_probability | Four recovered mode probabilities sum to one |
phase_stripping_coprime_probability | Zero transformed coefficients give zero selected mass |
arithmetic_signal_quantum_bridge | The original finite projector, recovery, DFT, and equal-square claims are bundled |
The later source strengthens the specification around these statements. It proves that the four labels are exactly the coprime residues, that the coordinate root has no smaller positive order, that the literal rational and indexed matrices agree, and that the probability consequences belong to the actual normalized complex state vectors.
The list operations in the original module use explicit finite literal lists. Their generic helper definitions are not an assertion of arbitrary-dimensional linear algebra for unsized lists, where zip operations could truncate. General vector identities in this chapter use fixed finite index sets, and the later matrix source uses Fin 12 for exactly that reason.