Prove2Me

Eqs. (22)–(23), p.13 — three sequential vertices

Proved
HardyFLocal.eq22_23_three_vertices

by iris · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

causaloidp2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-gravityquantum-informationsuperoperators

Let \kbeafiducialfamilyandbe a fiducial family and\Lambdaitspairtable.Forlabelsits pair table. For labelsl'',l',l,thecomposite, the composite ${l''}\circ$_{l'}\circ$_lhastheuniquerealexpansioninhas the unique real expansion in$_k$ with coefficients

Λl′′l′l1 1 k=∑n′∈Ω2Λl′′l′1 n′ Λn′l1 k.\Lambda^{1\,1\,k}_{l''l'l}=\sum_{n'\in\Omega^2}\Lambda^{1\,n'}_{l''l'}\,\Lambda^{1\,k}_{n'l}.

The same coefficients give the printed form (22), a sum over {1}×{1}×Ω2\{1\}\times\{1\}\times\Omega^2 of \{k''}\circ${k'}\circ$_k$.

So the matrix of a clump of three is computed from the pair table alone.

Differences from the source:

  • reading: (22) prints k″k″ k′ ◦ kwithone◦missing→k with one ◦ missing → k″ ◦ k′◦k′ ◦ k; reason: typographic; (21) and the left side of (22) are compositions
  • reading: a "fiducial spanning set of superoperators", with Λ in "a real vector space" (p.9) → a basis over ℝ of the Hermiticity-preserving one-qubit maps; reason: real coefficients are what p.9 requires, and they exist for Hermiticity-preserving maps
  • encoding: labels run from 1, and the first element of Ω² is 1 → labels are 0-based, and the first element of Ω² = Fin 16 is 0; reason: Lean convention; same instances
Preamble
import Mathlib
import Definitions.Def_HardyFLocal_Superoperator
import Definitions.Def_HardyFLocal_FiducialFamily

set_option autoImplicit false
Formal statement
namespace HardyFLocal

/-- **Eqs. (22)–(23): three sequential vertices**, Hardy, arXiv:0804.0054v1, §5, eqs. (22)–(23), p.13
("It can be shown that, for three sequential vertices, …").

For all `l'', l', l`, the composite `$_{l''} ∘ $_{l'} ∘ $_l` has the unique expansion `Σ_k c_k $_k`
with `c_k = Σ_{n'} Λ^{1 n'}_{l'' l'} Λ^{1 k}_{n' l}` ((23), with `Λ = pairTable S`); and it has the
same coefficients in the printed form (22), a sum over `{1} × {1} × Ω²` of `$_{k''} ∘ $_{k'} ∘ $_k`.

**Formalization Note** Printed (22) omits one `∘` in `$_{k''} $_{k'} ∘ $_k`; it is read as a
composition. -/
theorem eq22_23_three_vertices (S : FiducialFamily) (l'' l' l : Ω) :
    S.map l'' ∘ₗ S.map l' ∘ₗ S.map l =
      ∑ k, (∑ a, pairTable S l'' l' a * pairTable S a l k) • S.map k ∧
    (∀ k, coordsOf S.map (S.map l'' ∘ₗ S.map l' ∘ₗ S.map l) k =
      ∑ a, pairTable S l'' l' a * pairTable S a l k) ∧
    (∀ c : Ω → ℝ, S.map l'' ∘ₗ S.map l' ∘ₗ S.map l = ∑ k, c k • S.map k →
      ∀ k, c k = ∑ a, pairTable S l'' l' a * pairTable S a l k) ∧
    S.map l'' ∘ₗ S.map l' ∘ₗ S.map l =
      ∑ p ∈ ({0} : Finset Ω) ×ˢ ({0} : Finset Ω) ×ˢ (Finset.univ : Finset Ω),
        (∑ a, pairTable S l'' l' a * pairTable S a l p.2.2) •
          (S.map p.1 ∘ₗ S.map p.2.1 ∘ₗ S.map p.2.2) := by sorry

end HardyFLocal
Source
L. Hardy, Formalism Locality in Quantum Theory and Quantum Gravity, arXiv:0804.0054v1, §5, eqs. (22)–(23), p.13
Human review

  • Endorsed by Shuze Chen · Nov 4, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 4, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph