A.13 The publication theorem in full
On this page · Permalink · Source line 696
The final declaration bundles the formal core of the worked example. Every conjunct is supported by a previously proved declaration rather than by a new numerical test or an implicit physical assumption.
Literal source. Publication.lean, physical lines 67–80.
/-- Publication theorem gathering the complex identities stated in the worked example. -/
theorem publication_bridge :
Fᴴ * F = 1 ∧ F * Fᴴ = 1 ∧ F * D * Fᴴ = P ∧
P * P = P ∧ Pᴴ = P ∧ F.mulVec unitState = psi ∧
Fᴴ.mulVec psi = unitState ∧ totalProbability psi = 1 ∧
totalProbability chi = 1 ∧
(∀ i, Complex.normSq (psi i) = Complex.normSq (chi i)) ∧
(∑ i, star (psi i) * chi i) = 0 ∧
coprimeProbability (Fᴴ.mulVec psi) = 1 ∧
coprimeProbability (Fᴴ.mulVec chi) = 0 := by
exact ⟨fourier_unitary_left, fourier_unitary_right, projector_transport,
projector_idempotent_complex, projector_selfAdjoint_complex, state_preparation,
state_recovery, psi_normalized, chi_normalized, same_initial_probabilities,
states_orthogonal, signed_state_recovers_arithmetic, unsigned_state_erases_arithmetic⟩The bundled theorem has a fixed dimension and explicitly named operators and states. It establishes the bridge used in the paper. Broader arbitrary-modulus results remain separate prose theorems, with their own proofs and evidence.
The manuscript's QA18 additionally includes filtering and energy, normalization of \(u\), the projector actions on both states, and noninjectivity. Those clauses use separately exported declarations, including projector12_recovers_test_signal, energy_decomposition, unitState_normalized, projector_fixes_psi, projector_kills_chi, and projector_not_injective. The complete machine concordance lists these supporting results. The manuscript bundle is not identified with a literal statement that omits its extra clauses.