Two Books at the Bookstore.
Seven Archival Statements at Home.

The displayed archival statement says that an isometry satisfying the archive's isCloner predicate leads to False. The predicate definition and proof are not published or independently checked on this page, so the excerpt is not a general implementation certificate.

theorem no_cloning
    (U : EuclideanSpace ℂ (Fin 4) →ₗᵢ[ℂ] EuclideanSpace ℂ (Fin 4))
    (hC : isCloner U) : False

For the archive's ClassicalStrategy and chshValue definitions, the displayed statement bounds the absolute classical value by 2. It does not display a quantum strategy, derive the 2√2 value, or certify an experiment.

theorem classical_CHSH_bound
    (s : ClassicalStrategy) : |chshValue s| ≤ 2

Alice

Bob

The displayed algebraic identity says that, for the archive's branch and correction definitions and two bit indices a and b, applying the indexed correction returns ψ. It does not certify the toy animation or a physical teleportation system.

theorem teleportation_fidelity
    (ψ : Fin 2 → ℂ) (a b : Fin 2) :
    correction (a, b) *ᵥ branch (a, b) *ᵥ ψ = ψ

Under the displayed hypotheses M ≥ 1, M ≤ N, and 0 < grTheta N M, this archival statement lower-bounds the squared grAmp value after groverSteps by 1 − M/N. It does not state a query count, a classical lower bound, or Grover optimality.

theorem grover_success
    (hM : 1 ≤ M) (hMN : M ≤ N) (hθ : 0 < grTheta N M) :
    1 - (M : ℝ) / N ≤ (grAmp N M (groverSteps N M))²

For a real-valued function on the archive's Boolean cube, this statement equates the sum of squared Fourier coefficients with the archive's expected squared value. It makes no claim about every machine-learning algorithm, training, or generalization.

theorem parseval
    (n : ℕ) (f : BoolCube n → ℝ) :
    ∑ S : Finset (Fin n), (fourierCoeff n f S) ^ 2 =
    boolExpect n (fun x => (f x) ^ 2)

Assuming the archive's hasFourierDeg predicate at degree d, this statement bounds the fourth moment by 9^d times the square of the second moment. It does not by itself prove noise smoothing, KKL, gradient-descent behavior, or why machine learning works.

theorem bonami_lemma
    (n : ℕ) (f : BoolCube n → ℝ) (d : ℕ)
    (hDeg : hasFourierDeg n f d) :
    boolExpect n (fun x => (f x) ^ 4) ≤
    9 ^ d * (boolExpect n (fun x => (f x) ^ 2)) ^ 2

Statement excerpt from a separate unpinned archive. No compiler result or axiom audit is attached here. No Jill manifest receipt is attached here.