All missions

Motivation

We construct some new cohomology theories for topological groups and Lie groups and study some of its basic properties. For example, we introduce a cohomology theory based on measurable cochains which are continuous in a neighbourhood of identity. We show that if G and A are locally compact and second countable, then the second cohomology group based on locally continuous measurable cochains as above parametrizes the collection of locally split extensions of G by A.

This mission is the statement-level formalization of On Cohomology theory for topological groups (arXiv:1009.4519v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

14 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is A Borel section continuous near identity for Lindelof quotient (Remark 2: the Lindelof section construction, PDF p. 10). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

32 results of the paper are not stated yet, because the library lacks an interface they need:

• Abstract main result; Theorems 1 and 5: locally split extension classification: Unnormalized Borel locally continuous H^2 and its canonical extension-class bijection (hard)
• Proposition 1: holomorphic first cohomology: Holomorphic crossed homomorphisms modulo principal ones as actual H_lhm^1 (source-ambiguity)
• Theorem 1: classification announcement: Canonical H_lcm^2 classification by all fixed-action locally split topological extensions (hard)
• Theorem 2: smooth extension classification announcement: Unnormalized locally smooth measurable H^2 and smooth extension classification map (hard)
• Theorem 3: degree-two smooth/continuous comparison announcement: Inclusion-induced H_lsm^2 to H_lcm^2 homomorphism on actual quotient groups (hard)
• Introduction: first-cohomology comparisons: Actual degree-one quotients and canonical comparisons in continuous, Borel, lcm and smooth regimes (hard)
• Introduction: restriction to smooth cochain germs: Smooth cochain germ complex, its homology, and the restriction-induced homomorphism (hard)
• Swierczkowski germ/Lie-algebra comparison: smoothGermCohomology; Lie algebra of G; differentiated representation; Lie-algebra cohomology; lieAlgebraCohomology; differentiatedRepresentation (hard)
• Example 1: connected/discrete vanishing and exponential-sequence failure: Continuous-cohomology quotient, exponential coefficient sequence and its exactness obstruction (hard)
• Theorem 4 (Mackey, Dixmier): measurable quotient section: PolishSpace; closed subgroup; quotient topology; quotient Borel structure; measurable section (hard)
• Proposition 2 (Moore): measurable extension classification: measurableCochains; regularCohomology; topologicalExtension; extensionEquivalence; inducedMeasurableModule; extensionClassificationMap; measurableCohomology; inducedMeasurableQuotient (hard)
• Section 2.3: induced measurable module and dimension shift: inducedMeasurableModule; measurableCochains; regularCohomology; dimension-shift connecting map; measurableCohomology; inducedMeasurableQuotient (source-ambiguity)
• Remark 1 (Mackey): local compactness of measurable extensions: measurableCochains; topologicalExtension; inducedMeasurableModule (hard)
• Sections 3.1 and Introduction: complex, invariants and natural comparisons: All-degree restricted cochain differential, kernel/image quotients, H^0 identification and natural inclusions (hard)
• Section 3.2: change of groups, coefficients and restriction: Cochain pullback/coefficient map and its induced all-degree lcm homomorphism (hard)
• Unnumbered theorem (Mostert): local sections: coveringDimension; closed normal subgroup; locallySplitSequence (hard)
• Lemma 1: global measurable locally continuous section: locallySplitSequence; measurableLocallyRegularSection (source-ambiguity)
• Corollary 1: cochain short exact sequence and cohomology long exact sequence: locallySplitSequence; lcmCochains; regularCohomology; coefficientConnectingMaps; locallyContinuousMeasurableCohomology (source-ambiguity)
• Theorem 5: locally split topological extension classification: Cocycle-class quotient, extension equivalence quotient, and canonical two-way classification map (hard)
• Lemma 6: positivity of open sets and measurable preimages: nonzero left-invariant Borel measures; Lindelof space; measurable group homomorphism (source-ambiguity)
• Corollary 3: injectivity into measurable cohomology: Canonical degree-two lcm-to-measurable quotient comparison (hard)
• Corollary 4: two degree-two comparison regimes: Both canonical degree-two continuous/lcm/measurable comparison homomorphisms in both regimes (hard)
• Proposition 7: smooth invariants, degree one and coefficient long exact sequence: Smooth cohomology quotients and actual coefficient connecting maps with exactness (source-ambiguity)
• Theorem 7: classification of Lie-group extensions: Smooth regular-cochain H^2 and quotient of fixed-action Lie extensions with measurable locally smooth sections (hard)
• Remark 6: identity-component construction from local regularity: Constructed identity-component topology and smooth atlas for a nonmeasurable-away-from-identity cocycle (hard)
• Theorem 8: canonical smooth/continuous degree-two comparison: Canonical inclusion-induced homomorphism between actual locally smooth and locally continuous measurable H^2 (hard)
• Moore background: exactness, degree one and comparisons: measurableCochains; continuousCochains; regularCohomology; coefficientConnectingMaps; crossedHomQuotient; continuousCohomology; measurableCohomology (hard)
• Continuous-cohomology background: abstract finite-group case and profinite limits: continuousCochains; regularCohomology; abstract group cohomology; direct-limit comparison; continuousCohomology (source-ambiguity)
• Rajan background: measurable Schur cohomology of Weil groups: Weil group of a number field; measurableCochains; regularCohomology; nonzero complex numbers; measurableCohomology; weilGroup (hard)
• Banach background: automatic continuity: PolishSpace; Borel measurable homomorphism; continuous homomorphism (hard)
• Hilbert fifth and finite-dimensional Lie-group regularity background: finite-dimensional Lie group; locally Euclidean topology; closed subgroup theorem; smooth quotient submersion; local section (hard)
• Riesz representation and Fell–Doran measure-construction background: compactly supported continuous maps; leftInvariantIntegral; leftInvariantBorelMeasure; Lusin approximation (hard)

Selected references

• On Cohomology theory for topological groups, arXiv:1009.4519v1, https://arxiv.org/abs/1009.4519v1

Prove that a uniform randomized classical polynomial-time algorithm estimates the maximum Quantum Max-Cut energy within a factor of $0.595$ on every graph with nonnegative rational edge weights.

The output is a nonnegative rational number $v(G,R)$ satisfying $v(G,R)\le \mathrm{OPT}(G)$ for every prescribed random tape and $\mathbb E_R[v(G,R)]\ge 0.595\,\mathrm{OPT}(G)$. The expectation is over the algorithm’s internal fair random bits, separately for each input graph; running time is polynomial on every run. Here $\mathrm{OPT}(G)=\lambda_{\max}(\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij}))$.

Lee and Parekh (ICALP 2024), Theorem 11, obtain this expected guarantee by combining GP rounding with a maximum-matching state. Reference table. Source.

The goal uses the campaign’s shared classical numerical-output model. A complete proof must justify finite-bit computation, precision, randomization and the stated ratio. The algorithm may use any valid construction.

Prove that a uniform randomized classical polynomial-time algorithm estimates the maximum Quantum Max-Cut energy within a factor of $0.603$ on every graph with nonnegative rational edge weights.

The output is a nonnegative rational number $v(G,R)$ satisfying $v(G,R)\le \mathrm{OPT}(G)$ for every prescribed random tape and $\mathbb E_R[v(G,R)]\ge 0.603\,\mathrm{OPT}(G)$. The expectation is over the algorithm’s internal fair random bits, separately for each input graph; running time is polynomial on every run. Here $\mathrm{OPT}(G)=\lambda_{\max}(\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij}))$.

The QMC reference attributes this value to Gribling, Sinjorgo and Sotirov’s improved Lee–Parekh analysis using a level-13 sum-of-squares matching bound. The cited work is a public preprint. Reference table. Source.

The goal uses the campaign’s shared classical numerical-output model. A complete proof must justify finite-bit computation, precision, randomization and the stated ratio. The algorithm may use any valid construction.

Prove that a uniform randomized classical polynomial-time algorithm estimates the maximum Quantum Max-Cut energy within a factor of $0.614$ on every graph with nonnegative rational edge weights.

The output is a nonnegative rational number $v(G,R)$ satisfying $v(G,R)\le \mathrm{OPT}(G)$ for every prescribed random tape and $\mathbb E_R[v(G,R)]\ge 0.614\,\mathrm{OPT}(G)$. The expectation is over the algorithm’s internal fair random bits, separately for each input graph; running time is polynomial on every run. Here $\mathrm{OPT}(G)=\lambda_{\max}(\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij}))$.

The QMC reference attributes this value jointly to ALMPS25’s partially entangled matching algorithms and BBKL26’s later matching bound. The ESA 2025 paper alone states 0.611; this 0.614 target also cites the public BBKL26 preprint. Reference table. Source 1 · Source 2.

The goal uses the campaign’s shared classical numerical-output model. A complete proof must justify finite-bit computation, precision, randomization and the stated ratio. The algorithm may use any valid construction.

Approximation for quantum spin systems

Quantum Max-Cut asks for a high-energy state of an antiferromagnetic spin system specified by a weighted graph. Vertices carry qubits, and an edge rewards the two qubits for occupying their antisymmetric singlet state. A single qubit participates in several interactions, so maximizing each edge separately generally gives incompatible demands. The problem supplies a concrete setting in which to compare efficiently generated quantum states with the best state allowed by quantum mechanics.

The relevant quantity is an approximation ratio: a constant fraction of the optimum that one algorithm guarantees on every input graph. The target concerns the whole input family, rather than favorable examples or numerically observed performance. Gharibian and Parekh established an efficient product-state guarantee of 0.498 in 2019. Parekh and Thompson subsequently established a 1/2 product-state guarantee. Later algorithms use entanglement to improve the general-graph ratio, including 0.595, 0.611, and the 0.614 efficient guarantee of Bakshi, Basu, Kothari, and Li. These mathematical results provide targets for formalization; their existence does not supply Lean proofs in the shared model.

The graph and its energy

An input consists of a finite vertex set $\{0,\ldots,n-1\}$ and a nonnegative rational weight $w_{ij}$ for each unordered pair $i<j$. A zero weight represents an absent edge. The associated Hamiltonian is

$$H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij})=\frac12\sum_{i<j}w_{ij}(I-X_iX_j-Y_iY_j-Z_iZ_j).$$

Here $\mathrm{SWAP}_{ij}$ exchanges qubits $i$ and $j$, and $X,Y,Z$ are the Pauli matrices. This fixes the normalization: a singlet earns energy $2$ on a unit-weight edge, and an antiparallel computational-basis pair earns $1$. A quantum state is represented by complex amplitudes indexed by bitstrings. Its squared norm is the sum of the squared absolute values of those amplitudes. The energy is evaluated by a finite sum of squared amplitude differences under coordinate swaps, equal to the Hamiltonian expectation in this convention.

A prepared state may use additional qubits, called ancillas. The input graph occupies the first $n$ output wires. The Hamiltonian acts only on these wires, while the other wires are retained. This convention includes mixed states on the graph qubits and averages over quantum measurement outcomes without selecting a favorable outcome.

Formalization target

The first open campaign target is $\alpha=0.498=249/500$. Prove that there exists one uniform polynomial-time quantum algorithm satisfying

$\forall G,\quad E_G(A(G))\ge 0.498\,\mathrm{OPT}(G).$

The optimum ranges over all normalized quantum states on the graph qubits, including entangled states. The formal statement expresses the same comparison by requiring the output energy to dominate $0.498$ times the energy of every normalized comparison state. One algorithm and one polynomial runtime bound must work for every input graph. The output may depend on the graph and cannot depend on the comparison state used to test the inequality.

The target is an exact existential guarantee in the campaign's shared model. It does not prescribe a rounding method or a restricted output-state family. The $0.25$ foundation is already proved; $0.498$ is the next open value, and $0.5$ remains a later challenge.

What a formal proof establishes

The $0.498$ target follows the historical general-graph guarantee of Gharibian and Parekh (2019), Theorem 6, as summarized in the Quantum MaxCut reference. This mission requests a proof of algorithmic existence under the common finite H/T/CNOT circuit model. The cited paper motivates the numerical target; transferring ideal real-valued rounding into this exact gate model still requires preparation and precision justification.

A successful Lean development connects a finite classical computation, its output preparation circuit, and the energy guarantee. The existing server-accepted $1/4$ proof supplies a fully verified starting point. Contributions may follow any mathematically sound route to the common existential theorem; a stronger guarantee also suffices.

The mathematical and computational obligations

The central obligation is to exhibit an algorithm and prove both its runtime and its worst-case energy guarantee. The assertion that some state attains the optimum does not provide an algorithm for finding or preparing it. Likewise, a short circuit description alone is insufficient unless the circuit can be generated uniformly in polynomial time from the encoded graph.

The optimal state may have entanglement across many vertices. A proposed algorithm therefore has to be compared against all quantum states, rather than only against product states or its own output family. Local edge gains must be justified under the simultaneous state preparation on the entire graph. The formalization also needs to account for exact rational input comparisons, empty graphs, zero-weight edges, and any ancillary wires.

Formalization scope

The foundation is pinned to Lean 4.33.1 and its selected Mathlib environment. The computational model is a uniform classical polynomial-time generator of finite circuits over H, T, and CNOT, followed by execution of the generated circuit. Every wire starts in the all-zero state. CNOT requires distinct control and target wires. The definition uses Mathlib's explicit polynomial-time Turing-machine predicate, not a freely assumed efficiency label.

Rational numerators and denominators have fixed binary encodings. The graph order, circuit width, and gate wire indices are encoded in unary, and every gate is listed explicitly. Unary wire indices add only polynomial overhead because register width is already unary. Thus the input cannot hide an exponentially large vertex set, and a short output cannot hide an exponentially large ancillary register or an implicit circuit. The expected-energy inequality retains all output branches. It is not a claim that each individual run attains the bound or that the output energy can be simulated classically in polynomial time.

The ratio is exact in this fixed gate model. An argument using ideal arbitrary real rotations needs a separate preparation and precision justification; approximate universality by itself does not preserve an exact sharp threshold. The shared model contains no custom axioms or unproved supporting lemmas. The open goal theorem intentionally has an unfinished proof. Contributions establishing the state semantics, energy inequalities, concrete circuit generators, and their genuine runtime certificates all support the final existence theorem.

Historical context

The Quantum MaxCut reference records the progression from the $0.498$ general-graph guarantee of GP19 to $1/2$ and later improvements. The campaign begins with a completed Lean proof at $0.25$, then asks for $0.498$ as its first open target. Published mathematical values and the campaign's verified record are distinct: this mission has no accepted proof yet.

Selected references

• Sevag Gharibian and Ojas Parekh, Almost Optimal Classical Approximation Algorithms for a Quantum Generalization of Max-Cut, APPROX/RANDOM 2019. Paper.
• Anurag Anshu, David Gosset, and Karen Morenz, Beyond product state approximations for a quantum analogue of Max Cut, TQC 2020, Lemma 1, Eq. (9). Paper.
• Ojas Parekh and Kevin Thompson, An Optimal Product-State Approximation for 2-Local Quantum Hamiltonians with Positive Terms, 2022, revised 2026. Paper.
• Eunou Lee and Ojas Parekh, An Improved Quantum Max Cut Approximation via Maximum Matching, ICALP 2024. Paper.
• Anuj Apte, Eunou Lee, Kunal Marwaha, Ojas Parekh, and James Sud, Improved Algorithms for Quantum MaxCut via Partially Entangled Matchings, ESA 2025. Paper.
• Bakshi, Basu, Kothari, and Li, Sharp Bounds on the Eigenvalues of Kikuchi Graphs and Applications to Quantum Max Cut, 2026, Theorem 1.3. Paper.

Approximation for quantum spin systems

Quantum Max-Cut asks for a high-energy state of an antiferromagnetic spin system specified by a weighted graph. Vertices carry qubits, and an edge rewards the two qubits for occupying their antisymmetric singlet state. A single qubit participates in several interactions, so maximizing each edge separately generally gives incompatible demands. The problem supplies a concrete setting in which to compare efficiently generated quantum states with the best state allowed by quantum mechanics.

The relevant quantity is an approximation ratio: a constant fraction of the optimum that one algorithm guarantees on every input graph. The target concerns the whole input family, rather than favorable examples or numerically observed performance. Gharibian and Parekh established an efficient product-state guarantee of 0.498 in 2019. Parekh and Thompson subsequently established a 1/2 product-state guarantee. Later algorithms use entanglement to improve the general-graph ratio, including 0.595, 0.611, and the 0.614 efficient guarantee of Bakshi, Basu, Kothari, and Li. These mathematical results provide targets for formalization; their existence does not supply Lean proofs in the shared model.

The graph and its energy

An input consists of a finite vertex set $\{0,\ldots,n-1\}$ and a nonnegative rational weight $w_{ij}$ for each unordered pair $i<j$. A zero weight represents an absent edge. The associated Hamiltonian is

$$H_G=\sum_{i<j}w_{ij}(I-\mathrm{SWAP}_{ij})=\frac12\sum_{i<j}w_{ij}(I-X_iX_j-Y_iY_j-Z_iZ_j).$$

Here $\mathrm{SWAP}_{ij}$ exchanges qubits $i$ and $j$, and $X,Y,Z$ are the Pauli matrices. This fixes the normalization: a singlet earns energy $2$ on a unit-weight edge, and an antiparallel computational-basis pair earns $1$. A quantum state is represented by complex amplitudes indexed by bitstrings. Its squared norm is the sum of the squared absolute values of those amplitudes. The energy is evaluated by a finite sum of squared amplitude differences under coordinate swaps, equal to the Hamiltonian expectation in this convention.

A prepared state may use additional qubits, called ancillas. The input graph occupies the first $n$ output wires. The Hamiltonian acts only on these wires, while the other wires are retained. This convention includes mixed states on the graph qubits and averages over quantum measurement outcomes without selecting a favorable outcome.

Formalization target

The requested bound is $\alpha=\frac12$. The goal is the existence statement

$$\exists A,\quad A\text{ runs in polynomial time}\quad\land\quad\forall G,\ \mathbb{E}[E_G(A(G))]\ge \frac12\,\mathrm{OPT}(G).$$

The optimum ranges over all normalized quantum states on the graph qubits, including entangled states. The formal statement expresses the same comparison by requiring the output energy to dominate the scaled energy of every normalized comparison state; it does not introduce a separate optimizer or a supremum. One algorithm and one polynomial runtime bound must work for every input graph. The output may depend on the graph but cannot depend on which comparison state is used to test the inequality.

This mission fixes the starting value $1/2$. A later improvement can reuse its definitions while changing only the numerical value in the campaign template.

What a formal proof establishes

The $1/2$ bound is a known mathematical target, not a new approximation claim. The mission asks for a Lean proof of the stated algorithmic existence theorem. A successful development must connect a finite classical computation, its output preparation circuit, and the energy guarantee. Verifying only an energy inequality for an unspecified state leaves out the computational content.

The shared definitions give later work a stable meaning for input size, permissible preparation, and approximation ratio. They also make comparisons between different state families possible without changing the optimization problem. The weighted-star energy inequality of Anshu, Gosset, and Morenz is a useful established supporting result for a first proof. Supporting lemmas and reusable proofs can be developed separately while preserving the campaign's common existential target.

The mathematical and computational obligations

The central obligation is to exhibit an algorithm and prove both its runtime and its worst-case energy guarantee. The assertion that some state attains the optimum does not provide an algorithm for finding or preparing it. Likewise, a short circuit description alone is insufficient unless the circuit can be generated uniformly in polynomial time from the encoded graph.

The optimal state may have entanglement across many vertices. A proposed algorithm therefore has to be compared against all quantum states, rather than only against product states or its own output family. Local edge gains must be justified under the simultaneous state preparation on the entire graph. The formalization also needs to account for exact rational input comparisons, empty graphs, zero-weight edges, and any ancillary wires.

Formalization scope

The foundation is pinned to Lean 4.33.1 and its selected Mathlib environment. The computational model is a uniform classical polynomial-time generator of finite circuits over H, T, and CNOT, followed by execution of the generated circuit. Every wire starts in the all-zero state. CNOT requires distinct control and target wires. The definition uses Mathlib's explicit polynomial-time Turing-machine predicate, not a freely assumed efficiency label.

Rational numerators and denominators have fixed binary encodings. The graph order, circuit width, and gate wire indices are encoded in unary, and every gate is listed explicitly. Unary wire indices add only polynomial overhead because register width is already unary. Thus the input cannot hide an exponentially large vertex set, and a short output cannot hide an exponentially large ancillary register or an implicit circuit. The expected-energy inequality retains all output branches. It is not a claim that each individual run attains the bound or that the output energy can be simulated classically in polynomial time.

The ratio is exact in this fixed gate model. An argument using ideal arbitrary real rotations needs a separate preparation and precision justification; approximate universality by itself does not preserve an exact sharp threshold. The shared model contains no custom axioms or unproved supporting lemmas. The open goal theorem intentionally has an unfinished proof. Contributions establishing the state semantics, energy inequalities, concrete circuit generators, and their genuine runtime certificates all support the final existence theorem.

Selected references

• Sevag Gharibian and Ojas Parekh, Almost Optimal Classical Approximation Algorithms for a Quantum Generalization of Max-Cut, APPROX/RANDOM 2019. Paper.
• Anurag Anshu, David Gosset, and Karen Morenz, Beyond product state approximations for a quantum analogue of Max Cut, TQC 2020, Lemma 1, Eq. (9). Paper.
• Ojas Parekh and Kevin Thompson, An Optimal Product-State Approximation for 2-Local Quantum Hamiltonians with Positive Terms, 2022, revised 2026. Paper.
• Eunou Lee and Ojas Parekh, An Improved Quantum Max Cut Approximation via Maximum Matching, ICALP 2024. Paper.
• Anuj Apte, Eunou Lee, Kunal Marwaha, Ojas Parekh, and James Sud, Improved Algorithms for Quantum MaxCut via Partially Entangled Matchings, ESA 2025. Paper.
• Bakshi, Basu, Kothari, and Li, Sharp Bounds on the Eigenvalues of Kikuchi Graphs and Applications to Quantum Max Cut, 2026, Theorem 1.3. Paper.

Motivation

Metabolic control analysis (MCA) describes how changes in enzyme activities propagate through a biochemical network. It is used to separate local biochemical sensitivity from global system-level control, which is relevant to pathway engineering, drug-target analysis, and quantitative interpretation of steady-state experiments. The summation and connectivity theorems are the algebraic backbone of this framework: they constrain how concentration control, flux control, and local elasticities can vary together. The source formalized here is Weijiu Liu, “Simple Proofs of the Summation and Connectivity Theorems in Metabolic Control Analysis,” arXiv:2501.12519v2 (2025), especially Sections 2–3: https://arxiv.org/abs/2501.12519.

Setting

Fix finite index types Fin n for reactions and Fin m for internal concentrations. A parameter vector is a function p : Fin n → ℝ, and a steady-state concentration map is s : (Fin n → ℝ) → (Fin m → ℝ). Each enzyme-catalysed rate is represented by a function f k : (Fin m → ℝ) → ℝ, with total rate v_k(p) = p_k f_k(s(p)). A stoichiometric matrix N : Matrix (Fin m) (Fin n) ℝ maps reaction rates to concentration dynamics; the steady-state condition is N.mulVec (fun k => v_k(p)) = 0 for every parameter vector.

The formal development defines the derivative matrix D from Mathlib's Fréchet derivative fderiv, with entries D k j = ∂f_k/∂s_j, and the sensitivity matrix S with entries S i l = ∂s_i/∂p_l. It then defines the dimensionless elasticity, concentration-control, and flux-control coefficients by logarithmic derivatives:

$$\varepsilon_{kj}=\frac{s_j}{f_k}\frac{\partial f_k}{\partial s_j},\qquad C^S_{il}=\frac{p_l}{s_i}\frac{\partial s_i}{\partial p_l},\qquad C^J_{rl}=\frac{p_l}{J_r}\frac{\partial J_r}{\partial p_l}.$$

Here J = R v is any finite collection of linear fluxes obtained from a matrix R : Matrix (Fin q) (Fin n) ℝ.

Formalization targets

Concentration connectivity (goal)

Under differentiability of every f k and of s, the all-parameter steady-state identity, a left inverse for N * diagonal p * D, and the required nonzero concentration and rate values, prove

$$C^S\,\varepsilon=-I_m.$$

The Lean goal is the theorem MCAEndToEndMission.concentration_connectivity, stated as the normalized form of the published MCAEndToEnd.normalized_connectivity result.

Concentration summation

If the steady-state map is homogeneous of degree zero, prove for every concentration index i

$$\sum_l C^S_{il}=0.$$

Flux summation

If the steady-state map is homogeneous of degree zero and each selected flux is nonzero, prove for every flux index r

$$\sum_l C^J_{rl}=1.$$

Flux connectivity

Under the same differentiability, steady-state, inverse, and nondegeneracy assumptions, prove for every flux r and concentration index j

$$\sum_l C^J_{rl}\varepsilon_{lj}=0.$$

Significance

The four identities describe complementary conservation laws for local and global control. Concentration summation expresses invariance under a common rescaling of all enzyme parameters. Flux summation records first-degree homogeneity of fluxes in those parameters. Concentration connectivity relates parameter sensitivity to local concentration elasticity, while flux connectivity states that the induced flux-control vector annihilates the elasticity matrix. Together they provide consistency checks for analytic calculations and a reusable interface for later MCA results.

The mathematical results are already machine-checked in the published Lean definition MCAEndToEnd_formalization. This mission packages the four theorem statements as an auditable research-paper formalization with a clean dependency on that definition. It preserves the explicit derivative construction, chain-rule proofs, product-rule calculation, diagonal inverse identities, and all nondegeneracy conditions, so future work can reuse the declarations rather than treating the control coefficients as free matrices.

Difficulty

The main difficulty is keeping the matrix dimensions and derivative conventions aligned across three levels: reaction-rate derivatives, the steady-state concentration map, and linear flux combinations. The steady-state equation is an identity of functions, so its derivative must be obtained from Mathlib's chain and product rules before matrix algebra can be applied. Homogeneity is also only assumed for positive scalars, requiring a local derivative argument at c = 1; replacing it with an unrestricted algebraic scaling axiom would change the theorem. Finally, the connectivity statements require division by concentrations, enzyme rates, and fluxes, so all corresponding nonzero hypotheses are explicit.

Formalization scope

The Lean representation uses finite-dimensional real vector spaces encoded as functions on Fin, finite sums, and Mathlib's fderiv and HasFDerivAt. The development is noncomputable but contains no sorry, admit, or axiom, and the complete file compiles under the pinned platform environment. The stoichiometric matrix, rate functions, state map, and flux map remain general; no numerical network or hard-coded special case is used. The left-inverse assumption is retained because it is the structural rank condition needed to derive concentration connectivity, while rate, concentration, parameter, and flux nonzero conditions govern the logarithmic normalizations. Reusable infrastructure includes the derivative-matrix interface, finite-dimensional continuous-linear-map expansion lemmas, steady-state linearization, homogeneous Euler identities, and diagonal inverse calculations.

Selected references

• Weijiu Liu, Simple Proofs of the Summation and Connectivity Theorems in Metabolic Control Analysis, arXiv (2025), Sections 2–3. https://arxiv.org/abs/2501.12519
• Henrik Kacser and John A. Burns, The control of flux, Symposia of the Society for Experimental Biology 27 (1973), 65–104. https://doi.org/10.1111/j.2042-3306.1973.tb02402.x
• David A. Fell, Understanding the Control of Metabolism, Portland Press (1997). https://doi.org/10.1042/9781855739082

Motivation

The Fisher information of a real random variable measures how sharply its density is peaked: it is the information an observation $X=\theta+N$ carries about a translation parameter $\theta$, and by the Cramér–Rao bound its reciprocal is the smallest variance of an unbiased estimator of $\theta$. The Fisher information inequality (FII) says how this quantity behaves under the addition of independent noise. It was proved by Stam (1959) and Blachman (1965) as the key step in their proof of Shannon's entropy power inequality, and it remains a standard tool in information theory, in the information-theoretic proofs of the central limit theorem, and in statistical physics.

Liu and Viswanath (arXiv:cs/0604028) give two new proofs of the FII from data processing inequalities: one for mutual information (§2.1) and one for conditional variance (§2.2). This mission formalizes the inequality and the steps of the second, Bayesian estimation, proof.

Timeline.

• 1959, Stam: the FII and the conditional-mean representation of the score of a sum; the entropy power inequality via de Bruijn's identity.
• 1965, Blachman: a streamlined version of Stam's argument.
• 1998, Zamir (IEEE Trans. IT 44): a proof from the data processing inequality for Fisher information itself.
• 2006, Liu–Viswanath: proofs from data processing for mutual information and for conditional variance, the latter via an identity (Lemma 1) linking Fisher information and minimum mean-square error in Gaussian noise, related to the I-MMSE relation of Guo, Shamai and Verdú (IEEE Trans. IT 51, 2005).

Setting

Let $X$ be a real random variable whose law has a density $f$ that is absolutely continuous, with derivative $f'$. The score of $X$ is $\rho_X=f'/f=\frac{\partial}{\partial x}\ln f$, and the Fisher information is

$$J(X)=\mathbb E\big[\rho_X(X)^2\big]=\int_{\mathbb R}\frac{f'(x)^2}{f(x)}\,dx\in[0,\infty].$$

It depends on the law of $X$ only. If the law has no absolutely continuous density, $J(X)=+\infty$. In Lean: IsACDensity μ f g (a density f of μ with derivative g), fisherInfo μ, and score μ, applied to the law P.map X.

For a real random variable $W$ and an observation $X$, the conditional variance (minimum mean-square error) is the number

$$\mathrm{VAR}[W\mid X]=\mathbb E\big[(W-\mathbb E[W\mid X])^2\big],$$

in Lean mmse P W X. Random variables $W\to X\to Y$ form a Markov chain when $W$ and $Y$ are conditionally independent given $X$ (IsMarkovChain).

The proof works with the Bayesian estimation model (22): for $a,b\ge0$ and $t>0$,

$$X_1=N_1+\sqrt{at}\,W_1,\qquad X_2=N_2+\sqrt{bt}\,W_2,$$

with $W_1,W_2$ standard Gaussian and $N_1,N_2,W_1,W_2$ mutually independent.

Formalization targets

Goal: the Fisher information inequality, eq. (4)

For independent real random variables $N_1,N_2$ with densities and all $a,b\ge0$,

$$(a+b)^2J(N_1+N_2)\le a^2J(N_1)+b^2J(N_2).$$

No finiteness of $J(N_1)$, $J(N_2)$ is assumed.

Milestones, in the order the proof uses them

1. Eq. (6): $\rho_{N_1+N_2}(N_1+N_2)=\mathbb E[\rho_{N_1}(N_1)\mid N_1+N_2]$ for independent $N_1,N_2$ with an integrable score $\rho_{N_1}(N_1)$.
2. Lemma 1: for $W\sim N(0,\sigma^2)$ independent of $N$, $J(N+W)=\sigma^{-4}\{\sigma^2-\mathrm{VAR}[N\mid N+W]\}$.
3. Eq. (13): if $W\to X\to Y$, then $\mathrm{VAR}[W\mid Y]\ge\mathrm{VAR}[W\mid X]$.
4. Eq. (28): in model (22), $\mathrm{VAR}[N_1+N_2\mid X_1,X_2]=\mathrm{VAR}[N_1\mid X_1]+\mathrm{VAR}[N_2\mid X_2]$.
5. Eq. (29): in model (22), $(a+b)^2J(X_1+X_2)\le a^2J(X_1)+b^2J(X_2)$.
6. After (29): $J(N+\sqrt s\,W)\to J(N)$ as $s\downarrow0$, in $[0,\infty]$.

Significance

The FII gives the canonical form $1/J(N_1+N_2)\ge1/J(N_1)+1/J(N_2)$ (choose $a=1/J(N_1)$, $b=1/J(N_2)$), and through de Bruijn's identity it integrates to the entropy power inequality, which bounds the capacity of additive-noise channels and of Gaussian broadcast and wiretap channels. Lemma 1 is of independent use: it expresses the Fisher information of a Gaussian-perturbed variable through an estimation error, the link behind the I-MMSE identities.

The result has been proved since 1959; this mission produces a machine-checked proof. To the best of the curators' knowledge, neither Mathlib nor this platform has the classical Fisher information of a real law, the score of a sum, or the MMSE identities; they are formalized here for the first time. The equality case of the canonical form ("if and only if both are Gaussian") is not part of the mission: the paper states that its proofs do not give it.

Difficulty

Each step in the paper is a line, but each rests on analytic facts the text takes for granted. Eq. (6) requires differentiating the convolution density of $N_1+N_2$ under the integral sign with only an integrable score. Lemma 1 needs the Gaussian score $\rho_W(w)=-w/\sigma^2$ and the orthogonality of the estimation error, which holds in $L^2$ while $N$ need not even be integrable (the conditional mean is that of the conditional law of $N$ given $N+W$, which has Gaussian tails). The final step needs the limit $J(N+\sqrt s\,W)\to J(N)$, which is a lower-semicontinuity statement for Fisher information under weak convergence, including the case $J(N)=\infty$; the inequality $J(N+\sqrt sW)\le J(N)$ alone gives only half of it.

The naive reading of the paper's independence assumption fails: under pairwise independence of $N_1,N_2,W_1,W_2$, eq. (28) is false (a counterexample is recorded on the milestone). The proof needs mutual independence, which it may assume since it chooses $W_1,W_2$ itself.

Formalization scope

Random variables are measurable maps $\Omega\to\mathbb R$ on a probability space (Ω, P); $J$ of a random variable is fisherInfo (P.map X), valued in ℝ≥0∞, and the coefficients are ENNReal.ofReal of the real squares, so $0\cdot\infty=0$. The Gaussian law is Mathlib's gaussianReal 0 v, with $v$ the variance. In (6) the conditional expectation is Mathlib's condExp on the $\sigma$-algebra generated by $N_1+N_2$. In mmse the conditional mean $\mathbb E[W\mid X=x]$ is the mean of the regular conditional law condDistrib W X P, as in the paper's $\mathbb E[N\mid X=x]$; it agrees with condExp for integrable $W$ and needs no integrability, so no statement about mmse assumes any. VAR is the expected conditional variance (a number), not Mathlib's condVar (a random variable).

The definition of $J$ cannot be trivialized: the mission's sanity checks prove $J(N(0,v))=1/v$, $J(\mathrm{Unif}[0,1])=J(\delta_c)=+\infty$, and that every absolutely continuous representation of a density gives the same value. A finiteness hypothesis on $J$ in the goal would make it a special case and is ruled out.

Reusable beyond this mission: the definitions of Fisher information and score of a real law, the MMSE, and the elementary Markov-chain predicate; the score-of-a-sum identity (6) and the Gaussian-smoothing limit are standard lemmas of information theory. Contributions are welcome on each milestone and on supporting lemmas (convolution densities, the Gaussian score, the orthogonality principle for conditional laws).

Selected references

• T. Liu, P. Viswanath, Two Proofs of the Fisher Information Inequality via Data Processing Arguments, arXiv:cs/0604028v1, 2006. https://arxiv.org/abs/cs/0604028
• A. J. Stam, Some inequalities satisfied by the quantities of information of Fisher and Shannon, Information and Control 2(2), 101–112, 1959. https://doi.org/10.1016/S0019-9958(59)80010-7
• N. M. Blachman, The convolution inequality for entropy powers, IEEE Trans. Inform. Theory 11(2), 267–271, 1965. https://doi.org/10.1109/TIT.1965.1053768
• R. Zamir, A proof of the Fisher information inequality via a data processing argument, IEEE Trans. Inform. Theory 44(3), 1246–1250, 1998. https://doi.org/10.1109/18.669301
• D. Guo, S. Shamai (Shitz), S. Verdú, Mutual information and minimum mean-square error in Gaussian channels, IEEE Trans. Inform. Theory 51(4), 1261–1282, 2005. https://doi.org/10.1109/TIT.2005.844072

Motivation

Tensor networks represent the state of a many-body quantum system on $N$ sites as a contraction of small tensors, one per vertex of a graph. They underlie the matrix product state, PEPS and MERA methods of condensed-matter physics and quantum chemistry. Many physical systems have a global symmetry: a group $G$ acting by the same unitary $U_g$ on every site, under which the state is invariant, $(U_g)^{\otimes N}|\Psi\rangle=|\Psi\rangle$. Particle-number conservation ($G=U(1)$) and spin isotropy ($G=SU(2)$) are the standard examples.

Singh, Pfeifer and Vidal (arXiv:0907.2994) observe that such a state can be written with symmetric tensors, each invariant under the simultaneous action of $G$ on its indices, and they describe the structure of these tensors. Every symmetric tensor splits into degeneracy tensors, which carry all the free parameters, and structural tensors, which depend only on the group. This is the basis of symmetry-exploiting numerical codes for $U(1)$ and $SU(2)$ (arXiv:1008.4774), and it identifies the symmetric part of a tensor network with a spin network, the object used in loop quantum gravity (Rovelli–Smolin 1995).

Setting

Fix a group $G$ and a catalogue of irreps: a set of charges $a$ and, for each, an irreducible unitary matrix representation $U^a:G\to U(\dim a)$ on $\mathbb V^a=\mathbb C^{\dim a}$, with distinct charges labelling inequivalent irreps. The charge $0$ is the trivial irrep, $\dim 0=1$, $U^0_g=1$.

Fusion data decomposes tensor products, Eq. (9): $\mathbb V^a\otimes\mathbb V^b\cong\bigoplus_cN^c_{ab}\mathbb V^c$. For each pair $(a,b)$ there is a finite set of channels $\kappa$ with output charge $c=\mathrm{out}(\kappa)$ and an isometry $\iota_\kappa=(Q^{abc})_{m_an_bo_c}$, the Clebsch–Gordan coefficients, which intertwines $U^a\otimes U^b$ with $U^c$. The isometries are orthonormal and complete. Conjugation data gives, for each $a$, a charge $\bar a$ and a unitary $J^a$ with $J^a\overline{U^a_g}=U^{\bar a}_gJ^a$.

A tensor $T$ has a finite set $S$ of legs, each outgoing or incoming. The index of a leg is $i=(a,\alpha_a,m_a)$, where $a$ is a charge, $\alpha_a$ labels a basis vector of a finite degeneracy space $\mathbb D^a$ and $m_a$ labels a basis vector of $\mathbb V^a$ (Eq. (4)). The group acts on an outgoing leg by $\bigoplus_a(\mathbb I^a\otimes U^a_g)$ (Eq. (5)) and on an incoming leg by its complex conjugate. $T$ is symmetric when it is invariant under the simultaneous action on all legs, as in Eq. (7).

A fusion tree $\tau$ for a root leg $r$ is a binary tree whose leaves are the other legs, each exactly once. Fix leg charges $a_s$. A labelling $\ell$ assigns a channel to every inner node, and so an intermediate charge $e_k$ to every inner branch; it is admissible when the tree fuses into the root's charge. The structural tensor $Q(a,\ell)$ composes the isometries $\iota_\kappa$ along the tree. It is defined from the fusion data alone: the paper's $\delta_{ab}\delta_{m_an_b}$ for two legs, $Q^{abc}$ for three legs, and $\sum_qQ^{abe}_{m_an_bq}Q^{ecd}_{qo_cp_d}$ for four legs.

Formalization targets

Goal: Eq. (15)

For every valid tree $\tau$ and all degeneracy spaces, the map from unconstrained degeneracy families $P$ to tensors

$$T_{i_1\dots i_t}=\sum_{\ell}\big(P^{a_1\dots a_t}_{\ell}\big)_{\alpha_{a_1}\dots\alpha_{a_t}}\big(Q^{a_1\dots a_t}_{\ell}\big)_{m_{a_1}\dots m_{a_t}}$$

is a bijection onto the symmetric tensors. For two trees $\tau,\tilde\tau$ with the same root, there are unitary matrices $F(a)$, fixed by the symmetry before any tensor is chosen, with

$$\tilde Q_{\tilde\ell}=\sum_\ell F_{\ell\tilde\ell}\,Q_\ell,\qquad \tilde P_{\tilde\ell}=\sum_\ell\overline{F_{\ell\tilde\ell}}\,P_\ell .$$

These are the paper's three claims: $P$ holds all the degrees of freedom, $Q$ is determined by the symmetry, and a change of tree is an F-move.

Milestones

1. Eqs. (4)–(5): a unitary representation is unitarily equivalent to $\bigoplus_a(\mathbb I^a\otimes U^a_g)$.
2. Eq. (9): fusion and conjugation data exist for a catalogue closed under tensor products and conjugates.
3. One leg: a one-leg tensor is symmetric exactly when it lives on charge $0$.
4. Eq. (10): the Wigner–Eckart theorem, $T_{ijk}=\sum_\kappa P^{abc}_\kappa Q^{abc}_\kappa$, with $P$ unique.
5. Eqs. (11) and (12): four legs, with the two trees $((ab)c)$ and $(a(bc))$.
6. Eqs. (13) and (14): the unitary $F^{abc}_d$ relating the two four-leg bases, and $\tilde P=F^\dagger P$.
7. The tree basis: the fusion-tree maps are orthonormal intertwiners that span all intertwiners from $U^c$ into a tensor product of irreps, and for any leg directions and root the structural tensors of a tree form a basis of the intertwiners between the tensor products of incoming and outgoing irreps.

Significance

The decomposition lets a numerical code store only the degeneracy tensors. Contractions then become blockwise products, and quantum numbers are preserved exactly during approximate simulation. The paper reports 5 and 35 times fewer parameters for $U(1)$ and $SU(2)$ MERA (p.4). The statement also shows that, for fixed charges, a symmetric tensor network is a linear superposition of spin networks, with the degeneracy tensors as coefficients.

The paper gives no proofs: it cites Schur's lemma and the Wigner–Eckart theorem. None of this is formalized on the platform. A related open item, NonAbelianDMNRG.Recursion.eq_43, poses the two-leg case (Eqs. (6), (8)). Other platform results cover a tensor-product decomposition up to linear (not unitary) equivalence and a Wigner–Eckart factorization for polynomial irreps of $U(d)$. The mission adds fusion trees, labellings by intermediate charges, recoupling unitaries, and a general uniqueness statement for every number of legs and every choice of directions.

Difficulty

For fixed charges, a block of $T$ is an invariant vector in a tensor product of irreps and conjugate irreps, and such vectors correspond to intertwiners from one irrep into a tensor product of irreps. The main step is to show, by induction over an arbitrary tree, that the composed Clebsch–Gordan isometries form an orthonormal family that exhausts this space. Schur's lemma then gives uniqueness. Leg order is arbitrary, so the trees are not planar, and the two trees in the change-of-tree clause need not differ by a single move. The direct route, which composes elementary F-moves of Eq. (13), does not apply. Unitarity of $F$ instead follows because both families of structural tensors are orthogonal with the same norm, and this holds only for a common root. Carrying the leg directions through the conjugation unitaries $J^a$, and the dependent index types $\mathrm{Fin}(\dim a)$, adds a second layer of work.

Formalization scope

$G$ is an arbitrary Group with no topology. Compactness is used only for complete reducibility, which unitarity provides, so compact groups with their continuous irreps are an instance. Irreps are unitary matrix representations G →* Matrix.unitaryGroup (Fin (dim a)) ℂ. The catalogue may be infinite and is part of the data, with irreducibility and pairwise inequivalence as fields. Multiplicity freeness is not assumed: channels play the role of the paper's pairs $(c,\mu)$ (footnote [10]). The leg index $(a,\alpha_a,m_a)$ is encoded as a finite set of degeneracy labels $\alpha$, each carrying a charge, together with $m\in\mathrm{Fin}(\dim a)$. Degeneracy spaces may be empty.

The intermediate index $q_e$ of Eqs. (11), (12), (15) is contracted inside $Q$. No intermediate degeneracy index $\epsilon_e$ is attached to $P$: the paper itself writes $\tilde Q$ without $r_f$, and Fig. 2(iv) shows the inner edge only in the structural part.

A trivializing reading is excluded: $Q$ is a definition computed from the fusion data before the degeneracy spaces and $T$ are introduced, $P$ is unconstrained, and $F$ is quantified before any tensor. A proved $\mathbb Z_2$ instance shows that the hypotheses can be met with a nonzero symmetric tensor.

Useful infrastructure beyond this mission: Schur's lemma for unitary matrix representations of an arbitrary group, unitary complete reducibility, and the orthonormality and completeness of composed isometries over trees. Contributions to these lemmas are welcome, as are proofs of the milestones in any order.

Selected references

• S. Singh, R. N. C. Pfeifer, G. Vidal, Tensor network decompositions in the presence of a global symmetry, arXiv:0907.2994v2, 2010; Phys. Rev. A 82, 050301(R) (2010). https://arxiv.org/abs/0907.2994
• S. Singh, R. N. C. Pfeifer, G. Vidal, Tensor network states and algorithms in the presence of a global U(1) symmetry, Phys. Rev. B 83, 115125 (2011). https://arxiv.org/abs/1008.4774
• C. Rovelli, L. Smolin, Spin networks and quantum gravity, Phys. Rev. D 52, 5743 (1995). https://doi.org/10.1103/PhysRevD.52.5743

Motivation

General relativity has a dynamical causal structure: whether one event can influence another depends on the metric, which is itself a physical variable. Quantum theory, in its standard formulations, presupposes a fixed causal structure: states evolve in a given time, and systems are composed in a given order. A theory of quantum gravity is expected to combine the indefiniteness of quantum theory with the dynamical causal structure of general relativity. L. Hardy's paper Towards Quantum Gravity: A Framework for Probabilistic Theories with Non-Fixed Causal Structure (2006) proposes an operational framework for probabilistic theories in which no causal structure is given in advance, and in which the question "is this probability determined?" is answered by the theory instead of by reference to a background spacetime.

In ordinary physics one knows that a probability is well defined by appeal to causal structure: given the boundary conditions in the past light cone of a region and the settings chosen there, the probabilities in the region are fixed. The paper replaces that appeal by a single mathematical object, the causaloid, from which every well-defined conditional probability between two regions can be decided and computed. This mission formalizes that claim, the conclusion of §4.5.

Setting

An experiment is described by a set $X$ of locations $x$. At each location there is a set of settings $F_x$ and, for each setting $f$, a set of possible outcomes under $f$. A label at $x$ is a pair $\alpha_x=(f,y)$. A finite set $O\subseteq X$ determines a region $R_O$, and a label of $R_O$ is a family of labels $(\alpha_x)_{x\in O}$. An experiment model gives, for every choice of settings $F$ at all locations and every outcome family $Y$ under $F$, a probability $\mathrm{Prob}(Y\mid F)\ge 0$, with $\sum_Y\mathrm{Prob}(Y\mid F)=1$ for every $F$.

For a region $R_1$, what happens outside it (its settings and outcomes) is a generalised preparation $s$, and $p_{\alpha_1}(s)$ is the probability of the label $\alpha_1$ in $R_1$ together with $s$ outside. A finite set $\Omega_1$ of labels of $R_1$ is sufficient if every $p_{\alpha_1}$ is one fixed linear combination of the $p_{l_1}$, $l_1\in\Omega_1$:

$$p_{\alpha_1}(s)=\mathbf r_{\alpha_1}(R_1)\cdot\mathbf p(R_1)(s)\quad\text{for all }s,\qquad \mathbf p(R_1)(s)=(p_{l_1}(s))_{l_1\in\Omega_1}.$$

It is fiducial if no proper subset is sufficient. The vectors $\mathbf r$ of the elementary regions $R_x$ form matrices $\Lambda^{l_x}_{\alpha_x}$; for a composite region $R_O$ with fiducial set $\Omega_O\subseteq\prod_{x\in O}\Omega_x$, the vectors of the labels in $\prod_{x\in O}\Omega_x$ form matrices $\Lambda^{k}_{l}$. The causaloid is this list of matrices, eq. (30), and from it the causaloid product computes

$$\big(\mathbf r_\alpha(R_O)\big)_k=\sum_{l\in\prod_{x\in O}\Omega_x}\Big(\prod_{x\in O}\Lambda^{l_x}_{\alpha_x}\Big)\Lambda^{k}_{l}.$$

For disjoint regions $R_1,R_2$, a label $\alpha_1$ of $R_1$ and a label $\alpha_2=(Y_2,F_2)$ of $R_2$, put

$$\mathbf a=\mathbf r_{\alpha_1\alpha_2}(R_1\cup R_2),\qquad \mathbf b=\sum_{\beta_2}\mathbf r_{\alpha_1\beta_2}(R_1\cup R_2),$$

with $\beta_2$ over all outcomes under $F_2$. The conditional probability $\mathrm{Prob}(Y_2\mid Y_1,F_1,F_2)$ is well defined if the ratio of $p_{\alpha_1\alpha_2}(s)$ to $\sum_{\beta_2}p_{\alpha_1\beta_2}(s)$ takes one value under every preparation $s$ for which the denominator is nonzero.

Formalization targets

Goal: the causaloid decides and computes every conditional probability

For every model and every choice of elementary fiducial sets, a causaloid exists, and for every causaloid of the model and every pair of disjoint regions:

$$\mathrm{Prob}(Y_2\mid Y_1,F_1,F_2)\text{ is well defined}\iff \mathbf a=c\,\mathbf b\text{ for some }c\in\mathbb R\qquad(36),$$

every value $p$ satisfies $\mathbf a=p\,\mathbf b$ (37), and if $\mathbf b\neq0$ then $p=|\mathbf a|/|\mathbf b|$. The statement also records that the joint probability and the probability of the conditioning event are $\mathbf a\cdot\mathbf p(R_1\cup R_2)$ and $\mathbf b\cdot\mathbf p(R_1\cup R_2)$, that the sums over $\beta_2$ converge, and that $\mathbf b=0$ exactly when the conditioning event is impossible under every preparation.

Milestones

In proof order: existence of a finite sufficient set and of a fiducial subset (§4.2, (13)–(15)); a fiducial set has $|\Omega_1|$ linearly independent states (§4.2, p.12); the expansion (22) of $p_{\alpha_1\alpha_2}$ over $\Omega_1\times\Omega_2$; a fiducial set $\Omega_{12}\subseteq\Omega_1\times\Omega_2$ (21); the composite vector (24); the causaloid product (25)–(27); the existence of a causaloid for every region (28)–(30); and the three clauses of §4.5, (35), (36), (37).

Correction. As printed, (35) names the ratio $\mathrm{Prob}(Y_1^{\alpha_1}\mid Y_2^{\alpha_2},F_1,F_2)$. Since its denominator sums over the outcomes $\beta_2$ of region 2, the ratio is $\mathrm{Prob}(Y_2\mid Y_1,F_1,F_2)$, the probability (7) that §3 sets out to find. With one setting at each of two locations, binary outcomes and $\mathrm{Prob}(0,0)=\tfrac12$, $\mathrm{Prob}(0,1)=\tfrac14$, $\mathrm{Prob}(1,0)=0$, $\mathrm{Prob}(1,1)=\tfrac14$, one has $\mathrm{Prob}(Y_1=0\mid Y_2=0)=1$, while the printed ratio is $\tfrac{1/2}{3/4}=\tfrac23$. The mission states the corrected form; (36) and (37) are unchanged. The paper has no numbered theorems; results are cited by section and equation.

Significance

The result is the operational content of the framework: the causaloid alone answers both questions the paper sets for a physical theory (p.9), whether a probability is well defined and what it is, and it does so for any pair of regions with no causal order on the locations. The paper's later sections use this to treat quantum theory as a particular causaloid (§5) and to propose the framework as a setting for quantum gravity (§6–§7); those parts are outside this mission.

The claim is proved in the paper by a short linear-algebra argument; no machine-checked version exists. Formalizing it fixes what "well defined", "just sufficient" and "the causaloid" mean precisely, exposes the misprinted conditional in (35), and checks the argument in the generality the paper allows: arbitrary sets of locations, settings and outcomes, with no finiteness beyond that of the fiducial sets.

Difficulty

Each step is elementary; the work is in the quantifiers. Passing from "just sufficient" to "spanning states" requires the states to range over every generalised preparation, including the labels of the other region, and fails if the vector $\mathbf r$ is allowed to depend on the preparation. The vector $\mathbf b$ is an infinite sum when region 2 has infinitely many outcomes; its convergence follows only by expressing $\mathbf r$ through a basis of states. The direction "parallel ⇒ well defined" is immediate, but "well defined ⇒ parallel" needs the identity $\mathbf a\cdot\mathbf p=c\,\mathbf b\cdot\mathbf p$ also at preparations where the denominator vanishes, and that holds only because probabilities are nonnegative: for a signed array the equivalence fails.

Formalization scope

Locations are an arbitrary type with decidable equality; settings and outcomes are arbitrary types, labels are dependent pairs, and normalization is HasSum. A region is a Finset of locations. A generalised preparation is a total label whose values on the region are ignored. Fiducial sets are finite, and "just sufficient" means inclusion-minimal. The causaloid is the structure of matrices (30), with no reference to any model; a separate predicate says it is a causaloid of a given model. Well-definedness is a statement about ratios of actual probabilities over the preparations with nonzero denominator, never "$\mathbf a=c\,\mathbf b$" by definition, which would make (36) empty. Lengths are Euclidean.

No product form of the probabilities and no causal order on the locations is assumed anywhere. The development needs finite-dimensional linear algebra, unconditional sums in $\mathbb R^\Omega$, and finite products over Finsets; the definitions of sufficient and fiducial sets are stated for an arbitrary real table and are reusable for other operational frameworks. Proofs of the milestones, and alternative arguments for (21) and (24), are welcome.

Selected references

• L. Hardy, Towards Quantum Gravity: A Framework for Probabilistic Theories with Non-Fixed Causal Structure, arXiv:gr-qc/0608043v1, 2006. https://arxiv.org/abs/gr-qc/0608043
• L. Hardy, Probability Theories with Dynamic Causal Structure: A New Framework for Quantum Gravity, 2005 (cited in the paper as quant-ph/0509120; on arXiv as gr-qc/0509120). https://arxiv.org/abs/gr-qc/0509120

Motivation

An extension of a Lie algebra $\mathfrak g$ by a Lie algebra $\mathfrak n$ is a Lie algebra $\widehat{\mathfrak g}$ containing $\mathfrak n$ as an ideal with quotient $\widehat{\mathfrak g}/\mathfrak n\cong\mathfrak g$. Extensions are how larger Lie algebras are assembled from smaller ones: central extensions produce the Virasoro and affine Kac–Moody algebras from vector fields on the circle and loop algebras, semidirect products build the Lie algebras of symmetry groups of physical systems, and every finite-dimensional Lie algebra is an extension of a semisimple one by its radical.

When the kernel $\mathfrak n$ is abelian, extensions with a fixed $\mathfrak g$-module structure on $\mathfrak n$ are classified by the second Lie algebra cohomology $H^2(\mathfrak g,\mathfrak n)$. For a non-abelian kernel, $\mathfrak g$ no longer acts on $\mathfrak n$ — only on $\mathfrak n$ modulo inner derivations — and the classification needs non-abelian data. In infinite-dimensional Lie theory (Lie algebras of vector fields, current algebras, Banach–Lie algebras of operators) the extension must moreover respect a topology, so that it can be integrated to an extension of infinite-dimensional Lie groups.

Timeline (as surveyed in Neeb, pp. 1–2):

• 1948 — Chevalley and Eilenberg: abelian extensions with a given module structure correspond to $H^2(\mathfrak g,\mathfrak a)$ (CE48).
• 1953–1954 — Mori and Hochschild: for a $\mathfrak g$-kernel $(\mathfrak n,s)$, $s\colon\mathfrak g\to\operatorname{out}(\mathfrak n)$, extensions exist only if a class in $H^3(\mathfrak g,\mathfrak z(\mathfrak n))_s$ vanishes, and then form an affine space over $H^2(\mathfrak g,\mathfrak z(\mathfrak n))_s$ (purely algebraic, over a field).
• 1966 — Shukla: the same over commutative rings in which $2$ is invertible.
• 2004 — Neeb, Non-abelian extensions of topological Lie algebras (arXiv:math/0411256v1): the classification for topologically split extensions of topological Lie algebras over any topological field of characteristic $0$, set up so that it transfers to infinite-dimensional Lie groups.

Setting

Throughout, $\mathbb K$ is a topological field of characteristic $0$ (the discrete topology is allowed), topological vector spaces are Hausdorff, and a topological Lie algebra is a Lie algebra with a vector-space topology for which the bracket is continuous.

A topologically split extension of $\mathfrak g$ by $\mathfrak n$ is a short exact sequence $\mathfrak n\overset{\iota}{\hookrightarrow}\widehat{\mathfrak g}\overset{q}{\twoheadrightarrow}\mathfrak g$ of continuous Lie homomorphisms with a continuous linear section $\sigma$ of $q$ such that $(n,x)\mapsto\iota(n)+\sigma(x)$ is a homeomorphism $\mathfrak n\times\mathfrak g\to\widehat{\mathfrak g}$. Two extensions are equivalent if a continuous Lie homomorphism between the middle terms is the identity on $\mathfrak n$ and commutes with the projections to $\mathfrak g$. $\mathrm{Ext}(\mathfrak g,\mathfrak n)$ denotes the set of equivalence classes.

Continuous $p$-cochains $C^p(\mathfrak g,V)$ are continuous alternating $p$-linear maps $\mathfrak g^p\to V$; $C^1(\mathfrak g,\mathfrak n)$ is the space of continuous linear maps. For a linear map $S\colon\mathfrak g\to\operatorname{der}\mathfrak n$ with $(x,m)\mapsto S(x).m$ continuous, the curvature is $R_S(x,y)=[S(x),S(y)]-S([x,y])$ and the covariant differential $d_S$ is the Chevalley–Eilenberg formula with $S$ in place of a module action.

A pair $(S,\omega)$ with $\omega\in C^2(\mathfrak g,\mathfrak n)$ is a continuous factor system if $R_S=\operatorname{ad}\circ\omega$ and $d_S\omega=0$; the set of these is $Z^2(\mathfrak g,\mathfrak n)$. Each one defines the twisted product $\mathfrak n\times_{(S,\omega)}\mathfrak g$, the space $\mathfrak n\times\mathfrak g$ with the bracket

$$[(n,x),(n',x')]=\big([n,n']+S(x).n'-S(x').n+\omega(x,x'),\ [x,x']\big).$$

The group $C^1(\mathfrak g,\mathfrak n)$ acts on factor systems by the gauge action $\gamma.(S,\omega)=(S+\operatorname{ad}\circ\gamma,\ \omega+d_S\gamma+\tfrac12[\gamma,\gamma])$, where $\tfrac12[\gamma,\gamma](x,y)=[\gamma(x),\gamma(y)]$. An $S$ admitting some $\omega$ with $R_S=\operatorname{ad}\circ\omega$ is a continuous outer action; $S\sim S'$ if $S=S'+\operatorname{ad}\circ\gamma$, and the class $[S]$ is a continuous $\mathfrak g$-kernel. $\mathrm{Ext}(\mathfrak g,\mathfrak n)_{[S]}$ collects the extensions whose outer action $x\mapsto\operatorname{ad}(\sigma(x))|_{\mathfrak n}$ lies in $[S]$. Finally $S$ makes the centre $\mathfrak z(\mathfrak n)$ a $\mathfrak g$-module by $x.z=S(x).z$, with cocycles $Z^2(\mathfrak g,\mathfrak z(\mathfrak n))_S$, coboundaries $B^2(\mathfrak g,\mathfrak z(\mathfrak n))_S=d_S C^1(\mathfrak g,\mathfrak z(\mathfrak n))$ and cohomology $H^2(\mathfrak g,\mathfrak z(\mathfrak n))_S$; and $Z^2(\mathfrak g,\mathfrak n)_S=\{\omega\in C^2(\mathfrak g,\mathfrak n): R_S=\operatorname{ad}\circ\omega,\ d_S\omega=0\}$.

Formalization targets

Goal: Theorem II.7 (p. 13)

$$\overline\Gamma\colon Z^2(\mathfrak g,\mathfrak n)/C^1(\mathfrak g,\mathfrak n)\xrightarrow{\ \sim\ }\mathrm{Ext}(\mathfrak g,\mathfrak n),\qquad [(S,\omega)]\mapsto[\mathfrak n\times_{(S,\omega)}\mathfrak g],$$

and for every continuous outer action $S$ the map $Z^2(\mathfrak g,\mathfrak n)_S\to\mathrm{Ext}(\mathfrak g,\mathfrak n)_{[S]}$, $\omega\mapsto[\mathfrak n\times_{(S,\omega)}\mathfrak g]$, is onto with fibres the cosets of $B^2(\mathfrak g,\mathfrak z(\mathfrak n))_S$ in the affine space $Z^2(\mathfrak g,\mathfrak n)_S$ over $Z^2(\mathfrak g,\mathfrak z(\mathfrak n))_S$. Hence

$$\mathrm{Ext}(\mathfrak g,\mathfrak n)_{[S]}\ \text{is an affine space with translation group}\ H^2(\mathfrak g,\mathfrak z(\mathfrak n))_S .$$

The Lean goal states this without quotient types: $Z^2(\mathfrak g,\mathfrak n)$ is gauge invariant, every extension is equivalent to a twisted product, and two twisted products are equivalent exactly when their factor systems lie in one $C^1(\mathfrak g,\mathfrak n)$-orbit; for fixed $S$, surjectivity, the coset description of the fibres, the affine structure of $Z^2(\mathfrak g,\mathfrak n)_S$, and the simply transitive action of $H^2$ through a base point (Corollary II.8).

Milestones

1. Lemma I.9 (p. 8): the gauge action is an action; $R_{S+\operatorname{ad}\circ\gamma}=R_S+\operatorname{ad}\circ(d_S\gamma+\tfrac12[\gamma,\gamma])$; $\{R_S=\operatorname{ad}\circ\omega\}$ is invariant; $d_S\omega\in Z^3(\mathfrak g,\mathfrak z(\mathfrak n))_S$ and is constant on orbits.
2. Lemma II.4 (p. 11): for a continuous factor system, $\mathfrak n\times_{(S,\omega)}\mathfrak g$ is a topological Lie algebra and a split extension; conversely every split extension is equivalent to one.
3. Lemma II.5 (p. 12): $(n,x)\mapsto(\alpha(n)+\gamma(\beta(x)),\beta(x))$ is an isomorphism $\mathfrak n\times_{(S,\omega)}\mathfrak g\to\mathfrak n\times_{(S',\omega')}\mathfrak g$ iff $(\alpha,\beta).(S,\omega)=\gamma.(S',\omega')$.

Significance

The theorem reduces the classification of non-abelian extensions to two problems: which continuous $\mathfrak g$-kernels $[S]$ occur, and, for each, the cohomology $H^2(\mathfrak g,\mathfrak z(\mathfrak n))_S$ of $\mathfrak g$ with coefficients in the centre of $\mathfrak n$. The first problem is answered in the same paper by the obstruction class $\chi(S)=[d_S\omega]\in H^3(\mathfrak g,\mathfrak z(\mathfrak n))_S$ (Theorem IV.4), whose definition rests on Lemma I.9. For an abelian kernel the result recovers the classical bijection $H^2(\mathfrak g,\mathfrak a)_S\cong\mathrm{Ext}(\mathfrak g,\mathfrak a)_S$; for centreless $\mathfrak n$ it shows that an extension is determined by its outer action. The topological version is the infinitesimal input for integrating extensions of infinite-dimensional Lie groups.

The algebraic case (discrete topologies) is classical; the topological statement is the paper's. Neither is machine-checked: Mathlib has Lie algebra extensions and low-degree Chevalley–Eilenberg cochains for genuine modules, but no outer actions, no factor systems for non-abelian kernels and no topological Lie algebras. The mission produces these objects together with a checked proof of the classification; the algebraic Mori–Hochschild theorem is the special case of discrete topologies.

Difficulty

The obvious approach transfers the abelian proof. It fails because $S$ is not a representation: $d_S^2\neq0$ in general, so the cochains do not form a complex, and the gauge action is affine with the quadratic term $\tfrac12[\gamma,\gamma]$. The needed identities — the curvature formula, invariance of $d_S\omega$, and $d_S\omega$ taking central values — hold only under $R_S=\operatorname{ad}\circ\omega$ and require careful bookkeeping of signs and of the factor $\tfrac12$. A second difficulty is topological: every map produced (the factor system of an extension, the equivalences, the cochain $\gamma$ extracted from an equivalence) must be shown continuous, which is where the splitting hypothesis enters, since $\widehat{\mathfrak g}/\mathfrak n$ need not be topologically isomorphic to $\mathfrak g$ without it.

Formalization scope

All objects live in the namespace NeebLieExt. $\mathbb K$ carries [Field K] [TopologicalSpace K] [IsTopologicalDivisionRing K] [CharZero K]; $\mathfrak n$, $\mathfrak g$ and extension middle terms $E$ are Lie algebras with [IsTopologicalAddGroup] [ContinuousSMul K], the class IsTopLieAlgebra (continuous bracket), and [T2Space] for $\mathfrak n$, $\mathfrak g$; $E$ ranges over an arbitrary universe. Cochains are plain functions with predicates IsCochain2, IsCochain3 (multilinear, alternating, jointly continuous); $S$ is a linear map into Mathlib's LieDerivation K n n with jointly continuous evaluation; $d_S$ is written out in degrees 1–3 (dS1, dS2, dS3). The twisted bracket is the function twistedBracket S ω on n × g — Mathlib's bracket on n × g is the direct product and is never used for twisted products. $\mathrm{Ext}(\mathfrak g,\mathfrak n)$ and $H^2$ are not quotient types: the goal states surjectivity and the exact description of the fibres. The paper's hypothesis $\mathrm{Ext}(\mathfrak g,\mathfrak n)_{[S]}\neq\emptyset$ is dropped, since every clause holds without it. Lemma II.5 prints the map as $(\alpha(n)+\gamma(\beta(x)),\beta(n))$; the formalization uses $\beta(x)$, as the proof does.

A trivializing reading is excluded: equivalences must fix $\mathfrak n$ and the $\mathfrak g$-coordinate, and $B^2$ uses $\mathfrak z(\mathfrak n)$-valued $\alpha$; without either, the fibre statements would be false.

Contributions are welcome on the gauge-action identities (Lemma I.9), the construction of the factor system of a split extension (Lemma II.4), and the isomorphism criterion (Lemma II.5); a reusable library of continuous cochains, outer actions and twisted products would serve the obstruction theory of §IV and the Lie group version.

Selected references

• K.-H. Neeb, Non-abelian extensions of topological Lie algebras, preprint arXiv:math/0411256v1, 2004. https://arxiv.org/abs/math/0411256
• C. Chevalley, S. Eilenberg, Cohomology theory of Lie groups and Lie algebras, Trans. Amer. Math. Soc. 63, 1948. https://doi.org/10.1090/S0002-9947-1948-0024908-8
• D. Alekseevsky, P. W. Michor, W. Ruppert, Extensions of Lie algebras, preprint, 2000 (partly contains Lemma I.9). https://arxiv.org/abs/math/0005042
• G. Hochschild, Lie algebra kernels and cohomology, Amer. J. Math. 76, 1954; M. Mori, On the three-dimensional cohomology groups of Lie algebras, J. Math. Soc. Japan 5, 1953 — cited after Neeb's bibliography, p. 36 of https://arxiv.org/abs/math/0411256

Motivation

A decoherence-free subspace (DFS) is a subspace of a quantum register on which a given noise process acts trivially, so that information stored there is protected without active error correction. Weak collective decoherence is the simplest noise with such subspaces: every qubit couples to the environment through the same operator, which after a fixed single-qubit rotation is the collective operator $S_z^{[n]}$ (Zanardi and Rasetti 1997; Lidar, Chuang and Whaley 1998). It models closely spaced qubits subject to a common fluctuating field, for instance ions in a trap.

Storage alone is not computation. To use a DFS, one needs Hamiltonians that never leave it and that enact every unitary on it. Chapter 9 and Appendix B of Bacon's thesis (arXiv:quant-ph/0305025v1), following Kempe, Bacon, DiVincenzo and Whaley (arXiv:quant-ph/0004064; arXiv:quant-ph/0112013), show that a short list of nearest-neighbour two-qubit Hamiltonians suffices, and that it acts on each DFS separately.

Setting

Take $n$ qubits with computational basis $|x\rangle$, $x\in\{0,1\}^n$. The collective operator is diagonal, $S_z^{[n]}|x\rangle=\tfrac12\big(n-2H(x)\big)|x\rangle$, where $H(x)$ is the Hamming weight (the number of ones) of $x$. Its eigenspaces are the decoherence-free subspaces

$$\mathrm{DFS}_n(h)=\operatorname{span}\{|x\rangle : H(x)=h\},\qquad 0\le h\le n,\qquad \dim \mathrm{DFS}_n(h)=\binom nh ,$$

with orthogonal projectors $P_h$. Appendix B labels the same subspaces by $K=n-2h$.

The two-qubit Hamiltonians that commute with $S_z^{[n]}$ are exactly the matrices

$$T(z_1,z_2,z_3,z_4,h)=\begin{pmatrix} z_1&0&0&0\\ 0&z_2&h&0\\ 0&\bar h&z_3&0\\ 0&0&0&z_4\end{pmatrix}$$

in the basis $|00\rangle,|01\rangle,|10\rangle,|11\rangle$. From them the thesis picks the exchange interaction $E$ (the swap of two qubits) and the diagonal operators $T^P=\mathrm{diag}(1,0,0,0)$, $T^Q=\mathrm{diag}(0,0,0,1)$, $\bar Z=\mathrm{diag}(0,0,1,0)$, and forms the nearest-neighbour set

$$\mathsf H=\{E_{i,i+1},\,T^P_{i,i+1},\,T^Q_{i,i+1},\,\bar Z_{i,i+1} : i=1,\dots,n-1\}.$$

The Lie algebra generated by $\mathsf H$ is the closure of $\mathsf H$ under real scalar multiplication, addition and the commutator $i[A,B]$. In the Lean development it is written $L=\operatorname{Lie}_{\mathbb R}\{iG: G\in\mathsf H\}$, with bracket $AB-BA$; a Hamiltonian $X$ is generated exactly when $iX\in L$.

Formalization targets

Goal: Theorem B.0.1 (Theorem 9.2.1, containment form)

For every $n\ge2$, every $0\le h\le n$ and every $n$-qubit matrix $X$,

$$X^\dagger=-X,\qquad P_hXP_h=X,\qquad \operatorname{tr}X=0\quad\Longrightarrow\quad X\in L .$$

So $L$ contains $\mathfrak{su}\big(\binom nh\big)$ acting on $\mathrm{DFS}_n(h)$ and annihilating every other DFS ("independence"). Theorem 9.2.1 also displays the equality $L=\bigoplus_h\mathfrak{su}\big(\binom nh\big)$. That equality is false: for $n=2$, $iT^P_{12}=i|00\rangle\langle00|$ lies in $L$ and acts nontrivially on the one-dimensional $\mathrm{DFS}_2(0)$, where $\mathfrak{su}(1)=0$. The goal is the containment, which both theorems state in words and Appendix B proves.

Milestones

1. Eqs. (9.3)–(9.4). A Hermitian two-qubit operator placed on qubits $k\neq l$ commutes with $S_z^{[n]}$ if and only if it equals $T(z_1,z_2,z_3,z_4,h)$ for some real $z_i$ and complex $h$.
2. Eqs. (B.3)–(B.4). For $n=2$: $\bar Y=i[\bar Z_{12},E_{12}]$ is the explicit matrix (B.3). $\bar Y$, $\bar Z=i[E_{12},\bar Y]$ and $\bar X=i[\bar Y,\bar Z]$ are generated by $\mathsf H$ and supported on $\operatorname{span}\{|01\rangle,|10\rangle\}$, and their real span contains every traceless Hermitian operator supported there. This is the base case of the goal.

Significance

Exponentiating $L$ gives every special unitary on each $\mathrm{DFS}_n(h)$ separately, with the identity on all other DFSs. Encoded universal computation on weak collective DFSs therefore needs only nearest-neighbour interactions that never leave the protected subspaces. Chapter 10 applies this to ion traps. The same inductive scheme, with Lemmas from Appendix D, handles strong collective decoherence and the exchange interaction alone (Theorem C.2.1, the companion mission IX of this series).

The result is published and proved on paper. This mission formalizes it; no machine-checked proof of it is known. The work also corrects the overstated equality (9.11), and the base case and commutant characterization are self-contained finite computations.

Difficulty

The generators do not act independently on the DFSs. Every element of $L$ acts simultaneously on all the DFSs it preserves, and the obvious inductive step falls short. Lifting $\mathfrak{su}$ from $n-1$ to $n$ qubits gives operators that act at once on the daughter subspaces of $\mathrm{DFS}_{n+1}(h)$ and $\mathrm{DFS}_{n+1}(h+1)$. These are the paths through the lattice of partial weights in Appendix B. The proof must first separate these simultaneous actions (the "independence step"), and then glue $\mathfrak{su}$ on two overlapping subspaces into $\mathfrak{su}$ on their span. That needs a quantitative supply of elements of $L$, not just closure arguments, and it must work for every $n$ and every weight $h$, including the one-dimensional DFSs at $h=0$ and $h=n$.

Formalization scope

Lean represents the register by the index type Fin n → Fin 2, and operators by Matrix (Fin n → Fin 2) (Fin n → Fin 2) ℂ. Qubits are numbered $0,\dots,n-1$; the book numbers them $1,\dots,n$. Two-qubit matrices are indexed by Fin 2 × Fin 2 with the first qubit first, and they are placed on qubits $k,l$ by tensoring with the identity elsewhere. $L$ is LieSubalgebra.lieSpan ℝ of $\{iG\}$, with the matrix commutator (LieRing.ofAssociativeRing, a local instance). It allows real scalars only and has no $iI$ generator, and $\mathsf H$ is exactly the nearest-neighbour set (9.10). Adding all pairs or single-qubit $\sigma_z$ terms would weaken the theorem. The support hypothesis $P_hXP_h=X$ is what makes the statement about one DFS at a time, so dropping it, or replacing the containment by the false equality, changes the theorem.

A complete development needs the following: the commutant computation (milestone 1), the two-qubit base case (milestone 2), the independence step, and a lemma that combines $\mathfrak{su}$ on two non-orthogonal subspaces. The last of these is the Enlarging and Mixing Lemmas of Appendix D, posed in mission IX. The block-matrix and Lie-span infrastructure is reusable for other symmetry-restricted universality results. Contributions to any of these are welcome.

Selected references

• D. Bacon, Decoherence, Control, and Symmetry in Quantum Computers, PhD thesis, UC Berkeley, 2001. arXiv:quant-ph/0305025v1
• J. Kempe, D. Bacon, D. A. Lidar, K. B. Whaley, Theory of decoherence-free fault-tolerant universal quantum computation, Phys. Rev. A 63, 042307 (2001). arXiv:quant-ph/0004064
• J. Kempe, D. Bacon, D. P. DiVincenzo, K. B. Whaley, Encoded universality from a single physical interaction, Quantum Inf. Comput. 1, 33 (2001). arXiv:quant-ph/0112013
• P. Zanardi, M. Rasetti, Noiseless quantum codes, Phys. Rev. Lett. 79, 3306 (1997). doi:10.1103/PhysRevLett.79.3306
• D. A. Lidar, I. L. Chuang, K. B. Whaley, Decoherence-free subspaces for quantum computation, Phys. Rev. Lett. 81, 2594 (1998). arXiv:quant-ph/9807004