All missions

Symmetry as a design principle

Geometric deep learning is the programme, set out by Bronstein, Bruna, Cohen and Veličković in Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges (arXiv:2104.13478v2, 2021), of deriving neural network architectures from the symmetries of the domain on which the data live. Convolutional networks on images, permutation-invariant networks on sets, graph neural networks and equivariant networks for molecules are presented there as instances of one template. Chapter 3 of the book, Geometric Priors, gives that template: it fixes what a symmetry of a signal is, what it means for a function to respect it, and how invariant functions are assembled from simpler blocks. This mission formalizes the definitions and the elementary claims of Chapter 3. Its goal is the observation the book uses to explain why such networks must be non-linear.

The book numbers no theorem, lemma or definition. Its only labels are the sections, the equations (1)–(53) and the figures. Every item of this mission is therefore cited by section, equation number (where there is one) and printed page of the arXiv v2 text; a margin note is cited as "side-note, p. n".

Setting

A domain is a set $\Omega$. A signal on $\Omega$ with values in a set of channels $C$ is a function $x : \Omega \to C$; the signals form the space $X(\Omega, C)$ (equation (1)), written $X(\Omega)$ when $C = \mathbb R$.

A group $\mathfrak G$ acts on $\Omega$ through a map $(\mathfrak g, u) \mapsto \mathfrak g . u$ with $\mathfrak g . (\mathfrak h . u) = (\mathfrak g \mathfrak h) . u$. It then acts on signals by equation (3):

$$(\mathfrak g . x)(u) = x(\mathfrak g^{-1} u).$$

On real signals this action is linear, so $\rho(\mathfrak g) x = \mathfrak g . x$ defines a representation $\rho$ of $\mathfrak G$ on $X(\Omega)$.

A function $f : X(\Omega, C) \to Y$ is $\mathfrak G$-invariant if $f(\mathfrak g . x) = f(x)$ for all $\mathfrak g$ and $x$. A map $B : X(\Omega, C) \to X(\Omega', C')$ between signal spaces on which $\mathfrak G$ acts is $\mathfrak G$-equivariant if $B(\mathfrak g . x) = \mathfrak g . B(x)$. A map $\sigma : C \to C'$ acts on signals element-wise, $(\boldsymbol\sigma(x))(u) = \sigma(x(u))$.

For a measure $\mu$ on $\mathfrak G$ with $0 < \mu(\mathfrak G) < \infty$, the $\mathfrak G$-average of a real signal is

$$A x = \frac{1}{\mu(\mathfrak G)} \int_{\mathfrak G} (\mathfrak g . x)\, \mathrm d\mu(\mathfrak g).$$

The book takes $\mu$ to be the Haar measure of the group.

The metric distortion of a map $\eta$ between metric spaces is $\operatorname{dis}(\eta) = \sup_{u,v} |d(\eta(u), \eta(v)) - d(u, v)|$ (§4.4, p. 51). A self-map $\tau$ with distortion at most $\varepsilon$ is an $\varepsilon$-isometry.

The Geometric Deep Learning Blueprint (§3.5, p. 29) builds functions

$$f = A \circ \boldsymbol\sigma_J \circ B_J \circ P_{J-1} \circ \cdots \circ P_1 \circ \boldsymbol\sigma_1 \circ B_1$$

from equivariant linear layers $B_j$, element-wise nonlinearities $\boldsymbol\sigma_j$, poolings $P_j$ onto coarser domains, and an invariant global pooling $A$.

Formalization targets

Goal: linear invariants see only the average (§3.5, p. 27)

For a finite domain $\Omega$, a finite nonzero measure $\mu$ on $\mathfrak G$, and a linear $\mathfrak G$-invariant map $f$ from $X(\Omega)$ into a real Banach space, for every signal $x$,

$$f(x) = \frac{1}{\mu(\mathfrak G)} \int_{\mathfrak G} f(\mathfrak g . x)\, \mathrm d\mu(\mathfrak g) = f\!\left( \frac{1}{\mu(\mathfrak G)} \int_{\mathfrak G} (\mathfrak g . x)\, \mathrm d\mu(\mathfrak g) \right) = f(Ax).$$

A linear invariant therefore depends on $x$ only through $Ax$.

Milestones, in attack order

1. The action (3) is a group action: $\mathfrak g . (\mathfrak h . x) = (\mathfrak g\mathfrak h) . x$ (p. 14).
2. It is linear: $\mathfrak g . (\alpha x + \beta x') = \alpha(\mathfrak g . x) + \beta(\mathfrak g . x')$ (p. 15).
3. It is a representation: $\rho(\mathfrak g)(\rho(\mathfrak h)x) = \rho(\mathfrak g\mathfrak h)x$ (p. 15).
4. Two $\varepsilon$-isometries compose to a $2\varepsilon$-isometry, and $\varepsilon$-isometries are not closed under composition (side-note, p. 20).
5. $U = \boldsymbol\sigma \circ B$ is equivariant for equivariant $B$ and any element-wise $\sigma$ (p. 27).
6. The $\mathfrak G$-average is invariant, so $A \circ U$ is invariant (p. 27).
7. The blueprint $f$ is $\mathfrak G$-invariant (p. 29).

Companion: the Fourier modulus (§3.4, p. 25)

With $\hat x(\xi) = \int x(u) e^{-\mathrm i\xi u}\,\mathrm du$ and $(S_v x)(u) = x(u - v)$, $\widehat{S_v x}(\xi) = e^{-\mathrm i \xi v}\hat x(\xi)$, so $|\widehat{S_v x}| = |\hat x|$.

Significance

The goal is the book's reason for non-linearity. Linear invariant models collapse to functions of the group average, so they cannot tell apart two images with the same mean colour. Expressive invariant models must interleave equivariant linear layers with non-linear maps. Milestones 5–7 are the positive half of the same argument: element-wise nonlinearities keep equivariance, the average turns equivariance into invariance, and stacking such blocks gives the blueprint that the later chapters instantiate on grids, groups, graphs and manifolds. Milestone 4 is the book's reason for leaving exact symmetry behind: small deformations do not form a group, so it replaces invariance to deformations by stability to them.

Each claim of the chapter is proved in one or two lines on the page, and none is new mathematics. What a formalization adds is the precise setting in which they hold. The book names the Haar measure but its identity needs no invariance of $\mu$; the average's invariance needs right invariance, which the page does not state; and the printed blueprint is invariant only if the poolings are equivariant. As far as a search of the platform and Mathlib shows, none of these statements has a machine-checked proof. The definitions here (the action on signals, invariance, equivariance, the average, the blueprint) are reusable by every later mission of this series.

Difficulty

The obvious argument for the goal pulls $f$ through the integral, which uses linearity in the form "a continuous linear map commutes with the Bochner integral". That needs continuity of $f$ and integrability of $\mathfrak g \mapsto \mathfrak g . x$, and neither is stated on the page. On a finite domain both follow from the setting, finite dimension for continuity and boundedness with measurability for integrability. The measurability of $\mathfrak g \mapsto \mathfrak g^{-1} . u$ has to be assumed of the group and the action.

For the average's invariance, the substitution $\mathfrak g \mapsto \mathfrak g\mathfrak h$ is valid only for a right-invariant measure. For the blueprint, the composite's invariance fails for a non-equivariant pooling, so the box's claim is false as printed. For the $\varepsilon$-isometries, the subtle half is the negative one: exhibiting a deformation that is an $\varepsilon$-isometry while its square is not.

Formalization scope

• Signals are functions Ω → C. The goal and the average use real signals on a finite domain ([Fintype Ω]), following the book's side-note on p. 15 that one must always discretise to a finite grid in practice; the other milestones allow any domain and any channel types.
• The action (3) is a function act g x := fun u => x (g⁻¹ • u) for [MulAction G Ω], not a MulAction instance on Ω → C.
• The measure is any μ with [IsFiniteMeasure μ] and μ ≠ 0. Without those hypotheses Lean's (μ univ).toReal⁻¹ would be $0$ and the goal false. The goal assumes no invariance of μ. Milestone 6 adds [μ.IsMulRightInvariant], which the Haar measure of a compact group satisfies.
• Measurability: [MeasurableInv G], [MeasurableSMul G Ω] and the discrete σ-algebra on Ω; integrability of g ↦ g.x is a consequence, not a hypothesis. A finite group with the counting measure and a compact group with its Haar measure both fit.
• The blueprint is indexed from $0$ to $n = J - 1$. A single group acts on all domains, and the poolings are assumed equivariant (a correction of the printed box, disclosed in the statement). The box's remark that different blocks may use different groups is not formalized.
• $\varepsilon$-isometries are defined pointwise ($|d(\tau u, \tau v) - d(u,v)| \le \varepsilon$ for all $u, v$), avoiding a real supremum that would be $0$ on an unbounded set. Non-closure is witnessed on $\mathbb R$ by a continuous bijection.
• The Fourier transform of the companion is the book's $\int x(u)e^{-\mathrm i\xi u}\,\mathrm du$ (no $2\pi$), a Bochner integral over $\mathbb R$.

The goal cannot be satisfied trivially. groupAverage is defined from μ and the action alone, the goal quantifies over every linear invariant f, and the measure hypotheses exclude the degenerate case in which the average is $0$. Proofs, finite-sum encodings of the average, and versions for complex or vector-valued channels are welcome.

Selected references

• M. M. Bronstein, J. Bruna, T. Cohen, P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021. https://arxiv.org/abs/2104.13478v2
• S. Mallat, Group Invariant Scattering, Communications on Pure and Applied Mathematics 65(10), 2012. https://doi.org/10.1002/cpa.21413

Motivation

Many learning problems take an unordered collection as input: the points of a point cloud, the particles of a physical system, the atoms of a molecule, the nodes of a graph. Storing such data in memory fixes an order of the elements, but the order carries no information, and a model whose output changes when the rows of its input are shuffled is answering a different question from the one posed. Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges (arXiv:2104.13478v2, 2021), §4.1, make this the first instance of their blueprint: the domain is a set (or a graph) of $n$ nodes, and the symmetry group is the symmetric group $\Sigma_n$ of all reorderings.

Two architectures used in practice follow this pattern. Deep Sets (Zaheer et al., NeurIPS 2017) and PointNets (Qi et al., CVPR 2017) process sets; message-passing graph neural networks process graphs. The design question in both cases is which layers respect the symmetry. For linear layers the question has a complete answer, and the answer determines the layer used by Deep Sets. For graphs, Maron, Ben-Hamu, Shamir and Lipman (2018) counted the linear layers acting on adjacency matrices.

Setting

A set of $n$ nodes $\mathcal V=\{1,\dots,n\}$ carries node features $\mathbf x_u\in\mathbb R^d$, stacked as the rows of a matrix $\mathbf X\in\mathbb R^{n\times d}$. A graph adds an adjacency matrix $\mathbf A\in\mathbb R^{n\times n}$, eq. (8), whose nonzero entries are the edges.

A permutation $\sigma\in\Sigma_n$ acts through its permutation matrix $\mathbf P$ by reordering rows: row $u$ of $\mathbf P\mathbf X$ is row $\sigma^{-1}(u)$ of $\mathbf X$. On adjacency matrices it acts by $\mathbf A\mapsto\mathbf P\mathbf A\mathbf P^\top$, reordering rows and columns together.

A function $f$ is permutation invariant if $f(\mathbf P\mathbf X)=f(\mathbf X)$ for every permutation matrix $\mathbf P$, and a matrix-valued function $\mathbf F$ is permutation equivariant if $\mathbf F(\mathbf P\mathbf X)=\mathbf P\mathbf F(\mathbf X)$. On graphs the book's definitions (9) and (10) are

$$f(\mathbf P\mathbf X,\mathbf P\mathbf A\mathbf P^\top)=f(\mathbf X,\mathbf A)\quad(9),\qquad \mathbf F(\mathbf P\mathbf X,\mathbf P\mathbf A\mathbf P^\top)=\mathbf P\mathbf F(\mathbf X,\mathbf A)\quad(10),$$

for any permutation matrix $\mathbf P$.

The section's constructions are the sum readout $f(\mathbf X)=\phi\big(\sum_{u\in\mathcal V}\psi(\mathbf x_u)\big)$ (6); the shared node-wise linear map $\mathbf F_{\boldsymbol\Theta}(\mathbf X)=\mathbf X\boldsymbol\Theta$ (7); the neighbourhood $\mathcal N_u=\{v:(u,v)\in\mathcal E\text{ or }(v,u)\in\mathcal E\}$ (11) and the multiset of neighbourhood features $\mathbf X_{\mathcal N_u}=\{\!\{\mathbf x_v:v\in\mathcal N_u\}\!\}$ (12); and the local layer whose $u$-th row is $\phi(\mathbf x_u,\mathbf X_{\mathcal N_u})$ (13). For one feature channel the two linear generators are the identity $\mathbf F_1x=x$ and the average $\mathbf F_2x=\tfrac1n\mathbf 1\mathbf 1^\top x$, every entry of which is the mean $\tfrac1n\sum_u x_u$.

The book numbers no theorems, lemmas or definitions; every item of this mission is cited by section, equation number and printed page.

Formalization targets

Goal: linear equivariant maps on one channel

For $n\ge1$ and a linear map $\mathbf F:\mathbb R^n\to\mathbb R^n$,

$$\big(\forall\,\mathbf P,\ \forall x:\ \mathbf F\mathbf P x=\mathbf P\mathbf F x\big)\iff \exists\,\alpha,\beta\in\mathbb R\ \ \forall x:\ \mathbf F x=\alpha\,x+\beta\,\tfrac1n\mathbf 1\mathbf 1^\top x .$$

This is the book's sentence on p. 33: any linear equivariant "can be written as a linear combination of two generators, the identity … and the average". Both directions are stated; the content is the "only if" direction.

Milestones

1. The sum readout (6) is permutation invariant (p. 32).
2. The node-wise linear map (7) is permutation equivariant, with rows $\mathbf h_u=\boldsymbol\Theta^\top\mathbf x_u$ (p. 33).
3. The local layer (13) satisfies (10) whenever $\phi$ is invariant to the order of the neighbourhood (p. 34).
4. Invariant and equivariant functions give identical outputs on isomorphic graphs (p. 35).
5. On the complete graph $\mathbf A=\mathbf 1\mathbf 1^\top$, the aggregate $\bigoplus_{v\in\mathcal V}\psi(\mathbf x_v)$ is the same at every node (§5.4, p. 81).

Stronger statements

• Several channels (corrected). A linear $\mathbf F:\mathbb R^{n\times d}\to\mathbb R^{n\times d'}$ is permutation equivariant iff $\mathbf F(\mathbf X)=\mathbf X\boldsymbol\Theta_1+\tfrac1n\mathbf 1\mathbf 1^\top\mathbf X\boldsymbol\Theta_2$.
• Adjacency matrices (Maron et al., corrected). For $n\ge4$, the linear maps $L:\mathbb R^{n\times n}\to\mathbb R^{n\times n}$ with $L(\mathbf P\mathbf A\mathbf P^\top)=\mathbf P L(\mathbf A)\mathbf P^\top$ form a space of dimension $15=B_4$.

Significance

The result. The goal classifies the linear layers of a set network. Any equivariant linear layer on scalar node features mixes each node's own value with the mean of all values, and nothing else; with several channels the two scalars become two weight matrices, which is exactly the Deep Sets layer. Read the other way, the theorem says that the commutant of the permutation representation of $\Sigma_n$ on $\mathbb R^n$ is two-dimensional (for $n\ge2$), the algebraic fact behind the decomposition $\mathbb R^n=\mathrm{span}(\mathbf 1)\oplus\mathbf 1^\perp$ into two irreducible pieces. The Maron et al. count does the same for layers acting on adjacency matrices and fixes the size of the parameter space of invariant graph networks. The milestones give the elementary invariance and equivariance facts on which the graph-network chapter rests, including the constant aggregate on a complete graph.

Formalizing it. All results here are classical and proved on paper. None is formalized on Prove2Me, and Mathlib has no statement about the commutant of the permutation representation or about equivariant layers on sets. The mission produces a vocabulary of permutation actions on feature and adjacency matrices, and the invariance and equivariance definitions (9)–(10), that later missions of this series (the WL comparison, the E(3)-equivariant layer) also use. Two of the book's printed claims need correction to be true, and the formal statements record the corrected versions.

Difficulty

The milestones are short reindexing arguments; the work is in choosing encodings that keep them faithful. The goal's "if" direction is a one-line computation. The "only if" direction is where an argument is needed: equivariance under all of $\Sigma_n$ must force the matrix of $\mathbf F$ to have one value on the diagonal and one value off it. Equivariance under a smaller group does not suffice: commuting with the cyclic shift alone gives all circulant matrices, an $n$-dimensional space, so the argument must use permutations beyond the shifts. The channel version adds a tensor-product layer to the same argument. The Maron et al. count is a dimension statement, so it needs both a spanning family and its independence, and the count is sensitive to $n$: for $n<4$ the dimension is strictly smaller than 15, so any argument must use $n\ge4$ somewhere.

Formalization scope

Node features are Matrix (Fin n) (Fin d) ℝ (rows are nodes); a single channel is Fin n → ℝ. A permutation is σ : Equiv.Perm (Fin n), acting by X.submatrix σ.symm id (row $u$ of $\mathbf P\mathbf X$ is row $\sigma^{-1}(u)$) and on adjacency matrices by A.submatrix σ.symm σ.symm; this one convention is used in every statement. Adjacency matrices are real; the edge set is the set of nonzero entries, which for the book's 0/1 matrix (8) is its edge set and also admits weighted graphs. The function $\phi$ of (13) and the aggregator $\bigoplus$ of §5.4 take a Multiset, so their invariance to the order of the neighbours holds by construction. The average $\tfrac1n\mathbf 1\mathbf 1^\top$ is written with $(n:\mathbb R)^{-1}$, and the goal and channel version assume $0<n$. Equivariance quantifies over every permutation of $\Sigma_n$, never a generating subset. The complete-graph item states the identical-aggregate clause of §5.4. The page's later claim of equal expressive power across inputs is false: with $n=2$, $\psi(x)=x$, $\bigoplus=\sum$, and $\phi(x,s)=s$, changing $x_2$ changes $h_1$ while $x_1$ stays fixed, which no node-only map can reproduce.

A trivializing formalization is ruled out: "equivariant" is the commutation property itself, never defined as "of the form $\alpha\mathbf I+\beta\tfrac1n\mathbf 1\mathbf 1^\top$".

Two printed claims are corrected. On p. 33 the two-generator form is stated for matrices $\mathbf X$ with $d$ channels; it is false for $d>1$ (the map $\mathbf X\mapsto\mathbf X\boldsymbol\Theta$ of (7) is a counterexample), so the goal is single-channel and the multi-channel statement uses weight matrices. On p. 34 the fifteen generators are said to be independent of $n$; the dimension is 1, 8 and 14 for $n=1,2,3$, so that item assumes $n\ge4$, and it is stated for adjacency-to-adjacency maps as the side-note on p. 33 specifies.

The development needs Mathlib's Equiv.Perm, Matrix.submatrix, Finset sums and reindexing (Equiv.sum_comp), Multiset.map, and Module.finrank. Proofs of the commutant statements, of the multi-channel version and of the dimension count are welcome; the permutation-action and invariance lemmas proved along the way are reusable by any later development on graph networks.

Selected references

• M. M. Bronstein, J. Bruna, T. Cohen, P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint, 2021. https://arxiv.org/abs/2104.13478v2
• M. Zaheer, S. Kottur, S. Ravanbakhsh, B. Póczos, R. Salakhutdinov, A. Smola, Deep Sets, NeurIPS, 2017. https://arxiv.org/abs/1703.06114
• H. Maron, H. Ben-Hamu, N. Shamir, Y. Lipman, Invariant and Equivariant Graph Networks, ICLR, 2019. https://arxiv.org/abs/1812.09902
• C. R. Qi, H. Su, K. Mo, L. J. Guibas, PointNet: Deep Learning on Point Sets for 3D Classification and Segmentation, CVPR, 2017. https://arxiv.org/abs/1612.00593

Motivation

Convolutional networks use the same filter at many locations. A shift of the input then shifts the output in a predictable way, allowing one set of filter coefficients to serve every location. Bronstein, Bruna, Cohen and Veličković, Geometric Deep Learning, §4.3, pp. 40–43 ask how this idea extends when the transformations form a group and the signal domain need not be the group itself. A grid and its cyclic shifts are one example; a sphere and its rotation group are another. In the latter example, a rotation is an output index even though it is not a point of the sphere. This distinction matters when a second convolutional layer processes the first layer's output.

The chapter places this construction within its general account of geometric deep learning: symmetries specify how inputs transform, and a compatible map should transform its outputs in a corresponding way. Here the concrete question is whether the integral defining group convolution has that compatibility. The source calls this property equivariance and gives it immediately after equation (14). The book numbers equations but no theorems, lemmas, propositions, or definitions, so the items below are cited by section, equation, and printed page.

Setting

Let $G$ be a group acting transitively on a domain $\Omega$; write $g\cdot u$ for the image of $u\in\Omega$. The section makes this homogeneous-domain assumption explicit on p. 43. A signal is a scalar function $x:\Omega\to\mathbb R$, and a filter is another such function $\theta$. The group acts on signals by the inverse action on their arguments:

$$(\rho(g)x)(u)=x(g^{-1}\cdot u).$$

This convention makes $\rho$ a left group representation on functions. Let $\mu$ be a measure on $\Omega$ invariant under the action of every element of $G$. The book states this measure convention beside its pairing formula on p. 41. The pairing and group convolution are

$$\langle x,\theta\rangle_\mu=\int_\Omega x(u)\theta(u)\,d\mu(u),\qquad (x\star\theta)(g)=\langle x,\rho(g)\theta\rangle_\mu =\int_\Omega x(u)\theta(g^{-1}\cdot u)\,d\mu(u).$$

The convolution is indexed by $g\in G$, so it is a signal on $G$, even when $\Omega$ and $G$ are different spaces. Signals $y:G\to\mathbb R$ use the regular action $(\rho_G(h)y)(g)=y(h^{-1}g)$. On the cyclic grid $\mathbb Z_n$, the source uses $u\cdot v=v-u$ for the action of a shift $u$ on an index $v$. These conventions are the ones used throughout this mission. Equation (14) and the surrounding definitions, §4.3, pp. 41–43.

Formalization targets

Group convolution is equivariant

For every $h,g\in G$ and scalar signals $x,\theta$ on $\Omega$, the main target is

$$((\rho(h)x)\star\theta)(g) = (\rho_G(h)(x\star\theta))(g) = (x\star\theta)(h^{-1}g).$$

The theorem keeps the domain action $\rho$ and the output regular action $\rho_G$ distinct. The invariant measure and transitive action are part of the source's setting. §4.3, equation (14) and the following displayed identity, p. 41; homogeneous-domain assumption, p. 43.

Source claims that support the target

The milestone list records three claims from the same section. First, the pairing matches a transformed filter to the inversely transformed signal: $\langle x,\rho(g)\theta\rangle_\mu=\langle\rho(g^{-1})x,\theta\rangle_\mu$. Second, the signal action satisfies $\rho(h^{-1})\rho(g)=\rho(h^{-1}g)$. Third, for $n>0$ on the cyclic grid, the finite-sum instance of group convolution has the form $(x\star\theta)_u=\sum_{v=0}^{n-1}x_v\theta_{v+u\pmod n}$. The source's side-note calls the last expression cross-correlation. §4.3, pp. 41–42.

Significance

The equality specifies what happens to every output coordinate after a group transformation of the input. Its output is a function on $G$, so the statement also fixes which action later layers must use. In the sphere example, the first convolution produces a function on the rotation group rather than a function on the sphere; the book then describes applying a second group convolution on that output. §4.3, pp. 42–43.

The result is proved in the source. The remaining work here is to make the invariant measure, the two actions, and the real integral into separately inspectable Lean definitions and to supply machine-checked proofs of the open theorem statements. The cyclic example checks the sign convention at a concrete boundary: using $v-u$ for the group action yields $v+u$ after applying the inverse shift. Those definitions can also support later formalizations of group-indexed layers. This mission does not assert results for learned networks or approximation power; its target is the mathematical convolution identity displayed in the book.

Difficulty

The two occurrences of $\rho$ in the printed identity act on different function spaces. On the left, $\rho(h)$ transforms a signal on $\Omega$; on the right, the regular action transforms a function on $G$. Treating both as a single action obscures the type and can silently reverse the group multiplication order. The group need not be commutative, so this order matters. The measure must also be invariant: a Dirac measure concentrated at a point that moves under the group generally changes the pairing and breaks the claimed equivariance. In the cyclic example, an inverse shift changes the sign again, which is why the output has $v+u$ rather than $v-u$.

Formalization scope

Lean represents a signal as a function $\Omega\to\mathbb R$, the group action using MulAction, and the measure as a measure on $\Omega$. The action on signals, the pairing, group convolution, and the output regular action are explicit functions. The integral theorems require a transitive action, as the section specifies on p. 43, plus measurable spaces on $G$ and $\Omega$, a measurable group action, and an invariant measure. These are the conditions under which the source's change of variables is meaningful. The cyclic example applies the same group convolution to the counting measure on ZMod n, $n>0$, with the shift group acting by $v\mapsto v-u$. It does not identify a cyclic convolution with a planar convolution or assume the group and domain coincide in the general theorem.

The source describes $\mathcal X(\Omega)$ as a Hilbert space. The Lean theorem states the integral identity for arbitrary real functions; on integrable products the pairing has its ordinary meaning, while Lean assigns zero to a nonintegrable integral. The identity remains valid at those totalized inputs because the same measure-preserving transformation relates the two integrands. No integrability hypothesis is used to reduce the stated range. The zero measure is included, but the theorem is universal over invariant measures, including nonzero counting measure on finite group actions; it cannot be proved by choosing a zero measure or an empty domain. Reusable contributions include properties of the signal action, invariant integration under actions, and finite cyclic examples. The transform-and-convolve equation (32) and the second-layer composition on $G$ are outside this chunk's milestone list.

Selected references

• M. M. Bronstein, J. Bruna, T. Cohen and P. Veličković, Geometric Deep Learning: Grids, Groups, Graphs, Geodesics, and Gauges, arXiv preprint arXiv:2104.13478v2, 2021. arXiv.

Motivation

Retailers increasingly pair products with free in-store experiences: yoga classes at Lululemon, playgrounds at Toys "R" Us, cooking classes at Whole Foods. The experience is free to anyone who travels to the store, so it attracts buyers and free riders (visitors who enjoy the experience without buying) alike. The retailer earns revenue only from product sales, but pays for every visit to the experience. Whether a free experience pays for itself, and whether consumers gain from it, is the question of Mutlu, El-Amine and Sahin (SSRN 4617261; published in Manufacturing & Service Operations Management, 2023, doi:10.1287/msom.2021.0339).

The paper models the joint choice of experience and product with the multivariate logit (MVL) model of Russell and Petersen (2000), which builds a global choice model over baskets from conditional logit choices, via Besag's (1974) characterization of joint distributions from conditionals and the autologistic model of Cox (1972). The monopoly analysis (§3.1) yields two results: Theorem 1 on the optimal price and profit as functions of the experience quality, and Theorem 2, which says that low-quality experiences benefit both the retailer and its customers.

Setting

A monopolist sells a main product at price $p$ and offers a free experience of quality $u^x\ge 0$. A consumer chooses $z^x\in\{0,1\}$ (obtain the experience or not) and $z^m\in\{0,1\}$ (buy the product or not). The parameters are the product's nominal utility $u^m$, the travel cost $t>0$, the product's unit cost $c^m$, a memorable-event utility $s>0$, a synergy sensitivity $\lambda>0$, and a cost sensitivity $\eta>0$.

The baseline utilities are $v^x=u^x-t$ and $v^m=u^m-t-p$. Obtaining both offerings together saves one travel cost and creates a brand synergy $\beta(u^x)=s(1-e^{-\lambda u^x})$, so the interaction term is $\psi=t+\beta(u^x)$. Each basket has utility $\mu_{z^xz^m}=v^xz^x+v^mz^m+\psi z^xz^m$ and probability

$$q_{z^xz^m}=\frac{e^{\mu_{z^xz^m}}}{\sum_{j,i\in\{0,1\}}e^{\mu_{ji}}}.$$

The experience costs $c(u^x)=\eta(u^x)^2$ per user, and the retailer's profit is

$$\pi(p)=(q_{01}+q_{11})(p-c^m)-(q_{10}+q_{11})\,c(u^x).$$

Without an experience the model is the binary logit: $\pi^N(p)=q_1(p-c^m)$ with $q_1=e^{v^m}/(e^{v^m}+1)$.

An optimal price $p^*$ maximizes $\pi$ over all real $p$, and $p^{*N}$ maximizes $\pi^N$; $\pi^*(u^x)$ and $\pi^{*N}$ are the optimal profits. Consumer welfare is the logit log-sum $CS=\ln\sum_{j,i}e^{\mu_{ji}}$ with the experience and $CS^N=\ln(1+e^{v^m})$ without it.

Formalization targets

Goal: Theorem 2 (p. 13)

There is a threshold $\hat u^x>0$ such that for every $0\le u^x\le\hat u^x$,

$$\pi(p^*)>\pi^N(p^{*N})\quad\text{and}\quad CS(p^*)>CS^N(p^{*N})$$

for all optimal prices $p^*$, $p^{*N}$, which exist. In addition, some quality $u^x\ge0$ leaves the retailer strictly worse off than offering no experience. The threshold is existential, as in the paper; no particular value is claimed.

Milestones: three clauses of Theorem 1 (p. 12)

1. $p^*>p^{*N}$ for every $u^x\ge 0$ (with existence of the optimal prices and attainment of $\pi^*$, $\pi^{*N}$).
2. $\left.\partial\pi^*/\partial u^x\right|_{u^x=0}>0$.
3. $\lim_{u^x\to\infty}\pi^*=-\infty$ and $\pi^{*N}>0$.

Significance

The result. Theorem 2 identifies a regime in which a free experience is a win-win: the retailer raises its price (Theorem 1) yet sells enough more, through the complementarity between experience and product, to raise profit, and consumers gain despite the higher price. Theorem 1 marks the limits of that regime: experiences of high quality attract so many free riders that profits fall without bound. Together they explain why experiential retail is typically offered at modest quality, and they are the benchmark for the paper's duopoly (§3.2) and conditionally-free (§4) analyses.

Formalizing it. The paper's lemmas and proofs are in an appendix that is not part of the held working paper; the published proof has never been machine-checked. A complete development would give the first verified analysis of optimal pricing under the MVL basket model, including existence of optimal prices, which the paper presupposes when it writes $p^*$. The milestones are the clauses of Theorem 1 that the goal rests on.

Difficulty

The optimal profit $\pi^*$ is a supremum over prices of a ratio of exponential sums, and the experience quality $u^x$ enters through three channels at once: the experience-only basket, the synergy $\beta(u^x)$, and the cost $\eta(u^x)^2$, which is paid also for free riders. The obvious route, solving the first-order condition in closed form, fails: unlike the binary logit, where the optimal markup solves a Lambert-type equation, the MVL first-order condition mixes the free-rider basket into the denominator, and the optimal price need not be monotone in $u^x$ (Figure 1(a)). Comparing welfare requires the optimal prices themselves, not only the optimal profits, and the comparison is between two different optimization problems.

Formalization scope

All quantities are real numbers. Parameters form a structure with fields $u^m,t,c^m,s,\lambda,\eta$; the standing assumptions $t>0$, $\eta>0$, $s>0$, $\lambda>0$ are one predicate carried by every statement. $u^m$ and $c^m$ are unconstrained, and prices range over all of $\mathbb R$. The model uses only $\beta(u^x)=s(1-e^{-\lambda u^x})$ and $c(u^x)=\eta(u^x)^2$, not the constant, piecewise-linear or linear variants the paper mentions.

Conventions committed to:

• $s>0$ and $\lambda>0$ are read from "β(u^x) is positively valued and concave increasing" (p. 10).
• Consumer welfare is the log-sum, never defined in the paper; it reproduces Figure 1(d) ($CS^{*N}=\ln2$ at the Figure 1 parameters). The identification with expected maximum utility under Gumbel shocks, up to an additive constant, is cited, not formalized.
• Optimal prices are global maximizers; their existence is a conclusion of each statement, never a hypothesis, and uniqueness is never assumed, so every comparison holds for all optimal prices.
• "Improves" is strict. The derivative at $u^x=0$ is the right derivative on $[0,\infty)$.
• The second sentence of Theorem 2 is formalized as its retailer half.

A statement at a fixed price, at $u^x=0$ alone, or under an assumed (possibly non-existent) optimum would be trivial or vacuous and is ruled out: the goal quantifies over all optimal prices, asserts their existence, and covers a whole interval $[0,\hat u^x]$.

Not formalized: the remaining clauses of Theorem 1 ("if $p^*$ is decreasing in $u^x$, then $\pi^*$ is also decreasing in $u^x$", which needs $p^*$ as a function, and the comparative statics in $\eta$ and $\lambda$), and Theorems 3–8 (duopoly and conditionally-free offerings).

Needed infrastructure: continuity and coercivity arguments for existence of a maximizer over $\mathbb R$, a parametric envelope argument for $\pi^*$, and logit inequalities. Proofs of the milestones, of the existence of optimal prices, and reusable lemmas on logit pricing are welcome.

Selected references

• N. Mutlu, H. El-Amine, O. Sahin, Offering Memories to Sell Goods? Pricing and Welfare Implications of Experiential Retail, SSRN working paper 4617261, 2023. https://ssrn.com/abstract=4617261 ; published in Manufacturing & Service Operations Management, 2023, https://doi.org/10.1287/msom.2021.0339
• G. J. Russell, A. Petersen, Analysis of cross category dependence in market basket selection, Journal of Retailing 76(3), 2000. https://doi.org/10.1016/S0022-4359(00)00030-0
• J. Besag, Spatial interaction and the statistical analysis of lattice systems, Journal of the Royal Statistical Society B 36(2), 1974. https://doi.org/10.1111/j.2517-6161.1974.tb00999.x
• D. R. Cox, The analysis of multivariate binary data, Journal of the Royal Statistical Society C 21(2), 1972. https://doi.org/10.2307/2346482

Motivation

A pseudoholomorphic map from a planar domain $U\subseteq\mathbb{C}$ into an almost complex manifold solves the nonlinear Cauchy–Riemann equation

$$\bar\partial_Ju=\partial_su+J(u)\,\partial_tu=0,\qquad z=s+it.$$

These maps are the basic objects of Gromov's theory of holomorphic curves, of Floer homology and of symplectic field theory. Two analytic facts about them are used everywhere: solutions of low regularity are automatically smooth, and families with a uniform bound on the first derivative are precompact in $C^\infty_{\mathrm{loc}}$. A third fact, unique continuation, says that a solution is determined near a point by its derivatives there.

This mission formalizes these results locally, for maps from discs into a finite-dimensional real vector space with an almost complex structure defined on an open subset, following C. Wendl, Lectures on Symplectic Field Theory, Lecture 2 (§ 2.4–2.5) and Proposition 9.1. Mathlib has no Sobolev spaces of weakly differentiable maps, no almost complex structures and no pseudoholomorphic maps. The definitions build on the $W^{k,p}$ norm of the DbarRegularity mission.

Setting

• Target. $E$ is a finite-dimensional real vector space and $O\subseteq E$ is open. A smooth almost complex structure on $O$ is a $C^\infty$ map $J:O\to\operatorname{End}_{\mathbb{R}}(E)$ with $J(x)^2=-\mathrm{Id}$. Allowing an open subset rather than all of $E$ covers, for example, symplectizations of contact-type hypersurfaces.
• Domain. $U\subseteq\mathbb{C}$ is open, usually the open unit disc $D$; $\partial_su$ and $\partial_tu$ are the derivatives in the directions $1$ and $i$.
• $J$-holomorphic maps. $u$ is $J$-holomorphic on $U$ if it is differentiable there with $\partial_su+J(u)\partial_tu=0$.
• Weak solutions. $u$ is a $W^{1,p}_{\mathrm{loc}}$ solution if it is continuous with values in $O$, has weak partial derivatives that lie with $u$ in $L^p$ of every compact subset of $U$, and satisfies the equation almost everywhere.
• Convergence. $C^\infty_{\mathrm{loc}}$ convergence on an open set means uniform convergence of all derivatives on every compact subset.

Formalization targets

Goal: compactness of pseudoholomorphic discs

Let $J_\nu\to J$ in $C^\infty_{\mathrm{loc}}$ be smooth almost complex structures on $O$ and let $K_0\subseteq O$ be compact. Every sequence of $J_\nu$-holomorphic $C^1$ maps $u_\nu:D\to K_0$ with $\sup_\nu\sup_D\|Du_\nu\|<\infty$ has a subsequence converging in $C^\infty_{\mathrm{loc}}$ on $D$ to a smooth $J$-holomorphic map $D\to K_0$ (Wendl, Proposition 9.1).

Milestones

1. Regularity of weak solutions. For $p>2$, a continuous $W^{1,p}_{\mathrm{loc}}$ solution of $\partial_su+J(u)\partial_tu=0$ on an open $U$ is $C^\infty$ on $U$ (Theorem 2.22 (1)).
2. Uniform interior bounds. For $p>2$, smooth $J_\nu$-holomorphic discs with values in $K_0$ and uniformly bounded $W^{1,p}$ norm have derivatives of every order bounded on compact subsets of $D$, uniformly in $\nu$ (Theorem 2.22 (2a)).
3. Convergence. For $p>2$, if such discs converge in $W^{1,p}$ to a smooth map, they converge to it in $C^\infty_{\mathrm{loc}}$ (Theorem 2.22 (2b)).
4. Weakly holomorphic functions. An $L^1$ function on $D$ with $\partial_su+i\partial_tu=0$ in the sense of distributions agrees almost everywhere with a holomorphic function (Lemma 2.19).
5. Local solutions with prescribed value. For $2<p<\infty$ and $A\in L^p(D,\operatorname{End}_{\mathbb{R}}(\mathbb{C}^n))$, the equation $\partial_su+i\partial_tu+Au=0$ has, on every sufficiently small disc, a continuous $W^{1,p}$ solution with any prescribed value at $0$ (Lemma 2.24).
6. Local holomorphic factorization. A smooth solution of $\partial_sh+\bar J(z)\partial_th+A(z)h=0$, with $\bar J(z)$ a smooth family of complex structures on $E$, is locally of the form $h=\Phi f$, where $\Phi(z):\mathbb{C}^n\to E$ is a continuous family of real-linear bijections with $\Phi(z)\circ i=\bar J(z)\circ\Phi(z)$ and $f$ is holomorphic (Theorem 2.26).
7. Unique continuation. Two smooth $J$-holomorphic discs whose derivatives of all orders agree at $0$ coincide near $0$ (Proposition 2.28).

Significance

The results. Regularity and $C^\infty_{\mathrm{loc}}$ compactness are the local half of Gromov compactness: once a moduli space of holomorphic curves has a uniform $C^1$ bound, it is precompact in the smooth topology. Unique continuation is the local input for the structure theory of holomorphic curves, such as the decomposition of a curve into a simple curve and a branched cover.

Formalizing them. The mission introduces almost complex structures, pseudoholomorphic maps, weak derivatives and $W^{1,p}_{\mathrm{loc}}$ solutions of a nonlinear first-order system, in a form that applies to any finite-dimensional target and to structures defined on an open subset. These are foundations for finite-energy holomorphic curves in symplectizations, the next stage of this series. Milestones 4 and 5 are statements about linear first-order elliptic equations in the plane, and milestone 6 is a normal form for real-linear Cauchy–Riemann equations; all three are of independent use in complex analysis.

Difficulty

The equation is nonlinear in $u$ and the structures $J_\nu$ vary with $\nu$; the statements about sequences are uniform in $\nu$, with all constants chosen before the index. The weak formulation involves maps that are not assumed differentiable, and the conclusion of milestone 1 is classical smoothness of the given continuous map, not of a representative. The almost complex structure is only defined on an open subset of the target, so every statement keeps track of where the maps take their values. In milestone 6 the complex structure on the target varies with the point of the domain.

Formalization scope

• Namespace JHolomorphic. The definition module JHolomorphic_Setting defines IsAlmostComplexOn, dbarJ, IsJHolomorphicOn, HasWeakPartialsOn, IsWeakJHolomorphicOn and TendstoCInftyLocOn. It imports the DbarRegularity setting for sobolevNorm (the $W^{k,p}(U)$ norm $\sum_{j\le k}\|D^j\varphi\|_{L^p(U)}$).
• Spaces. $E$ is a real normed space with [FiniteDimensional ℝ E], without an inner product. $\mathbb{C}^n$ is EuclideanSpace ℂ (Fin n). Almost complex structures have type E → E →L[ℝ] E.
• Exponents. $p$ is a real number with $p>2$, used as ENNReal.ofReal p.
• Smoothness. Smoothness is ContDiffOn ℝ ∞ ($C^\infty$, not analytic); derivatives of order $m$ are iteratedFDeriv ℝ m.
• Generality. Wendl states the nonlinear results for $E=\mathbb{C}^n$ with the normalization $J(0)=i$, $u(0)=0$; the statements here drop the normalization, allow an open domain of definition $O$ for $J$, and require images in a fixed compact subset of $O$ in the statements about sequences.

Contributions welcome: general lemmas on weak derivatives and on $L^p$ spaces over planar domains.

Selected references

• C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, Lecture 2 and Lecture 9. https://arxiv.org/abs/1612.01009
• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52 (2012), Chapter 2 and Appendix B.
• C. Abbas, H. Hofer, Holomorphic Curves and Global Questions in Contact Geometry, Birkhäuser (2019).

Motivation

We consider group-covariant positive operator valued measures (POVMs) on a finite dimensional quantum system. Following Neumark's theorem a POVM can be implemented by an orthogonal measurement on a larger system. Accordingly, our goal is to find an implementation of a given group-covariant POVM by a quantum circuit using its symmetry. Based on representation theory of the symmetry group we develop a general approach for the implementation of group-covariant POVMs which consist of rank-one operators. The construction relies on a method to decompose matrices that intertwine two representations of a finite group. We give several examples for which the resulting quantum circuits are efficient. In particular, we obtain efficient quantum circuits for a class of POVMs generated by Weyl-Heisenberg groups. These circuits allow to implement an approximative simultaneous measurement of the position and crystal momentum of a particle moving on a cyclic chain.

This mission is the statement-level formalization of Implementation of group-covariant POVMs by orthogonal measurements (arXiv:quant-ph/0407054v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symmetry-preserving orthogonal dilation (Paper main result: symmetry-preserving orthogonal dilation, PDF p. 2). 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.

Selected references

• Implementation of group-covariant POVMs by orthogonal measurements, arXiv:quant-ph/0407054v1, https://arxiv.org/abs/quant-ph/0407054v1

Motivation

Within the abstract framework of dynamical system theory we describe a general approach to the Transient (or Evans-Searles) and Steady State (or Gallavotti-Cohen) Fluctuation Theorems of non-equilibrium statistical mechanics. Our main objective is to display the minimal, model independent mathematical structure at work behind fluctuation theorems. Besides its conceptual simplicity, another advantage of our approach is its natural extension to quantum statistical mechanics which will be presented in a companion paper. We shall discuss several examples including thermostated systems, open Hamiltonian systems, chaotic homeomorphisms of compact metric spaces and Anosov diffeomorphisms.

This mission is the statement-level formalization of Entropic Fluctuations in Statistical Mechanics I. Classical Dynamical Systems (arXiv:1009.3248v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

21 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Finite-time Evans–Searles theorem (Proposition 3.3, 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

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

• Proposition 3.9: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
• Proposition 4.2: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• Proposition 4.3: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• Proposition 4.5: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• Proposition 4.6: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• Proposition 5.6: Unpinned/incorrect source hypothesis or conclusion for Proposition 5.6 (source-ambiguity)
• Proposition 5.15: Unpinned/incorrect source hypothesis or conclusion for Proposition 5.15 (source-ambiguity)
• Proposition 5.16: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
• Proposition 5.17: Unpinned/incorrect source hypothesis or conclusion for Proposition 5.17 (source-ambiguity)
• Proposition 6.3: Unpinned/incorrect source hypothesis or conclusion for Proposition 6.3 (source-ambiguity)
• Proposition 6.4: Unpinned/incorrect source hypothesis or conclusion for Proposition 6.4 (source-ambiguity)
• Proposition 6.5: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
• Proposition 9.1: Gaussian cylinder probability, trace-class quadratic observable and evolved covariance (hard)
• Proposition 9.2: Gaussian cylinder probability, trace-class quadratic observable and evolved covariance (hard)
• Proposition 9.3: Unpinned/incorrect source hypothesis or conclusion for Proposition 9.3 (source-ambiguity)
• Theorem 9.4: Unpinned/incorrect source hypothesis or conclusion for Theorem 9.4 (source-ambiguity)
• Proposition 9.5: Unpinned/incorrect source hypothesis or conclusion for Proposition 9.5 (source-ambiguity)
• Corollary 10.4: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Proposition 10.5: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Corollary 10.6: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Proposition 10.7: Unpinned/incorrect source hypothesis or conclusion for Proposition 10.7 (source-ambiguity)
• Proposition 10.9: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Proposition 10.11: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Proposition 10.12: Resolution of printed sup versus inf in the concave rate, and the actual source weak-Gibbs/pressure interface (source-ambiguity)
• Proposition 10.13: Resolution of printed sup versus inf in the concave rate, and the actual source weak-Gibbs/pressure interface (source-ambiguity)
• Proposition 10.14: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Proposition 10.15: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Corollary 10.16: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Proposition 11.2: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
• Proposition 11.4: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
• Proposition 11.5: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
• Theorem 11.6: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
• discrete-integrated-entropy: Well-defined separate extended expectations of every transported discrete summand (source-ambiguity)
• reference-L2-moment-representation: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
• discrete-transfer-representation: Unpinned/incorrect source hypothesis or conclusion for discrete-transfer-representation (source-ambiguity)
• differentiable-jacobian-entropy: Euclidean C1 dynamics on a compact invariant set, normalized restricted Lebesgue probability, and its RN/Jacobian and divergence identification (hard)
• thermostat-energy-and-entropy: Unpinned/incorrect source hypothesis or conclusion for thermostat-energy-and-entropy (source-ambiguity)
• gas-exact-trajectory: Unpinned/incorrect source hypothesis or conclusion for gas-exact-trajectory (source-ambiguity)
• gas-finite-pressure: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
• canonical-smooth-flux: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• ges-functional-structure: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• finite-response-positivity: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• finite-einstein-relations: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• hamiltonian-flux-and-cocycle: General finite-dimensional coupled Hamiltonian system, normalized Gibbs probability on its convergence domain, and Poisson-bracket reservoir fluxes (hard)
• hamiltonian-TRI-criterion: Unpinned/incorrect source hypothesis or conclusion for hamiltonian-TRI-criterion (source-ambiguity)
• harmonic-finite-gaussian-formula: Unpinned/incorrect source hypothesis or conclusion for harmonic-finite-gaussian-formula (source-ambiguity)
• gas-asymptotic-entropy: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
• gas-asymptotic-pressure-and-response: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
• finite-harmonic-zero-currents: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
• harmonic-thermodynamic-limit: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
• harmonic-scattering-pressure: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
• harmonic-explicit-pressure-and-current: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
• harmonic-explicit-LDP: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
• harmonic-analytic-bound-and-FDT: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
• harmonic-energy-conservation: Unpinned/incorrect source hypothesis or conclusion for harmonic-energy-conservation (source-ambiguity)
• gas-NESS-and-GC-failure: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
• harmonic-NESS-and-GGC: concrete pinned-chain operators, Gaussian configuration laws and Fredholm/scattering calculus (hard)
• regular-fluctuation-implications: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• bernoulli-pressure-and-NESS: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
• bernoulli-FDT: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
• baker-Bernoulli-isomorphism: Unpinned/incorrect source hypothesis or conclusion for baker-Bernoulli-isomorphism (source-ambiguity)
• dilation-pressure-and-NESS: actual microcanonical/Bernoulli/dilation model and its flow-induced laws (hard)
• dilation-linear-response-counterexamples: Unpinned/incorrect source hypothesis or conclusion for dilation-linear-response-counterexamples (source-ambiguity)
• gaussian-configuration-and-support: Gaussian cylinder probability, trace-class quadratic observable and evolved covariance (hard)
• pressure-time-reversal: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• RN-entropy-homology: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• positive-Markov-fluctuations: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Markov-controlled-FDT: source pressure, partition entropy, normalized weak-Gibbs class and regular/specification dynamics (hard)
• Anosov-Jacobian-reversal-homology: Unpinned/incorrect source hypothesis or conclusion for Anosov-Jacobian-reversal-homology (source-ambiguity)
• Anosov-finite-time-ES: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
• Anosov-unique-NESS-and-LDP: Ck-Anosov manifold, stable/unstable Jacobians and SRB/NESS parameter family (hard)
• Proposition 5.15 part-2: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• Proposition 5.15 parts-3-4: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• Proposition 6.4 part-2: actual force-dependent flux laws, mixed moment regularity and full fluctuation-dissipation property (hard)
• NESS-L2-moment-representation: weightedTransferOperators / actual closed Liouvillean / resolvent (hard)
• regular-pressure-limit-exchange: Unpinned/incorrect source hypothesis or conclusion for regular-pressure-limit-exchange (source-ambiguity)
• gaussian-parameter-extension: Unpinned/incorrect source hypothesis or conclusion for gaussian-parameter-extension (source-ambiguity)
• Smale-transitivity-specification: Unpinned/incorrect source hypothesis or conclusion for Smale-transitivity-specification (source-ambiguity)
• Anosov-flow-extensions: Unpinned/incorrect source hypothesis or conclusion for Anosov-flow-extensions (source-ambiguity)

Selected references

• Entropic Fluctuations in Statistical Mechanics I. Classical Dynamical Systems, arXiv:1009.3248v2, https://arxiv.org/abs/1009.3248v2

Motivation

We point out a general argument leading from the formula for currents through an open mesoscopic system given by the theory of non-equilibrium steady states (NESS) to the Landauer-Büttiker formula.

This mission is the statement-level formalization of A general proof of Landauer-Büttiker formula (arXiv:math-ph/0603030v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Two-channel optical theorem with the Landauer–Büttiker transition normalization (Equations (15)–(17), PDF p. 5). 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

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

• Equation (19), main result; assumptions pp.2–4 and proof pp.5–6: Precisely specified rigged-Hilbert-space stationary scattering data, admissible resolvent boundary values, and a justified trace-to-transmission integral interface for the actual model. (source-ambiguity)
• Remark i, equation (24): The stationary scattering interface of (19), plus an energy-current commutator with its actual operator domain, trace-class extension and energy-weighted integrability. (source-ambiguity)
• Remark ii, unequal reservoir spectra: The stationary scattering interface of (19), with measurable channel fibers indexed by the distinct reservoir spectral supports. (source-ambiguity)
• Remark iii, equation (25): The stationary scattering interface of (19) for finitely many actual reservoirs, tied to the same incoming occupation and on-shell transition matrix. (source-ambiguity)
• Remark iii, charge conservation and normality: An assembled unbounded self-adjoint reservoir/sample model and canonical incoming occupation and finite-rank charge-current trace, together with the same model’s on-shell scattering representation. (hard)
• Remark iv, multiple spectral channels: Measurable reservoir channel fields of unrestricted multiplicity, correctly directed transmission blocks and their trace-class products, attached to the actual trace-current model. (source-ambiguity)

Selected references

• A general proof of Landauer-Büttiker formula, arXiv:math-ph/0603030v4, https://arxiv.org/abs/math-ph/0603030v4

Motivation

We establish a framework for cellularity of algebras related to the Jones basic construction. Our framework allows a uniform proof of cellularity of Brauer algebras, ordinary and cyclotomic BMW algebras, walled Brauer algebras, partition algebras, and others. Our cellular bases are labeled by paths on certain branching diagrams rather than by tangles. Moreover, for the class of algebras that we study, we show that the cellular structures are compatible with restriction and induction of modules. Applied to cyclotomic BMW algebras, our method allows a new a shorter proof of the finite spanning result and isomorphism with cyclotomic Kauffman tangle algebras.

This mission is the statement-level formalization of Cellularity and the Jones basic construction (arXiv:0906.1496v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Free modules embed into their fraction-field scalar extension (Lemma 2.20, PDF p. 15). 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

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

• Lemma 2.1: Tagged involution twist of both bimodules and their balanced tensor; descended C-B actions; canonical twist-reversing tensor map (hard)
• Lemma 2.9: Invariant two-sided ideals, split-ideal predicate with actual left ideal, and M tensor_R i(M) with both A actions and swap involution (hard)
• Lemma 2.10: Finite proper cell chains with split successive quotient ideals, actual quotient involutions, and relaxed cellular data (hard)
• Proposition 2.13: Lambda-cell net on upward-closed label sets, quotient bimodule actions and fixed-label cell data (hard)
• Lemma 2.19: Scalar-extended noncommutative algebra/module actions and canonical balanced-tensor base-change map, including optional left and right B^F actions (hard)
• Lemma 2.22: Constructed cell modules and coherent towers; all finite induction/restriction cell filtrations; actual generic inclusion multiplicities (hard)
• Lemma 2.23: Actual generic multiplicity-free branching paths and reindexed cellular data on the original label posets (hard)
• Theorem 3.2: All eight framework axioms on actual towers; constructed coherent cell-data family; reflected label order and branching multiplicities; same-level ideal-action scalar extension (hard)
• Lemma 4.1: Iterated noncommutative balanced tensor with canonical fraction-field base change and both optional B^F actions (hard)
• Lemma 4.2: Semisimple noncommutative algebra, two-sided ideal as a bimodule, and the induced contraction map on iterated balanced tensors (hard)
• Proposition 4.3: Full finite-tower induction setup; actual J(Gamma), Jhat(Gamma), tensor domain with A_(n+1) actions, unscaled Phi and inclusion beta (hard)
• Lemma 4.4: Canonical Phi and beta for nested cellular order-ideal spans within the finite-tower induction setup (hard)
• Lemma 4.5: Canonical Phi from the actual free tensor domain to Jhat(Gamma), with ambient bimodule actions (hard)
• Corollary 4.6: Canonical unscaled map xe_n tensor e_ny to xe_ny between actual A_(n+1) bimodules (hard)
• Proposition 4.7: Actual Jhat cell net; ambient cellular ideal; lifted ordinal-sum cellular datum and its tensor cell modules (hard)
• Corollary 4.8: Constructed next-level cellular datum and reflected disjoint-union label poset with both order cases (hard)
• Corollary 4.9: Same constructed next-level cell modules and basic-construction ideal-action submodule, extended to F only in the lower-label case (hard)
• Proposition 4.10: Restriction of every actual newly constructed cell module and genuine finite A_n-submodule filtrations (hard)
• Lemma 4.11: Scalar-extended noncommutative semisimple algebra and the canonical map id_P tensor inclusion on balanced tensors (hard)
• Lemma 4.12: Given actual finite cell filtration; canonical tensor embeddings, quotient maps, transported labels and next-level module action (hard)
• Lemma 4.13: Actual restriction functor and the two balanced tensor modules with A_(n+1)-linear equivalences (hard)
• Proposition 4.14: Ideal-tensor module, actual induction module, canonical embedding and quotient, and both Q_(n+1) and A_(n+1) cell filtrations (hard)
• Corollary 4.15: Simultaneously constructed cellular data and induction/restriction cell filtrations through level n+1 (hard)
• Corollary 4.16: Actual generic simple modules and inclusion matrices through n+1, and reflection preserving edge multiplicities (hard)
• Lemma 5.2: Brauer loop-count diagram algebra, inclusions and contraction e_n; actual corner and right-product submodules (hard)
• Lemma 5.3: Canonical Brauer strand inclusion, e_n, right-ideal images and multiplication-by-e_n map (hard)
• Proposition 5.4: Concrete generic Brauer and symmetric-group towers, involutions and all-eight-axiom framework predicate (hard)
• Corollary 5.5: Actual specialized Brauer cellular tower, parity Young labels, up-down paths, and whole compatible datum family (hard)
• Proposition 5.6: Temperley-Lieb presented algebra and structure maps over Z[delta]; constant quotient tower; all framework axioms (hard)
• Corollary 5.7: Specialized Temperley-Lieb cellular tower with actual at-most-two-row Young labels and standard-tableau bases (hard)
• Lemma 5.9: Ordinary BMW presentation with all seven relation groups, canonical strand maps, and corner/right-product submodules (hard)
• Lemma 5.10: Ordinary BMW algebra and generator-preserving homomorphism between levels, right-ideal images, and multiplication map (hard)
• Proposition 5.11: Generic BMW coefficient quotient ring, ordinary BMW/Hecke towers with matching quadratic convention, all framework axioms (hard)
• Corollary 5.12: Full BMW coefficient systems and actual specialized coherent cell data with parity Young labels and up-down bases (hard)
• Lemma 5.20: Geometric cyclotomic KT_0 with all local affine-loop/skein relations, canonical empty diagram, and actual W_0 (hard)
• Lemma 5.21: Actual admissible cyclotomic BMW/KT algebras and canonical phi and strand homomorphisms (hard)
• Lemma 5.23: Full generic admissible coefficient system and presented cyclotomic W_n; actual cardinal module rank and pairing count (hard)
• Lemma 5.24: Actual generic cyclotomic W_n and geometric KT_n, canonical phi and finite spanning-set cardinality (hard)
• Lemma 5.25: Actual W_0,W_1,W_2,KT_1 and cyclotomic H_1; canonical maps and finite free rank (hard)
• Lemma 5.26: Canonical cyclotomic phi maps at all levels through n, geometric KT and BMW strand maps, and corner/right-ideal images (hard)
• Theorem 5.27: Concrete generic cyclotomic BMW/Hecke framework pair, geometric KT with canonical phi, inclusions and constructed coherent cell data (hard)
• Corollary 5.28: Admissible specialized cyclotomic BMW/KT towers, canonical phi, multipartition cellular modules and up-down bases (hard)
• Lemma 5.31: Actual walled Brauer diagram subalgebras, long-range e_(a,b), both strand inclusions and both closure maps (hard)
• Lemma 5.32: Walled Brauer two-sided contraction ideal and actual involutive quotient to the product symmetric-group algebra (hard)
• Lemma 5.33: Walled Brauer left/right strand inclusions and contraction right-ideal images in two different ambient algebras (hard)
• Lemma 5.34: Actual Brauer and walled diagram multiplication and normalized full-closure traces over Q(delta) (hard)
• Lemma 5.35: Walled Brauer algebra over Q(delta) and finite product-of-full-matrix-algebras meaning of split semisimplicity (hard)
• Proposition 5.36: Alternating walled algebra and quotient towers, generators f_n, and generalized framework with replacement axiom (3 prime) (hard)
• Corollary 5.38: Walled cellular data for all pairs, both restriction/induction filtrations, integer size-difference labels and augmented branching paths (hard)
• Lemma 5.39: Actual even/odd partition diagram algebras and propagating ideals, quotient involutions and symmetric-group algebras (hard)
• Lemma 5.40: Partition diagram products, embeddings, propagating ideal J_k and image of A_(k-1)p_(k-1)A_(k-1) (hard)
• Lemma 5.41: Partition generators p_k, canonical level inclusions, and corner/right-product submodules with alternating parity (hard)
• Lemma 5.42: Partition tower canonical inclusions and actual map x to x p_(k-1), correcting the printed e notation (hard)
• Lemma 5.43: Actual partition diagram algebra and its alternating normalized closure trace over Q(delta) (hard)
• Proposition 5.45: Concrete generic partition and repeated symmetric-group quotient towers, p generators, and all framework axioms (hard)
• Corollary 5.46: Actual specialized partition cellular tower, corrected half-level Young labels and Lemma 5.44 branching-path bases (hard)
• Lemma 5.47: Oriented A-labelled planar algebra, western-depth subalgebra and every label generator a^(k) (hard)
• Lemma 5.48: Actual depth-restricted labelled planar algebra, strand inclusions and e generators with corner/right-product submodules (hard)
• Lemma 5.49: Contour strand homomorphisms, right-ideal images and actual multiplication-by-e_(n-1) map (hard)
• Lemma 5.50: Generic labelled contour algebra and normalized closure trace extended from the specified cellular label algebra (hard)
• Lemma 5.51: Actual generic contour algebra and finite-dimensional split matrix-block decomposition predicate (hard)
• Proposition 5.52: Concrete contour and tensor-power quotient towers over R_0[delta], with orientation-sensitive embeddings and all framework axioms (hard)
• §2.2: cell modules and canonical layer tensor isomorphism: Cell representation constructed from triangular coefficients; column and layer quotient actions; invariant cell ideals; canonical bimodule tensor-layer equivalence (hard)
• Remark 2.6: extensions of cellular algebras: Ambient cellular-ideal data, actual quotient involution and basis, ordinal-sum order and every choice of quotient-basis lifts (hard)
• Remark 2.11: strict cell chains: Finite proper cell chains with involution-invariant R-module complements at every successive pair (hard)
• Remark 2.14: strict cell nets: Fixed-Lambda cell nets, all nested-ideal and principal-layer invariant complements, and strict cellular data (hard)
• Remark 2.24: inductively lifted path bases: Actual restriction filtrations and quotient isomorphisms, recursive arbitrary R-linear lifts, and actual branching paths (hard)
• Remark 3.3: path-indexed cell bases: Constructed basic-construction cell data on reflected label posets and multiplicity-free generic branching paths (hard)
• Remark 5.29: strictly cellular cyclotomic Murphy-type bases: Full generic cyclotomic BMW presentation and coefficient system, strict cellular data and multipartition up-down path bases (hard)
• Remark 5.37: quotient walled branching diagram: Product symmetric-group quotient tower, its actual generic simple modules and inclusion multiplicities, and bipartition Young labels (hard)

Selected references

• Cellularity and the Jones basic construction, arXiv:0906.1496v2, https://arxiv.org/abs/0906.1496v2

Motivation

We propose a unified framework in which the different constructions of cohomology groups for topological and Lie groups can all be treated on equal footings. In particular, we show that the cohomology of "locally continuous" cochains (respectively "locally smooth" in the case of Lie groups) fits into this framework, which provides an easily accessible cocycle model for topological and Lie group cohomology. We illustrate the use of this unified framework and the relation between the different models in various applications. This includes the construction of cohomology classes characterizing the string group and a direct connection to Lie algebra cohomology.

This mission is the statement-level formalization of A Cocycle Model for Topological and Lie Group Cohomology (arXiv:1110.3304v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem VI.2: delta-functor comparison principle (Theorem VI.2: delta-functor comparison principle, PDF p. 25). 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

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

• Theorem IV.5 (Comparison Theorem); introductory theorem p. 2: Segal-Mitchison and global continuous cohomology as concrete delta-functors on locally contractible k-G-modules (hard)
• Remark I.2: local coefficient long exact sequences: Unnormalized continuous/smooth local cohomology and lift-defined connecting homomorphisms (hard)
• Remark I.3: degrees zero, one, two: Low-degree regular cohomology and the Baer group of locally trivial abelian extensions (hard)
• Remark I.4: comparison in low degrees and global coefficient sequence: Actual global-to-local cohomology maps, globally split coefficient sequences and connected-G extension comparison (hard)
• Proposition I.5: loop-contractible comparison (cited): Loop-contractible comparison for unnormalized regular cochain complexes (hard)
• Lemma I.6: discrete smooth-continuous comparison: Inclusion-induced map on the unnormalized discrete-coefficient local smooth and local continuous cohomologies (hard)
• Proposition I.7: finite-dimensional comparison: Regular cohomology inclusion for quasi-complete locally convex discrete-submodule quotients (hard)
• Remark I.8: ordinary-product variant: Ordinary-product local/global cohomology and locally split connecting sequences (hard)
• Remark II.2: simplicial sheaves form an abelian category with injectives: Category of compatible abelian sheaves on a simplicial space, with componentwise operations (hard)
• Lemma II.4: left exact section functor: The actual simplicial section functor ker(D0-D1) (hard)
• Proposition II.6: simplicial sheaf spectral sequence: Derived simplicial section cohomology, first-quadrant spectral sequence and convergence filtration (hard)
• Corollary II.8: acyclic component calculation: Cosimplicial section Moore complex and its comparison with derived simplicial sections (hard)
• Lemma II.11: simplicial coefficient sequences: Continuous and smooth simplicial coefficient functors with natural connecting maps (hard)
• Proposition II.12: contractible simplicial coefficients: Contractible-coefficient simplicial-to-global comparison (hard)
• Proposition II.15: local sheaves are soft: Local-regularity abelian sheaf, softness and positive-degree sheaf cohomology (hard)
• Corollary II.16: local sheaf model: Derived sections of local-regularity simplicial sheaves and local cohomology (hard)
• Remark II.17: sheaf-to-local comparison morphisms: Sheaf-inclusion-induced natural morphisms from simplicial to local cohomology (hard)
• Remark III.2: construction of semi-simplicial good covers: Coherent semi-simplicial open covers and good refinements (hard)
• Proposition III.4: Cech sequences and spectral sequence: Leray comparison for arbitrary sheaves on a fixed good cover (source-ambiguity)
• Remark III.5: explicit degree-two comparison: Consistent explicit right-fiber-coordinate Cech comparison (source-ambiguity)
• Lemma IV.3: sections of the soft embedding (cited): Thin Segal realization E_G(A), quotient B_G(A), local/global sections (hard)
• Proposition IV.4: soft module acyclicity: Globally continuous cohomology of the actual coinduced k-function module (hard)
• Remark IV.6: weaker loop-contractible comparison axiom: Loop contraction of actual Segal realization/coinduction and comparison on contractible coefficients (hard)
• Corollary IV.7: Natural Segal-Mitchison/simplicial cohomology comparison (hard)
• Corollary IV.8: Canonical local/Segal comparison and simplicial-to-local inclusion map (hard)
• Corollary IV.9: All three canonical arrows between smooth and continuous simplicial/local cohomology (hard)
• Corollary IV.10: Segal cohomology and fixed-good-cover Cech total cohomology (hard)
• Remark IV.11: explicit Cech-to-local map: Staircase Cech-to-local comparison as a delta-functor morphism (hard)
• Remark IV.12: Flach comparison: Precise Flach external cohomology functor and coefficient category (hard)
• Remark IV.12: smooth infinity-groupoid comparison: The cited big smooth topos cohomology and exact Schreiber comparison (hard)
• Remark IV.13: Moore and locally continuous measurable comparisons: Polish coefficient category, Borel/local-measurable cochain quotients and delta-functor comparisons (hard)
• Remark IV.14: bounded comparison for compact groups: Bounded and unbounded continuous Banach-coefficient cohomology with inclusion-induced map (hard)
• Remark IV.16(1): Twisted classifying-space cohomology with pi0 action and Hurewicz comparison (hard)
• Remark IV.16(2): Contractible-G global/local/Segal comparison maps (hard)
• Remark IV.16(3): Discrete-submodule quotient coefficients, twisted BG cohomology and degree-shift comparison (hard)
• Example V.1(1): spherical string four-cocycle: Actual smooth simplex fillings and their homology-valued four-cocycle (hard)
• Example V.1(2): integral string cocycle and connecting identity: Cartan-form singular integral, real lift, string cocycle and actual coefficient connecting map (hard)
• Example V.1(3) and continuation: external string models: External strict and stacky string models and characteristic classes (hard)
• Example V.2: characteristic spherical cocycles: Based simplex-valued filling choices, singular homology cocycle and choice independence (hard)
• Example V.2: realization gives a connected cover: Correctly indexed path-loop extension and connected-cover realization (source-ambiguity)
• Theorem V.4: crossed-module classification: Topologically split crossed modules, zigzag equivalence and characteristic 3-class (hard)
• Remark V.5: metrizable crossed-module realization: The constructed metrizable crossed module and string-generator specialization (hard)
• Remark V.6: topology on local cohomology: Shrinking-neighborhood colimit topology on local cochains and quotient cohomology (hard)
• Remark V.7: cup products and compatibility: Actual kTop tensor cup product, induced cohomology product and differentiation compatibility (hard)
• Equation (13): degree-two topological characteristic sequence: Bundle-characteristic map on actual ordinary-product H^2 and its compatible-extension image (hard)
• Proposition V.8: explicit Cech characteristic map: Explicit translated-cover Cech cocycle and induced natural characteristic homomorphism (hard)
• Proposition V.9: edge map is the explicit characteristic map: Filtered simplicial spectral-sequence edge and its actual characteristic-map square (hard)
• Remark V.10: degree-one edge with trivial action: Degree-one trivial-action edge and characteristic map (hard)
• Remark V.11: other edge is inclusion of global cochains: Other filtered edge, E2^(n,0) identification and inclusion-induced global-to-local map (hard)
• Corollary V.12: injectivity of the characteristic map: Actual tau_(n+1) on discrete-coefficient local cohomology and full Cech cohomology (hard)
• Remark V.13: primitive image: Cech pullbacks along multiplication/projections and the range of actual tau (hard)
• Remark V.13: string classes are generators: Integral string classes, characteristic isomorphisms and generator property (hard)
• Remark V.14: kernel of differentiation: Differentiation of actual local smooth quotient cohomology (hard)
• Remark V.14: discrete-coefficient exact sequence: Continuity of the same coefficient action after discretizing A (source-ambiguity)
• Remark V.14: van Est comparison (cited): Actual differentiation map, van Est comparison and split de Rham extension (hard)
• Remark V.14: period criterion and explicit integration: Consistent equivariant simplex integral and spherical period map for nontrivial coefficients (source-ambiguity)
• Example VI.5: effacement for sheaf cohomology: Positive-degree Cech/sheaf cohomology of actual E_G(A) (hard)
• Remark VI.6: counterexample to weaker comparison hypotheses: Concrete geometric counterexamples to weakened effacement hypotheses (hard)
• Section VII observation 1: invariants of a coinduced module: Coinduced k-function module and invariants on admissible extensions (hard)
• Section VII observation 2: soft resolutions compute SM: Arbitrary soft resolution, constituent local sections and its invariant cohomology complex (hard)
• Section VII observation 3: contractible coinduced quotients: Contractible coinduced quotient and its canonical coinduction isomorphism (hard)
• Section VII conclusion: SM soft acyclicity: Exact invariant augmented soft resolution and positive-degree Segal cohomology (hard)
• Section VII conclusion: SM equals global cohomology on contractible coefficients: Homogeneous coinduced resolution, natural invariant cohomology and global comparison (hard)

Selected references

• A Cocycle Model for Topological and Lie Group Cohomology, arXiv:1110.3304v3, https://arxiv.org/abs/1110.3304v3

Motivation

We present an axiomatic approach to finite- and infinite-dimensional differential calculus over arbitrary infinite fields (and, more generally, suitable rings). The corresponding basic theory of manifolds and Lie groups is developed. Special attention is paid to the case of mappings between topological vector spaces over non-discrete topological fields, in particular ultrametric fields or the fields of real and complex numbers. In the latter case, a theory of differentiable mappings between general, not necessarily locally convex spaces is obtained, which in the locally convex case is equivalent to Keller's C^k_c-theory.

This mission is the statement-level formalization of Differential Calculus, Manifolds and Lie Groups over Arbitrary Infinite Fields (arXiv:math/0303300v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

17 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Regularity of a co-restriction to a subspace (Lemma 10.1, PDF p. 48). 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

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

• Remark 1.2: C0Concept, ConceptLinearMaps (hard)
• Remark 1.4: C0Concept, ConceptDense (hard)
• Proposition 2.2: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ConceptLinearMaps (hard)
• Example 2.3: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Lemma 2.6: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Proposition 3.1 (Chain Rule): C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TangentMapOnDomain, ExtendedTangentMap (hard)
• 3.2 Linearity: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• 3.3 Product rule: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ConceptBilinearMap (hard)
• 3.4 Polynomial maps: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ModulePolynomialMap (hard)
• 3.5 Quotient rule: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ConceptInverseAlgebra (hard)
• 3.6 Rational maps: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, ModulePolynomialMap, RationalMap (hard)
• 3.7 Direct Products: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• 3.8 Rule on partial derivatives: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, PartialDifferenceQuotient (hard)
• Lemma 3.9: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, PartialDifferenceQuotient (hard)
• Remark 4.2: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Example 4.3: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Lemma 4.4: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Proposition 4.5: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Lemma 4.6 (Schwarz): C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, HigherDifferential (hard)
• Lemma 4.8: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, HigherDifferential (hard)
• Lemma 4.9: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Theorem 5.1: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TaylorCoefficient, TaylorRemainder (hard)
• Lemma 5.2: C0Concept, FiniteExpansion (hard)
• Proposition 5.3: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TaylorCoefficient, HigherDifferential (hard)
• Theorem 5.4: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TaylorCoefficient, TaylorRemainder, HigherDifferential (hard)
• Unnumbered second-quotient identity after Theorem 5.4: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, HigherDifferential, TaylorCoefficient (hard)
• Lemma 5.5: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Theorem 5.6: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, TaylorCoefficient, TaylorRemainder, ModulePolynomialMap (hard)
• Lemma 6.1: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, CurveDividedDifference (hard)
• Proposition 6.2: C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential, CurveDividedDifference, HigherDifferential, TaylorCoefficient, TaylorRemainder (hard)
• Remark 6.4: C0Concept, ConceptDense (hard)
• Lemma 6.6: C0Concept standing environment, plus symmetric raw-quotient splicing identity (hard)
• Lemma 6.7: SchikhofCk, CurveDividedDifference (hard)
• Lemma 6.8: SchikhofCk, CurveDividedDifference, C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Proposition 6.9: SchikhofCk, CurveDividedDifference, C0Concept, ConceptCk, ExtendedDifferenceQuotient, Differential (hard)
• Lemma 7.1: The Section 7 continuous C^0-concept construction over a Hausdorff commutative topological ring: the class of all Hausdorff topological K-modules, product topologies, and C^0(U,F) equal to continuous maps. Package axioms I.1–I.5 and II.1–II.5 and prove III: for every open U ⊆ K and Hausdorff topological K-module F, continuous f,g : U → F agreeing on U ∩ {a : K | IsUnit a} agree everywhere, assuming the units are dense. Include the nondiscrete topological-field specialization; open units and continuous inversion are the source’s standing topological-ring requirements. (hard)
• Proposition 7.4: MichalBastianiCk, ExtendedDifferenceQuotient, Differential (hard)
• Lemma 7.5: MichalBastianiCk, RepresentedWeakIntegral, FirstVariableDifferential (hard)
• Lemma 7.6: MichalBastianiCk, RepresentedWeakIntegral, FirstVariableDifferential (hard)
• Proposition 7.7: MichalBastianiCk, LocallyConvexComplexAnalytic, ContinuousDiagonalPolynomial, MackeyComplete, ExtendedDifferenceQuotient, Differential (hard)
• Proposition 7.11: PolynormedSpace, StrictDifferentiable, StrictCk, ExtendedDifferenceQuotient, Differential (hard)
• Proposition 7.20: UltrametricLocallyConvexSpace, ContinuousDiagonalPolynomial, PolynomialSeminorm, StrictConvergenceIndicatrix, UltrametricAnalytic, ExtendedDifferenceQuotient, Differential (hard)
• §7.3 Rational calculus: C0Concept, RationalMap, ZariskiVectorTopology, ConceptCk (hard)
• Remark 7.21: AlgebraicKGroup, RationalLieGroup (source-ambiguity)
• §7.4 Convenient calculus: C0Concept, CInfinityRefinement, MackeyComplete, ConvenientSmoothMap, ConceptCk (hard)
• §8.1 Category and products: ConceptManifold, ManifoldCkMap, ConceptProductManifold, SmoothScalarFunctions (hard)
• §8.2 Tangent functor: ConceptManifold, ManifoldCkMap, TangentVector, ConceptTangentBundle, ManifoldTangentMap (hard)
• §8.3 Bundle gluing: ConceptManifold, ManifoldCkMap, SmoothBundleCocycle, ConceptFiberBundle, ConceptVectorBundle (hard)
• §8.4 Sections and derivations: ConceptVectorBundle, SmoothSection, VectorField, SmoothScalarFunctions, VectorFieldDerivation, ManifoldTangentMap (hard)
• Example 8.2: VectorField, SmoothScalarFunctions, VectorFieldDerivation, QuasiBanachLp, ConceptManifold (hard)
• Example 8.3: VectorField, VectorFieldDerivation, SmoothScalarFunctions, HigherDifferential, CompactSymmetricBilinearForms, ConceptManifold (hard)
• Theorem 8.4: VectorField, VectorFieldBracket, ConceptManifold, ManifoldTangentMap (hard)
• Lemma 8.5: VectorField, VectorFieldBracket, RelatedVectorFields, ManifoldTangentMap, ConceptDiffeomorphism (hard)
• Unnumbered Lie homomorphism after Lemma 8.5: VectorField, VectorFieldBracket, VectorFieldDerivation, SmoothScalarFunctions (hard)
• §9.1 Tangent multiplication: ManifoldWithMultiplication, ConceptTangentBundle, ManifoldTangentMap (hard)
• §9.2 Tangent Lie group: ConceptLieGroup, ConceptTangentBundle, ManifoldTangentMap, LieGroupMorphism (hard)
• §9.3 Left invariant fields: ConceptLieGroup, LeftInvariantVectorField, VectorFieldBracket, TangentLieAlgebra, ManifoldTangentMap (hard)
• Theorem 9.1 (paper seed: Lie functor): ConceptLieGroup, LieGroupMorphism, TangentLieAlgebra, VectorFieldBracket, ManifoldTangentMap (hard)
• 12.2 Highest raw quotient criterion: RawIteratedDifferenceQuotient, ExtendedDifferenceQuotient, ConceptCk (hard)
• Lemma 12.3: RawIteratedDifferenceQuotient, ExtendedDifferenceQuotient, ConceptCk (hard)
• §13.1 Continuous inverse algebra examples: ContinuousInverseAlgebra, ConceptLieGroup, ContinuousFunctionAlgebra (hard)
• Proposition 13.1: SupportedContinuousMapGroup, UniformMapTopology, ConceptLieGroup, LieStructureOnGroup (hard)
• Proposition 13.2: SupportedCrMapGroup, CompactOpenCrTopology, TestFunctionGroup, LocallyConvexDirectLimit, ConceptLieGroup (hard)
• §13.3 Diffeomorphism groups: ConceptDiffeomorphism, CompactOpenCrTopology, CompactSupportVectorFields, DiffeomorphismGroupStructure (hard)
• §13.4 Direct limit groups: ConceptLieGroup, LieGroupMorphism, ClosedSubmanifold, LocallyConvexDirectLimit, DirectLimitGroup (hard)

Selected references

• Differential Calculus, Manifolds and Lie Groups over Arbitrary Infinite Fields, arXiv:math/0303300v1, https://arxiv.org/abs/math/0303300v1

Motivation

We generalize the classical construction principles of infinite-dimensional real (and complex) Lie groups to the case of Lie groups over non-discrete topological fields. In particular, we discuss linear Lie groups, mapping groups, test function groups, diffeomorphism groups, and weak direct products of Lie groups. The specific tools of differential calculus required for the Lie group constructions are developed. Notably, we establish differentiability properties of composition and evaluation, as well as exponential laws for function spaces. We also present techniques to deal with the subtle differentiability and continuity properties of non-linear mappings between spaces of test functions. Most of the results are independent of any specific properties of the topological vector spaces involved; in particular, we can deal with real and complex Lie groups modeled on non-locally convex spaces.

This mission is the statement-level formalization of Lie groups over non-discrete topological fields (arXiv:math/0408008v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The ordinary difference quotient and its continuous extension (Numbered assertion 1.8, PDF p. 14). 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

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

• Numbered assertion 1.7: Canonical iterated extended-quotient domains and values (hard)
• Proposition 1.18: ExtendedDifferenceDomain, BGNLieGroup, BGNManifoldCrMap, BGNManifold (hard)
• Proposition 2.2: The actual BGN Lie structure on the open unit submanifold (hard)
• Numbered assertion 3.2: Uniform-convergence topology on supported continuous maps and ultrametric local convexity (hard)
• Proposition 3.3: SupportedContinuousMaps, ParameterizedPushforward, ExtendedDifferenceDomain (hard)
• Corollary 3.4: SupportedContinuousMaps, ParameterizedPushforward, ExtendedDifferenceDomain (hard)
• Corollary 3.5: SupportedContinuousMaps, ParameterizedPushforward, ExtendedDifferenceDomain (hard)
• Remark 4.2: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.3: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.4: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.5: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.6: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.9: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Remark 4.10: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.11: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.12: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.13: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.14: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 4.15: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Proposition 4.16: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, ParameterizedPushforward (hard)
• Proposition 4.19: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, MackeyComplete, MackeyCauchySequence, UltrametricLocalConvexity, IteratedTangentDerivativeTopology, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, SupportedCrMaps (hard)
• Proposition 4.20: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, SupportedCrMaps, ParameterizedPushforward (hard)
• Corollary 4.21: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, SupportedCrMaps, ParameterizedPushforward (hard)
• Lemma 4.22: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint (hard)
• Proposition 4.23: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint, ParameterizedPushforward (hard)
• Lemma 4.24: CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, SupportedCrMaps (hard)
• Paper seed, pinned to Proposition 5.1: supported mapping groups and tangent bracket: SupportedMappingGroup, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BGNLieGroup, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential (hard)
• Proposition 5.7: SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Numbered assertion 6.3: BoxDirectSumTopology (hard)
• Numbered assertion 6.4: BoxDirectSumTopology, UltrametricLocalConvexity (hard)
• Numbered assertion 6.5: BoxDirectSumTopology, OpenDirectSumBox (hard)
• Remark 6.6: BoxDirectSumTopology, UltrametricLocalConvexity (hard)
• Remark 6.7: BoxDirectSumTopology, UltrametricLocalConvexity (hard)
• Lemma 6.8: BoxDirectSumTopology, ReorderedDifferenceQuotient, ExtendedDifferenceQuotient, ExtendedDifferenceDomain (hard)
• Proposition 6.9: BoxDirectSumTopology, ReorderedDifferenceQuotient, ExtendedDifferenceQuotient, ExtendedDifferenceDomain, OpenDirectSumBox (hard)
• Proposition 6.10: BoxDirectSumTopology, OpenDirectSumBox, ExtendedDifferenceDomain (hard)
• Remark 6.11: BoxDirectSumTopology, AffineAtInfinityGroup, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, CompactOpenCr, CrMappingSpace (hard)
• Proposition 7.1: WeakDirectProductLieChart, BGNLieGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology (hard)
• Lemma 7.2: WeakDirectProductLieChart, BGNLieGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology (hard)
• Lemma 8.3: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, LocalFieldManifoldBall (hard)
• Lemma 8.1: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain (hard)
• Lemma 8.5: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain (hard)
• Lemma 8.7: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ClopenPartitionOfUnity (hard)
• Lemma 8.8: BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ClopenPartitionOfUnity (hard)
• Lemma 8.10: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology (hard)
• Proposition 8.13: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, TestFunctionTVSDirectLimitTopology, TestFunctionLocallyConvexLimitTopology, UltrametricLocalConvexity (hard)
• Remark 8.15: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, TestFunctionLocallyConvexLimitTopology, UltrametricLocalConvexity (hard)
• Remark 8.17: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, BGNVectorBundle, BGNTangentBundle, DirectionalDifferential, CompactSupportVectorFields, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection (hard)
• Example 8.19: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, PatchedVectorSpace (hard)
• Proposition 8.21: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, PatchedMap, PatchedVectorSpace (hard)
• Proposition 8.22: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, ParameterizedPushforward, CompactImageConstraint (hard)
• Corollary 8.23: TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology, ParameterizedPushforward (hard)
• Proposition 9.1: TestFunctionGroup, BGNLieGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, BoxDirectSumTopology (hard)
• Theorem 10.4: LocallyAlmostLocalMap, AlmostLocalMap, TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, BoxDirectSumTopology (hard)
• Proposition 11.1: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint (hard)
• Proposition 11.2: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint, DirectionalDifferential, SupportedCrMaps (hard)
• Proposition 11.3: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint, DirectionalDifferential (hard)
• Lemma 11.4: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint (hard)
• Lemma 12.1: FunctionSpaceCurrying, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Proposition 12.2: FunctionSpaceCurrying, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 12.5: FunctionSpaceCurrying, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, ConvenientKSmooth, ConvenientOpenTopology (hard)
• Proposition 12.6: FunctionSpaceCurrying, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, ConvenientKSmooth, ConvenientOpenTopology (hard)
• Proposition 13.2: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, LocalFieldManifoldBall, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
• Lemma 13.7: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, LocalFieldManifoldBall, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, CompactOpenCr, CrMappingSpace, BoxDirectSumTopology (hard)
• Lemma 13.8: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, LocalFieldManifoldBall (hard)
• Lemma 13.9: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, LocalFieldManifoldBall, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
• Lemma 13.10: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, WeakDirectProductLieChart, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology, LocalFieldManifoldBall (hard)
• Lemma 13.11: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, WeakDirectProductLieChart, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology, LocalFieldManifoldBall (hard)
• Theorem 13.12: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, WeakDirectProductLieChart, BGNLieAlgebraFunctor, BGNTangentMap, BGNTangentBundle, DirectionalDifferential, ExtendedDifferenceQuotient, OpenDirectSumBox, BoxDirectSumTopology, LocalFieldManifoldBall, CompactSupportVectorFields, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, CompactOpenCr, CrMappingSpace (hard)
• Remark 13.14: DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, BGNLieGroup, CompactSupportDiffeomorphisms, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, FunctionSpaceEvaluationAndComposition, CompactImageConstraint (hard)
• Numbered assertion 14.2: CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Numbered assertion 14.3: CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology (hard)
• Numbered assertion 14.5: ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, DirectionalDifferential, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, CompactOpenCr, CrMappingSpace, BoxDirectSumTopology, TestFunctionBoxTopology, CompactSupportCrMaps, SupportedCrMaps (hard)
• Proposition 14.6: NaturalDiffeomorphismManifold, CompactSupportDiffeomorphisms, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNLieGroup (hard)
• Lemma 14.17: CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient (hard)
• Lemma 14.18: CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle (hard)
• Proposition 14.19: NaturalDiffeomorphismManifold, CompactSupportDiffeomorphisms, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNLieGroup (hard)
• Proposition 14.21: NaturalDiffeomorphismManifold, CompactSupportDiffeomorphisms, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNLieGroup (hard)
• Remark 14.22: NaturalDiffeomorphismManifold, CompactSupportDiffeomorphisms, DiffeomorphismGroup, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactSupportEndomorphismChart, CompactSupportEndomorphismMonoid, CompactSupportCrMaps, SupportedCrMaps, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, TestFunctionBoxTopology, BoxDirectSumTopology, ProjectiveFiniteOrderTopology, CompactSupportVectorFields, BGNTangentBundle, DirectionalDifferential, SectionBoxTopology, SupportedCrSections, CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNLieGroup (hard)
• Lemma A.1: IteratedTangentDerivativeTopology, BGNTangentMap, BGNTangentBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, DirectionalDifferential, ExtendedDifferenceQuotient, CompactOpenCr, CrMappingSpace (hard)
• Lemma A.2: IteratedTangentDerivativeTopology, BGNTangentMap, BGNTangentBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, DirectionalDifferential, ExtendedDifferenceQuotient, CompactOpenCr, CrMappingSpace (hard)
• Lemma A.3: IteratedTangentDerivativeTopology, BGNTangentMap, BGNTangentBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, DirectionalDifferential, ExtendedDifferenceQuotient, CompactOpenCr, CrMappingSpace (hard)
• Lemma A.4: Represented weak interval integrals in complete arbitrary locally convex spaces (hard)
• Lemma A.5: Weak-integral domain with all partial directional derivative integrals and induced derivative topology (hard)
• Lemma C.1: FunctionSpaceEvaluationAndComposition, CompactOpenCr, CrMappingSpace, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, ExtendedDifferenceQuotient, CompactImageConstraint (hard)
• Theorem D.1: Mackey completeness and ultrametric local convexity in the source topology (hard)
• Lemma E.1: The six concrete Boman target classes including Mackey completeness and ultrametric local convexity (hard)
• Theorem E.2: Mackey-complete ultrametric locally convex targets and the universal scalar Boman premise (hard)
• Remark F.2: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
• Lemma F.6: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
• Remark F.8: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, UltrametricLocalConvexity (hard)
• Lemma F.9: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
• Theorem F.11: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, FibrePreservingBundleMap, ParameterizedPushforward (hard)
• Numbered assertion F.12: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, WhitneySumBundle (hard)
• Corollary F.13: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
• Lemma F.15: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SupportedCrSections (hard)
• Lemma F.16: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient (hard)
• Lemma F.18: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
• Proposition F.19: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, SectionTVSDirectLimitTopology, SectionLocallyConvexLimitTopology, UltrametricLocalConvexity (hard)
• Remark F.20: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, SectionLocallyConvexLimitTopology, UltrametricLocalConvexity (hard)
• Remark F.21: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, PatchedVectorSpace (hard)
• Lemma F.22: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionImageConstraint, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
• Theorem F.23: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionImageConstraint, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, FibrePreservingBundleMap, ParameterizedPushforward (hard)
• Corollary F.24: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionImageConstraint, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, FibrePreservingBundleMap (hard)
• Remark F.25: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionImageConstraint, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, FibrePreservingBundleMap (hard)
• Numbered assertion F.26: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology, WhitneySumBundle (hard)
• Corollary F.27: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
• Remark F.28: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, BundleOfTopologicalModules, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
• Theorem F.30: CompactOpenCrSectionTopology, CrSection, BGNVectorBundle, BGNManifoldCrMap, BGNManifold, ExtendedDifferenceDomain, CompactOpenCr, CrMappingSpace, ExtendedDifferenceQuotient, AlmostLocalSectionMap, SectionBoxTopology, SupportedCrSections, BoxDirectSumTopology (hard)
• 10.3: local maps are almost local (explicit assertion): Germ and patch predicates on the actual box-topologized compact-support mapping spaces (hard)
• F.29: local maps are almost local (explicit assertion): Germ and patch predicates on actual compact-support section spaces (hard)

Selected references

• Lie groups over non-discrete topological fields, arXiv:math/0408008v1, https://arxiv.org/abs/math/0408008v1

Motivation

In order to study multipartite quantum cryptography, we introduce quantities which vanish on product probability distributions, and which can only decrease if the parties carry out local operations or carry out public classical communication. These ``secrecy monotones'' therefore measure how much secret correlations are shared by the parties. In the bipartite case we show that the mutual information is a secrecy monotone. In the multipartite case we describe two different generalisations of the mutual information, both of which are secrecy monotones. The existence of two distinct secrecy monotones allows us to show that in multipartite quantum cryptography the parties must make irreversible choices about which multipartite correlations they want to obtain. Secrecy monotones can be extended to the quantum domain and are then defined on density matrices. We illustrate this generalisation by considering tri-partite quantum cryptography based on the Greenberger-Horne-Zeilinger (GHZ) state. We show that before carrying out measurements on the state, the parties must make an irreversible decision about what probability distribution they want to obtain.

This mission is the statement-level formalization of Multipartite Classical and Quantum Secrecy Monotones (arXiv:quant-ph/0202103v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

24 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The two classical multipartite secrecy monotones (Abstract; §III, (12)–(17),(24),(28),(30),(35), PDF p. 1). 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

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

• §II.B.1, exact case of (8)–(11): A general exact finite-block LOPC conversion relation retaining arbitrary initial Eve side information, full public-copy transitions, and independent Eve output registers. (hard)
• §II.B.1, (8)–(11): An approximation metric, growth-controlled continuity modulus, and operational asymptotic rate for general M. (source-ambiguity)
• §III.B: The admissible classical local erasure operations, environment initialization/return constraints, entropy cost, and exact/asymptotic precision convention. (source-ambiguity)
• §V.B: The admissible quantum local erasure operations, environment initialization/return constraints, entropy cost, and exact/asymptotic precision convention. (source-ambiguity)
• §V.E, after (70): A correct equality characterization or a source-specified nondegenerate measurement class. (source-ambiguity)

Selected references

• Multipartite Classical and Quantum Secrecy Monotones, arXiv:quant-ph/0202103v1, https://arxiv.org/abs/quant-ph/0202103v1

Motivation

This article presents an isomorphism between two operator algebras $L_1$ and $L_2$ where $L_1$ is the set of operators on a space of Hilbert-Schmidt operators and $L_2$ is the set of operators on a tensor product space. We next compare our isomorphism to a well-known result called Choi's isomorphism theorem. The advantage of Choi's isomorphism is that it takes completely positive maps to positive operators. One advantage of our isomorphism is that it applies to infinite dimensional Hilbert spaces, while Choi's isomorphism only holds for finite dimensions. Also, our isomorphism preserves operator products while Choi's does not. We close with a brief discussion on some uses of our isomorphism.

This mission is the statement-level formalization of Operator Isomorphisms on Hilbert Space Tensor Products (arXiv:2010.15901v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1.3: formula for a basis conjugation (Lemma 1.3, PDF p. 3). 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

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

• Theorem 1.7: the operator C*-algebra isomorphisms R and S: The complete realized rectangular HS Hilbert space and the prescribed bounded maps J_A, J_A*, R, S (hard)
• Theorem 1.1 (background attributed to [3]): matrix-unit basis and three equivalent conditions: Theorem 1.1 (background attributed to [3]): matrix-unit basis and three equivalent conditions (source-ambiguity)
• Theorem 1.2: basis vectorization is unitary, with explicit adjoint: Complete realized HS(H1,H2), its matrix-unit basis, and the bounded series-defined J_A (hard)
• Lemma 1.5: rank-one operators and simple tensors, with conjugation: Rank-one elements of realized HS(H1,H2), J_A and its Hilbert adjoint (hard)
• Corollary 1.6: change of orthonormal bases: Two independently constructed HS vectorizations for the reference and new bases (hard)
• Lemma 1.8: finite-family positivity inequality for R: The prescribed R between endomorphism algebras of the realized HS and completed tensor spaces (hard)
• Theorem 1.9: R preserves the HS class and HS inner product: Nested realized HS Hilbert spaces and the restriction of source R (hard)
• Lemma 2.1: the one-basis vectorization equals J_A: HS-domain one-basis vectorization T_B and independently defined two-basis J_A (hard)
• Lemma 2.3: slice expansion of T_B adjoint: The bounded HS-domain T_B and HS-valued rank-one slice series (hard)
• Unnumbered claim: the spectrum characterization of conjugation: Unnumbered claim: the spectrum characterization of conjugation (source-ambiguity)
• Unnumbered consequence: positivity and complete positivity of R and S: Prescribed R and S on the full bounded endomorphism algebras of the HS Hilbert space and completed tensor space (hard)
• Unnumbered analogue of Theorem 1.9 for S: Nested realized HS Hilbert spaces and source S restricted to the HS class (hard)
• Unnumbered comparison: Choi fails product preservation and differs from R: Compatible finite HS Hilbert realization, prescribed R, and unnormalized input-first Choi map (hard)
• Discussion: concatenation of the displayed Kraus maps: Bounded HS endomorphisms and actual HS-norm-convergent Kraus sandwich series (hard)
• Equations (3.1)–(3.2): R of a represented Kraus map: HS-valued Kraus representation, constructed M_alpha and source R (hard)
• Discussion: adapted product vectors and their rank-one projections under S: Adapted complete bases, source J_A*, and S acting on rank-one projections (hard)
• Discussion: Schmidt coefficients detect entanglement and give the J_A* image: Finite realized HS Hilbert space and J_A* for the supplied Schmidt bases (hard)
• Discussion: the printed general product-operator action under S: Discussion: the printed general product-operator action under S (source-ambiguity)
• Discussion: the final printed HS expansion: Discussion: the final printed HS expansion (source-ambiguity)

Selected references

• Operator Isomorphisms on Hilbert Space Tensor Products, arXiv:2010.15901v1, https://arxiv.org/abs/2010.15901v1

Motivation

We study optimal teleportation based on the Bell measurements. An explicit expression for the quantum channel associated with the optimal teleportation with an arbitrary mixed state resource is presented. The optimal transmission fidelity of the corresponding quantum channel is calculated and shown to be related to the fully entangled fraction of the quantum resource, rather than the singlet fraction as in the standard teleportation protocol.

This mission is the statement-level formalization of Optimal Teleportation Based on Bell Measurement (arXiv:quant-ph/0208015v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

3 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Optimal Bell-measurement teleportation channel and attained mean fidelity (Theorem 3, Eqs.(14)-(15): optimal Bell-measurement channel and maximal mean fidelity (abstract seed), PDF p. 6). 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.

Selected references

• Optimal Teleportation Based on Bell Measurement, arXiv:quant-ph/0208015v2, https://arxiv.org/abs/quant-ph/0208015v2

Motivation

We construct classes of von Neumann algebra modules by considering ``column sums" of noncommutative L^p spaces. Our abstract characterization is based on an L^{p/2}-valued inner product, thereby generalizing Hilbert C*-modules and representations on Hilbert space. While the (single) representation theory is similar to the L^2 case, the concept of L^p bimodule (p not 2) turns out to be nearly trivial.

This mission is the statement-level formalization of Noncommutative Lp modules (arXiv:math/0301044v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Compatible bounded operator nets have a strong limit (corrected infinite endpoint) (unnumbered-infinite-exponent-compatible-net, PDF p. 5). 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

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

• Lemma 1.1: Actual Haagerup Lp quasi-norm and strong bounded-algebra action; positive spectrum norm images (hard)
• Lemma 1.2: Normal-functional densities, supports, and quasi-norm closure of left/right Haagerup cyclic ranges (hard)
• unnumbered-polar-multiplier-spectrum: Closed strong product and polar decomposition in the actual Haagerup Lp module (hard)
• Lemma 1.3: Finite-positive-exponent Haagerup action topologies and functional density powers (hard)
• Lemma 1.4: Actual complete Haagerup quasi-Lr space and right multiplication by projections (hard)
• Theorem 1.5: Actual Haagerup Lp/Lq/Lr spaces, closed strong product, and bounded complex-linear right-module maps (hard)
• Corollary 1.6: Bounded complex-linear endomorphisms of actual quasi-Lp and both multiplication action images (hard)
• Corollary 1.7: Diffuse projection lattice and actual bounded cross-exponent right-module Hom (hard)
• Proposition 2.2: Actual L^(p/2)-valued pre-inner-product module, affiliated square roots and products (hard)
• Theorem 2.5: Actual abstract Lp modules, their inherited completions, and arbitrary-index principal column modules (hard)
• Theorem 3.1: Canonical strong/weak Hilbert-module envelopes, self-duality and arbitrary ultraweak column sums (hard)
• unnumbered-strong-hilbert-module-envelope: Canonical strong Hilbert C*-module completion, principal envelope and dense embedding (hard)
• Lemma 3.2: Faithful strictly semifinite weight densities and actual weight-bounded Lp module vectors (hard)
• Lemma 3.3: Constructed weight-bounded vector set D_phi and inherited quasi-norm topology (hard)
• unnumbered-column-sum-realization: Completion of finite-support Lp columns and convergence of their positive inner-product sums (hard)
• unnumbered-improved-module-norm: Independently defined complete Lp inner-product modules at all positive exponents (hard)
• unnumbered-orthogonal-column-complement: Lp module orthogonality, closed linear module span, and induced embedded Lp submodules (hard)
• Proposition 4.2: Banach column ultrapower, Raynaud algebra and canonical p and p/2 identifications (hard)
• unnumbered-ultrapower-column-inclusion: Canonical column ultrapower inclusion, coordinatewise projection and properness witness (hard)
• Proposition 5.1: Arbitrary-cardinal Haagerup amplified columns, corner actions and bounded commutants (hard)
• Corollary 5.2: Bounded invertible maps of actual amplified Lp modules and projection comparison (hard)
• Corollary 5.3: Rectangular Haagerup multiplier corners and all bounded cross-exponent module maps (hard)
• unnumbered-II1-module-dimension: Normalized amplified II1 trace, projection-class dimension and countable column sums (hard)
• unnumbered-module-isomorphism-monoid: Isomorphism classes of countably generated actual Lp modules and projection-class addition (hard)
• unnumbered-module-stabilization: Actual countable Haagerup columns, column sum and spatial module isomorphism (hard)
• unnumbered-contragredient-involution: Constructed left/right Lp module structures on conjugate spaces and affiliated adjoint identification (hard)
• unnumbered-relative-tensor-existence-uniqueness: A pinned functor class with sufficient enrichment/normality or sum-preservation axioms (source-ambiguity)
• Proposition 5.6: Canonical sum-preserving relative tensor product and actual rectangular Haagerup Lr corner (hard)
• Lemma 6.1: Actual faithful Lp bimodule actions and induced amplified-corner right-action embedding (hard)
• Proposition 6.3: Centers and induced action images of an actual faithful two-sided Lp bimodule (hard)
• unnumbered-scalar-module-rigidity: Actual Haagerup Lp norm and compatible scalar-valued Hilbert-module structures (hard)
• Proposition 6.6: Induced normal corner inclusion, actual row-module presentation, Murray-von Neumann subequivalence (hard)
• Proposition 6.7: Finite-algebra amplified projection strict comparison and faithful Lp bimodule presentations (hard)
• Proposition 6.8: Measurable Hilbert fields and actual Lp direct integrals with both pointwise actions (hard)
• Theorem 6.10: Independent W*-Morita equivalence and actual faithful countably generated Haagerup bimodule existence (hard)
• Theorem 6.9: Canonical common-center abelian projection, actual bimodule restrictions and variable-fiber p-direct integrals (hard)
• unnumbered-representation-category-equivalence: Canonical tensor functors on actual Lp representation categories and well-typed conjugate tensor identities (hard)

Selected references

• Noncommutative Lp modules, arXiv:math/0301044v2, https://arxiv.org/abs/math/0301044v2

Motivation

We generalize the universally composable definition of Canetti to the Quantum World. The basic idea is the same as in the classical world. The main contribution is that we unfold the result in a new model which is well adapted to quantum protocols. We also simplify some aspects of the classical case. In particular, the case of protocols with an arbitrary number of layers of sub-protocols is naturally covered in the proposed model.

This mission is the statement-level formalization of General Security Definition and Composability for Quantum & Classical Protocols (arXiv:quant-ph/0409062v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is All parity-bit biases control the Euclidean distance of string laws (§2.4, unnumbered parity bound, PDF p. 5). 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

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

• Theorem 1: both scenarios: Bound-circuit execution, security families, typed tree substitution, and uniform computational resources (hard)
• Theorem 2: Environment-indexed error and recursively constructed hybrid replacement history (hard)
• §2.4, test-string composition: Operational string-output laws with one common bounded triangle comparison (hard)
• §2.5, forwarding applications: Typed forwarding-application construction with always-active Eve (hard)
• Appendix C, equivalence: Original and alternative security with typed direct application access (hard)
• Appendix C, first step: Probe-register channel mediation and simulator transport (hard)
• Appendix C, second step: Actual Adv-P gate subdivision defining Dummy, SAdv, and Eprime (hard)
• §2.5–2.6, concrete bias; compare pp.4,16: A source-consistent bit-valued rejection rule for the CT/BC attack (source-ambiguity)
• Appendix E, proposed DAG-to-tree reorganization: A quantified persistence condition for shared functionality and a last-caller boundary in the proposed rewrite (source-ambiguity)

Selected references

• General Security Definition and Composability for Quantum & Classical Protocols, arXiv:quant-ph/0409062v2, https://arxiv.org/abs/quant-ph/0409062v2

Motivation

In the present paper we study abelian extensions of connected Lie groups $G$ modeled on locally convex spaces by smooth $G$-modules $A$. We parametrize the extension classes by a suitable cohomology group $H^2_s(G,A)$ defined by locally smooth cochains and construct an exact sequence that describes the difference between $H^2_s(G,A)$ and the corresponding continuous Lie algebra cohomology space $H^2_c(\g,\a)$. The obstructions for the integrability of a Lie algebra extensions to a Lie group extension are described in terms of period and flux homomorphisms. We also characterize the extensions with global smooth sections resp. those given by global smooth cocycles. Finally we apply the general theory to extensions of several types of diffeomorphism groups.

This mission is the statement-level formalization of Abelian extensions of infinite-dimensional Lie groups (arXiv:math/0402303v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The group defined by a normalized two-cocycle (Lemma II.1, PDF p. 7). 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

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

• Proposition I.3: ContinuousLieCochain, LieAlgebraCohomology, LieAlgebraExtensionClasses, LieAlgebraExtensionProduct, LieCochainDifferential, TopologicalLieAlgebra, TopologicalLieModule, TopologicalSplitSubspace, TopologicallySplitLieAlgebraExtension (hard)
• Lemma II.3: ExtensionEquivalence, LieGroupExtension, LieGroupMorphism, PrincipalBundle (hard)
• Proposition II.6: ExtensionClasses, LieGroupExtension, LieGroupMorphism, PrincipalBundle, StrongSmoothGroupCocycle, StrongSmoothGroupCohomology (hard)
• Lemma II.7: DifferentiationMap, InvariantVectorField, LieAlgebraExtensionProduct, LieAlgebraFunctor, TangentBundle, TangentMap (hard)
• Lemma III.1: EquivariantForm, GroupCrossedHomomorphism, LogarithmicDerivative, TangentBundle, TangentMap (hard)
• Lemma III.2: EquivariantForm, GroupCrossedHomomorphism, IdentityComponent, LogarithmicDerivative, TangentBundle, TangentMap (hard)
• Proposition III.4: ContinuousLieCochain, DerivedModule, DifferentiationMap, GroupCohomology, HomotopyGroup, LieAlgebraCohomology, LieCochainDifferential, OneCocyclePeriod, PiecewiseSmoothMap, SequentialCompleteness, TopologicalLieModule (hard)
• Remark III.5: DeRhamCohomology, DifferentialForm, ExteriorDifferential, GroupCohomology, HomotopyGroup, IntegralDeRhamClasses, LogarithmicDerivative, OneCocyclePeriod, PiecewiseSmoothMap, SequentialCompleteness, TangentBundle, TangentMap (hard)
• Lemma III.7: CharacteristicHomomorphism, DerivedModule, IdentityComponent, ModuleIsomorphism (hard)
• Lemma IV.2: CocyclePeriod, EquivariantForm, ExteriorDifferential, HomotopyGroup, PeriodGroup, PiecewiseSmoothMap, SequentialCompleteness, SurfaceIntegral (hard)
• Example IV.4: BundleConnectingHomomorphism, ExactHomotopySequence, PrincipalBundle, RelativeHomotopyGroup (hard)
• Proposition IV.5: BundleConnectingHomomorphism, CocyclePeriod, HomotopyGroup, InvariantVectorField, LieAlgebraFunctor, LieGroupExtension, LieGroupMorphism, PiecewiseSmoothMap, PrincipalBundle, SequentialCompleteness, SurfaceIntegral, TangentBundle, TangentMap (hard)
• Remark IV.6: CocyclePeriod, ExactHomotopySequence, HomotopyGroup, LieGroupExtension, LieGroupMorphism, PiecewiseSmoothMap, PrincipalBundle, SequentialCompleteness, SurfaceIntegral (hard)
• Lemma V.1: CocyclePeriod, EquivariantForm, ExteriorDifferential, HomotopyGroup, PiecewiseSmoothMap, SequentialCompleteness, SurfaceIntegral, TriangleIntegrationCocycle (hard)
• Lemma V.2: DifferentialForm, ExteriorDifferential, LocalTriangle, MixedDerivative, SequentialCompleteness, SimplexIntegral, TangentBundle (hard)
• Corollary V.3: DifferentiationMap, LocalTriangle, TriangleIntegrationCocycle (hard)
• Theorem V.4: CocyclePeriod, DifferentiationMap, GroupCohomology, HomotopyGroup, LieAlgebraExtensionProduct, LieGroupExtension, LieGroupMorphism, PeriodGroup, PiecewiseSmoothMap, PrincipalBundle, SequentialCompleteness, SurfaceIntegral (hard)
• Remark VI.1: DifferentialForm, EnlargedLieCohomology, EquivariantForm, ExteriorDifferential, InfinitesimalFluxCocycle, TangentBundle (hard)
• Lemma VI.2: EquivariantForm, ExteriorDifferential, InvariantVectorField, LieCochainDifferential, PathFlux, PiecewiseSmoothMap, SequentialCompleteness, SurfaceIntegral (hard)
• Proposition VI.3: EnlargedLieCohomology, FluxCocycle, FluxHomomorphism, HomotopyGroup, InvariantVectorField, LieGroupMorphism, PathFlux, SequentialCompleteness, UniversalCoveringGroup (hard)
• Proposition VI.4: AdjointExtensionCocycle, BundleConnectingHomomorphism, CharacteristicHomomorphism, FluxCocycle, LieGroupExtension, LieGroupMorphism, PrincipalBundle (hard)
• Corollary VI.5: AdjointExtensionCocycle, CommutatorSurfaceFormula, FluxCocycle, InvariantVectorField, LieGroupExtension, LieGroupMorphism, PathFlux, PrincipalBundle, SequentialCompleteness, SurfaceIntegral (source-ambiguity)
• VI.5-sharp: AdjointExtensionCocycle, CommutatorSurfaceFormula, InvariantVectorField, LogarithmicDerivative, PathFlux, SequentialCompleteness, SurfaceIntegral, TangentBundle, TangentMap (hard)
• Corollary VI.6: AdjointExtensionCocycle, CentralSplitting, FluxHomomorphism, HomotopyGroup, LieGroupMorphism, UniversalCoveringGroup (hard)
• Theorem VI.7: CharacteristicHomomorphism, CocyclePeriod, FluxHomomorphism, HomotopyGroup, IdentityComponent, LieAlgebraExtensionProduct, LieGroupExtension, LieGroupMorphism, PeriodGroup, PiecewiseSmoothMap, PrincipalBundle, SequentialCompleteness, SurfaceIntegral (hard)
• Remark VI.8: CentralSplitting, CommutatorSurfaceFormula, EnlargedLieCohomology, FluxHomomorphism, InvariantVectorField, PathFlux, SequentialCompleteness, SurfaceIntegral, ToroidalPeriod (hard)
• Remark VI.9: InfinitesimalFluxCocycle, LieGroupExtension, LieGroupMorphism, PrincipalBundle, QuotientModule, TriangleIntegrationCocycle (hard)
• Proposition VII.1: ExtensionEquivalence, GraphQuotientExtension, LieGroupMorphism, LocalHomomorphicSection, LocallyZeroCocycle (hard)
• Theorem VII.2: CocyclePeriod, ContinuousLieCochain, DifferentiationMap, FluxHomomorphism, GraphQuotientExtension, GroupCohomology, HomotopyGroup, InflationRestriction, LieAlgebraCohomology, LieCochainDifferential, PiecewiseSmoothMap, SequentialCompleteness, SurfaceIntegral, TopologicalLieModule (hard)
• Corollary VII.3: ContinuousLieCochain, DifferentiationMap, GroupCohomology, HomotopyGroup, LieAlgebraCohomology, LieCochainDifferential, LieGroupMorphism, TopologicalLieModule, UniversalCoveringGroup (hard)
• Proposition VIII.2: DifferentialForm, DifferentiationMap, ExactDifferentialForm, ExteriorDifferential, GloballySmoothGroupCohomology, TangentBundle (hard)
• Corollary VIII.3: ExactDifferentialForm, GloballySmoothGroupCohomology, LieAlgebraExtensionProduct (hard)
• Proposition VIII.4: ExactDifferentialForm, FluxHomomorphism, GloballySmoothGroupCohomology, SmoothParacompactness (hard)
• Remark VIII.5: DeRhamCohomology, DifferentialForm, ExteriorDifferential, GlobalSection, GloballySmoothGroupCohomology, GraphQuotientExtension, TangentBundle (hard)
• VIII.5-classification: ExtensionClasses, GlobalSection, GloballySmoothGroupCohomology (hard)
• Lemma IX.3: SmoothMapSpace, TangentBundle, TangentMap, TopologicalLieModule, VectorField (hard)
• Lemma IX.4: ContinuousLieCochain, DeRhamCohomology, DifferentialForm, ExteriorDifferential, GeometricCochainMap, LieAlgebraCohomology, LieCochainDifferential, TangentBundle, TopologicalLieModule (hard)
• Proposition IX.5: CocyclePeriod, DiffeomorphismGroup, EvaluationMap, GeometricVectorFieldCocycle, HomotopyGroup, PiecewiseSmoothMap, SequentialCompleteness, SmoothMapSpace, SphericalPeriods, SurfaceIntegral, VectorFieldBracket (hard)
• Corollary IX.6: GeometricVectorFieldCocycle, PeriodGroup, SphericalPeriods (hard)
• Example IX.7: DiffeomorphismGroup, PeriodGroup, SmoothMapSpace, SphericalPeriods, VectorFieldBracket (hard)
• Lemma IX.8: DifferentialForm, EnlargedDeRhamCohomology, ExteriorDifferential, TangentBundle, VectorFieldBracket (hard)
• IX.9-integration: EnlargedDeRhamCohomology, GeometricFluxCocycle, GroupCrossedHomomorphism, HomotopyGroup, LieGroupMorphism, LogarithmicDerivative, TangentBundle, TangentMap, UniversalCoveringGroup (hard)
• Remark IX.10: EnlargedDeRhamCohomology, GeometricFluxCocycle, LogarithmicDerivative, SymplectomorphismGroup, TangentBundle, TangentMap (hard)
• Proposition IX.11: GeometricFluxCocycle, PiecewiseSmoothMap, SurfaceIntegral (hard)
• Corollary IX.12: DeRhamCohomology, DifferentialForm, ExteriorDifferential, FluxHomomorphism, GeometricFluxCocycle, TangentBundle (hard)
• Lemma IX.13: EnlargedDeRhamCohomology, FluxCocycle, GeometricCochainMap, GeometricFluxCocycle (hard)
• Corollary IX.14: FluxHomomorphism, GeometricVectorFieldCocycle, SurfaceIntegral (hard)
• Remark IX.15: FluxHomomorphism, SphericalPeriods, ToroidalCycles (hard)
• Example IX.16: BundleAutomorphismGroup, CharacteristicHomomorphism, ConnectionForm, CurvatureForm, GaugeGroup, GeometricVectorFieldCocycle, IntegralDeRhamClasses, PrincipalBundle (hard)
• Example IX.17: CentralSplitting, FluxHomomorphism, GaugeGroup, GeometricVectorFieldCocycle, HeisenbergExtension, PrincipalBundle, Torus (hard)
• IX.17-gauge-coordinate: GaugeGroup, HeisenbergExtension, PrincipalBundle (source-ambiguity)
• Lemma X.1: CircleDiffeomorphismGroup, DensityModule, GroupCrossedHomomorphism, SmoothMapSpace, VectorFieldBracket (hard)
• Remark X.2: DensityModule, GroupCrossedHomomorphism, SmoothMapSpace, VectorFieldBracket (hard)
• Proposition X.3: CochainProducts, ContinuousLieCochain, DensityCocycles, DensityModule, LieAlgebraCohomology, LieCochainDifferential, SmoothMapSpace, TopologicalLieModule, VectorFieldBracket (hard)
• X.degree1: CochainProducts, DensityCocycles, DensityModule, DifferentiationMap, GroupCohomology, SmoothMapSpace, VectorFieldBracket (hard)
• Proposition X.4: CochainProducts, DensityCocycles, DensityModule, DifferentiationMap, GroupCohomology, SmoothMapSpace, VectorFieldBracket (hard)
• Proposition X.5: CochainProducts, DensityCocycles, DensityModule, GroupCohomology, SmoothMapSpace, VectorFieldBracket (hard)
• X.SL2-extension: CochainProducts, DensityCocycles, DensityModule, GloballySmoothGroupCohomology, LieGroupExtension, LieGroupMorphism, PrincipalBundle, SL2CircleAction, SmoothMapSpace, VectorFieldBracket (hard)
• X.SL2-topology: A consistent topology claim for the globally smooth cocycle extension F1 x_f SL2(R): the underlying manifold is F1 x SL2(R), with fundamental group Z, so the printed diffeomorphism to F1 x R^3 and consequent contractibility cannot be stated literally. (source-ambiguity)
• X.SL2-central: ContinuousLieCochain, LieAlgebraCohomology, LieCochainDifferential, LieGroupExtension, LieGroupMorphism, PrincipalBundle, SL2CircleAction, TopologicalLieModule (source-ambiguity)
• X.SL2-cohomology: ContinuousLieCochain, DensityModule, FluxHomomorphism, LieAlgebraCohomology, LieCochainDifferential, SL2CircleAction, SmoothMapSpace, TopologicalLieModule, VectorFieldBracket (hard)
• XI.general-flux: DeRhamCohomology, DifferentialForm, ExteriorDifferential, GeneralFormFlux, PiecewiseSmoothMap, SequentialCompleteness, SingularChainIntegral, TangentBundle (hard)
• Lemma XI.1: DeRhamCohomology, DifferentialForm, EvaluationMap, ExteriorDifferential, GeneralFormFlux, SequentialCompleteness, TangentBundle, VolumeForm (hard)
• Remark XI.2: EnlargedDeRhamCohomology, EvaluationMap, ExteriorDifferential, GeneralFormFlux, LiftedDiffeomorphismGroup, SequentialCompleteness, VolumeForm (hard)
• Remark XI.3: DiffeomorphismGroup, ExactDivergenceFreeFields, LichnerowiczCocycle, LieGroupExtension, LieGroupMorphism, LiftedDiffeomorphismGroup, PrincipalBundle, SmoothMapSpace, SphericalPeriods, VectorFieldBracket, VolumeForm, VolumePreservingGroup (hard)
• Proposition XI.4: DiffeomorphismGroup, ExactDivergenceFreeFields, ExteriorDifferential, GeneralFormFlux, InvariantVectorField, LieAlgebraFunctor, LiftedDiffeomorphismGroup, SequentialCompleteness, SmoothMapSpace, TangentBundle, TangentMap, VectorFieldBracket, VolumeForm, VolumePreservingGroup (hard)
• Theorem XI.5: DiffeomorphismGroup, InvariantVectorField, LichnerowiczCocycle, LieAlgebraFunctor, LieGroupExtension, LieGroupMorphism, LiftedDiffeomorphismGroup, PrincipalBundle, SmoothMapSpace, TangentBundle, TangentMap, VectorFieldBracket, VolumeForm, VolumePreservingGroup (hard)
• Remark XI.6: DiffeomorphismGroup, LichnerowiczCocycle, LiftedDiffeomorphismGroup, SmoothMapSpace, Torus, UniversalLichnerowiczCocycle, VectorFieldBracket, VolumeForm, VolumePreservingGroup (hard)
• Proposition A.6: AlexanderSpanierCohomology, AlexanderSpanierToForms, DeRhamCohomology, DifferentialForm, ExteriorDifferential, LogarithmicDerivative, TangentBundle, TangentMap (hard)
• A.6-degree1: AlexanderSpanierCohomology, AlexanderSpanierToForms, LogarithmicDerivative, TangentBundle, TangentMap (source-ambiguity)
• Lemma B.5: DifferentialForm, EquivariantForm, ExteriorDifferential, LieCochainDifferential, TangentBundle (hard)
• Theorem B.6: AlexanderSpanierToForms, ContinuousLieCochain, DifferentiationMap, GroupCohomology, HomogeneousGroupCochain, LieAlgebraCohomology, LieCochainDifferential, TopologicalLieModule (hard)
• Lemma B.7: DifferentiationMap, MixedDerivative (hard)
• Lemma C.1: A separated group-topology construction from the supplied nonempty identity filter basis F: open sets O satisfy forall g in O, exists V in F, gV subset O; F must equal the resulting identity-neighborhood basis, with continuous multiplication/inversion and uniqueness of topology under U1-U3. (hard)
• Theorem C.2: A global topology and locally convex atlas built on the given abstract group from the specified Hausdorff manifold structure on symmetric U, using L1 local multiplication, L2 inversion and L3 every local conjugation; local inclusion must be a diffeomorphism and uniqueness must mean compatible smooth structures, not equality of arbitrary ChartedSpace records. (hard)
• Remark C.3: The same constructed compatible global Lie atlas and uniqueness as C.2 from L1-L2 alone when every identity neighborhood in U generates the entire abstract group; no L3 assumption may be retained, and generation must quantify over neighborhoods in the supplied local topology. (hard)
• Lemma C.5: BanachLieSubgroup, SplitLieSubgroup (hard)
• Theorem C.6: PrincipalBundle, SplitLieSubgroup (hard)
• Lemma D.2: InflationRestriction, SplitLieSubgroup (hard)
• Lemma D.3: GroupCohomology, InflationRestriction (hard)
• Lemma D.4: GroupCochainAction, InflationRestriction (hard)
• Proposition D.6: GroupCohomology, InflationRestriction, SmoothlyInvariantCohomology (hard)
• Lemma D.7: QuotientCoefficientCochain, SmoothlyInvariantCohomology, Transgression (hard)
• Proposition D.8: InflationRestriction, QuotientCoefficientCochain, SmoothlyInvariantCohomology, Transgression (hard)
• Example D.9: GroupCohomology, HeisenbergExtension, InflationRestriction, Torus (hard)
• Remark D.10: GroupCrossedHomomorphism, QuotientCoefficientCochain, Transgression (hard)
• Example D.11: CommutatorSurfaceFormula, FluxHomomorphism, HomotopyGroup, InflationRestriction, InvariantVectorField, LieGroupMorphism, PathFlux, SequentialCompleteness, SurfaceIntegral, UniversalCoveringGroup (hard)
• Remark D.12: PullbackQuotientExtension, PrincipalBundle, QuotientCoefficientCochain, Transgression (hard)
• E.long-exact: CoefficientConnectingMap, GlobalSection, GroupCohomology, ModuleExtension (hard)
• Remark E.1: CharacteristicHomomorphism, CoefficientConnectingMap, GroupCohomology, IdentityComponent (hard)
• Lemma F.1: CochainProducts, ContinuousLieCochain, LieCochainDifferential (hard)
• F.lie-products: CochainProducts, ContinuousLieCochain, LieAlgebraCohomology, LieCochainDifferential, TopologicalLieModule (hard)
• F.group-products: CochainProducts, GroupCohomology (hard)
• Lemma F.3: CochainProducts, ContinuousLieCochain, DifferentiationMap (hard)

Selected references

• Abelian extensions of infinite-dimensional Lie groups, arXiv:math/0402303v1, https://arxiv.org/abs/math/0402303v1

Motivation

In this paper we study non-abelian extensions of a Lie group $G$ modeled on a locally convex space by a Lie group $N$. The equivalence classes of such extension are grouped into those corresponding to a class of so-called smooth outer actions $S$ of $G$ on $N$. If $S$ is given, we show that the corresponding set $\Ext(G,N)_S$ of extension classes is a principal homogeneous space of the locally smooth cohomology group $H^2_{ss}(G,Z(N))_S$. To each $S$ a locally smooth obstruction class $\chi(S)$ in a suitably defined cohomology group $H^3_{ss}(G,Z(N))_S$ is defined. It vanishes if and only if there is a corresponding extension of $G$ by $N$. A central point is that we reduce many problems concerning extensions by non-abelian groups to questions on extensions by abelian groups, which have been dealt with in previous work. An important tool is a Lie theoretic concept of a smooth crossed module $\alpha : H \to G$, which we view as a central extension of a normal subgroup of $G$.

This mission is the statement-level formalization of Non-abelian extensions of infinite-dimensional Lie groups (arXiv:math/0504295v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

1 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Normalized factor systems: group criterion, inversion and conjugation (Lemma II.7 (continues on PDF p. 16), PDF p. 15). 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

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

• Paper main result: extension torsors and obstruction: ExtensionClasses, CenterValuedCohomology, CharacteristicClass, CohomologyTorsorAction (hard)
• I.5: LocallySmoothAutomorphismMap, LieAutomorphism, OuterAutomorphism, SmoothKernel (hard)
• I.6: InitialLieSubgroup, CenterAction, SmoothGModule (hard)
• I.7: InitialLieSubgroup, TangentFunctor, SmoothExponential, AdjointFixedCenter, MackeyCompleteness (hard)
• I.8: consistent semidirect-product action and center (source-ambiguity)
• I.10: CochainGaugeAction, center-valued cochain complex, H_s^3 and H_ss^3 (hard)
• II.3: SplitLieSubgroup, PrincipalBundle, InitialLieSubgroup (hard)
• II.5: LieGroupExtension, NormalizedLocalSection, local product diffeomorphism (hard)
• II.8: CompatibleLieAtlas, LieGroupExtension, PrincipalBundle (hard)
• II.9: LocallySmoothAutomorphismMap, LocallySmoothCochain, StrongSmoothTwoCochain (hard)
• II.10: ExtensionEquivalence, locally smooth gauge transformations (hard)
• II.11: NonabelianCohomologySet, ExtensionClasses (hard)
• II.12: ExtensionClasses with fixed kernel, center-valued strong cocycles and coboundaries (hard)
• II.13: CohomologyTorsorAction on ExtensionClasses (hard)
• II.14: SmoothGModule, center-valued cohomology, abelian extension classification map (hard)
• II.15: BaerSum as smooth fiber product modulo anti-diagonal (hard)
• II.16: action-dependent H_ss^2(R^2,R), Lie differentiation and fixed-kernel fibers (hard)
• II.17: CharacteristicClass, H_ss^3/H_s^3, ExtensionClasses (hard)
• II.18: SplitExtension, liftable central-defect quotient, ConnectingMap (hard)
• II.19: locally smooth central-defect cochains, twisted S_h, connecting-class example (hard)
• II.20: smooth crossed cocycles, central cocycle class, specified semidirect extension classes (hard)
• II.21: seven natural maps of pointed cohomology sets, ConnectingMap, split fiber (hard)
• III.2: SmoothCrossedModule with split kernel/image and smooth restricted action (hard)
• III.3: cochain-valued crossed cocycle, actual central twisted extension action (hard)
• III.5: CrossedModuleData, fiber D(f), quotient-cochain cocycle action (hard)
• III.6: admissible section/lift data and actual H_s^3/H_ss^3 obstruction (hard)
• III.7: CrossedModuleData groups and computed obstruction homomorphisms Q,Q_ss (hard)
• III.8: smooth crossed-module extension embedding and cocycle extension condition (hard)
• III.9: connected-group local obstruction with strong output extension (hard)
• IV.1: constructed reduced extension G^S, rho, alpha and their smooth structures (hard)
• IV.2: constructed ReducedExtensionGroup and smooth automorphism group without topology (hard)
• IV.3: AbelianReductionMap with actual quotient and equivariant image characterization (hard)
• IV.4: reduced crossed-module embedding obstruction and extension existence criterion (hard)
• A.1: AutomorphismPairAction on strong factor systems, semidirect gauge action, ExtensionTwist (hard)
• A.2: ExtensionAutomorphismMap Phi, cocycle-kernel homomorphism Psi (hard)
• A.3: ExtensionTwist, Phi image and explicit lift parametrization (hard)
• A.4: abelian smooth extension automorphism lift and exact-sequence maps (hard)
• A.5: smooth extension automorphism lift of (S(g),c_g) (hard)
• A.6: smooth factor-system automorphism action and gauge cochain (hard)
• A.7: GaugeCocycleMonoid units, gauge group, compatible-pair and torsor actions (hard)
• A.8: basepoint-dependent AutomorphismObstruction and central cocycle ratio (hard)
• A.9: pointed exactness of Phi followed by the computed crossed cocycle I (hard)
• A.11: abstract H-action on locally smooth cochains and explicit automorphism lifts (hard)
• A.12: pullback abelian extension and abstract H^2 action-lift obstruction (hard)
• A.13: locally glued extension atlas, evaluation and orbit-map smoothness (hard)
• A.4-exact-sequence (unnumbered): actual smooth automorphism kernel, extension stabilizer and short exact sequence (hard)

Selected references

• Non-abelian extensions of infinite-dimensional Lie groups, arXiv:math/0504295v1, https://arxiv.org/abs/math/0504295v1

Motivation

We study the twisted Weyl symbol of metaplectic operators; this requires the definition of an index for symplectic paths related to the Conley-Zehnder index. We thereafter define a metaplectically covariant algebra of pseudo-differential operators acting on functions on symplectic space.

This mission is the statement-level formalization of A Weyl Calculus on Symplectic Phase Space (arXiv:math-ph/0508024v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

9 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Symplectic Cayley bijection, product and inverse (Lemma 6: symplectic Cayley bijection, product and inverse, PDF p. 14). 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

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

• Proposition 20 (94), paper capstone: metaplectic covariance of the phase-space Weyl calculus: Independent concrete Mp action and full tempered phase-space Weyl calculus (hard)
• Unnumbered assertion after (39): integrality at arbitrary endpoints: Independently moderated correction or precise domain for Unnumbered assertion after (39): integrality at arbitrary endpoints (source-ambiguity)
• ν.1: inverse antisymmetry: Universal real symplectic/Lagrangian covers and concrete half-ALM graph index (hard)
• ν.2: action of the fundamental-group generator: Action-normalized deck generator for the concrete half-ALM graph index (hard)
• ν.3 (40): product formula for the graph index: Concrete ALM graph index and actual symmetric-matrix signature (hard)
• ν.4: constancy under paths avoiding fixed points: Lifted-path concatenation and concrete graph index (hard)
• Lemma 7 (42), including its invertibility continuation: Independently moderated correction or precise domain for Lemma 7 (42), including its invertibility continuation (source-ambiguity)
• Proposition 8 (43): graph index and relative Maslov index: Relative Maslov index and half-ALM graph index on actual covers (hard)
• Proposition 9 (49): weak Weyl form of Rν(S): Continuous Schwartz-to-tempered MW map from weak Weyl pairings (hard)
• Unnumbered (51): ordinary Weyl symbol of Rν(S): Independently moderated correction or precise domain for Unnumbered (51): ordinary Weyl symbol of Rν(S) (source-ambiguity)
• Proposition 10 (52)–(53): composition and inverse: Schwartz-preserving realization and composition of the concrete MW map (hard)
• Corollary 11: unitarity of Rν(S): Unitary L2 extension of the weak Gaussian MW map (hard)
• Unnumbered after (56): well-defined index of an actual Mp lift: Actual Mp group and lift-specific mod-four half-ALM index (hard)
• Proposition 12 (61)–(62): exact free-lift phase and determinant sign: Actual Mp lift index and weak MW/quadratic-generator comparison (hard)
• Corollary 13 (65): two nonfixed free MW factors generate Mp: Independently generated concrete Mp subgroup and admissible nonfixed MW elements (hard)
• Proposition 14 (67): MW form and composition phase for a nonfixed lift: Actual Mp projection, weak MW map and mod-four index of its lifts (hard)
• Proposition 15 (73)–(74): isometry, closed range, projection and covariance: Concrete metaplectic action on complex Schwartz windows and covariance of U_phi (hard)
• Example 16 (79): Gaussian range characterization: Independently moderated correction or precise domain for Example 16 (79): Gaussian range characterization (source-ambiguity)
• Proposition 18 (89)–(90), full printed statement: Independently moderated correction or precise domain for Proposition 18 (89)–(90), full printed statement (source-ambiguity)
• Proposition 18(ii) (90): general Weyl intertwining: Tempered-symbol Weyl maps and the canonical distributional U_phi extension (hard)
• Proposition 19: composition and twisted convolution: Independently moderated correction or precise domain for Proposition 19: composition and twisted convolution (source-ambiguity)
• Proposition 21: uniqueness from unitality and metaplectic covariance: Independently moderated correction or precise domain for Proposition 21: uniqueness from unitality and metaplectic covariance (source-ambiguity)
• Unnumbered after Proposition 21: the unit symbol gives identity: Normalized symplectic Fourier transform and Weyl quantization on tempered distributions (hard)

Selected references

• A Weyl Calculus on Symplectic Phase Space, arXiv:math-ph/0508024v2, https://arxiv.org/abs/math-ph/0508024v2

Motivation

This paper attempts to give an overview about sufficiency in the setting of quantum statistics. The basic concepts are treated paralelly to the the measure theoretic case. It turns out that several classical examples and results have a non-commutative analogue. Some of the results are presented without proof (but with exact references) and the presentation is intended to be self-contained. The main examples discussed in the paper are related the Weyl algebra and to the exponential family of states. The characterization of sufficiency in terms of quantum Fisher information is a new result.

This mission is the statement-level formalization of Sufficiency in quantum statistical inference. A survey with examples (arXiv:quant-ph/0604091v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

7 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is The Bernoulli sample mean is sufficient (Introduction: Bernoulli sample mean is sufficient, PDF p. 2). 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

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

• Theorem 5: Fisher information and sufficiency (original seed; printed global equivalence): Theorem 5: Fisher information and sufficiency (original seed; printed global equivalence) (source-ambiguity)
• Example 2: quantum sample-mean coarse-graining: Infinite tensor-product C-star algebra and its canonical shift (hard)
• Example 3: printed likelihood-ratio minimality: Example 3: printed likelihood-ratio minimality (source-ambiguity)
• Proposition 3: factorization criterion as printed: Proposition 3: factorization criterion as printed (source-ambiguity)
• Example 5: sufficient Gaussian quantum sample-mean map: Universal CCR algebra, quasifree states, and the quasifree recovery map (hard)
• Example 7: Gaussian shift modular group and cocycle: Gaussian GNS closure, modular flow and actual Connes cocycles (hard)
• Example 7: minimal sufficient Gaussian shift algebra: Generated Gaussian von Neumann subalgebra and minimal recovery comparison (hard)
• Theorem 1: five sufficient-subalgebra criteria: Relative modular operators, alpha quasi-entropies, cocycles and generalized expectation (hard)
• Fixed point algebras of the reference dual: Reference dual of a normal 2-positive map and modular intertwining (hard)
• Theorem 2: six sufficient-coarse-graining criteria: Reference dual, quasi-entropies and generated von Neumann images (hard)
• Noncommuting families admit no sufficient measurement: Noncommuting families admit no sufficient measurement (source-ambiguity)
• Proposition 4: finite relative-entropy preservation: General Araki relative entropy for normal states (hard)
• Support-corner reduction for nonfaithful references: Support projections, genuine corner algebras and normal 2-positive compressions (hard)
• Perturbed state: attained variational minimum and support: Normalized modular perturbation and attained Araki variational minimum (hard)
• Equation (15): finite-dimensional Gibbs formula: Variationally defined perturbed state on all finite-dimensional unital algebras (hard)
• Equation (16): normalized modular perturbation vector: Unbounded modular logarithm and exponential vector with domain control (hard)
• Theorem 3: perturbed-state sufficiency, modular orbits and fixed generators: Actual perturbed state, cocycle, modular group and generalized expectation (hard)
• Corollary 1: printed parameter-domain sufficiency equivalence: Corollary 1: printed parameter-domain sufficiency equivalence (source-ambiguity)
• Corollary 1: corrected full-real-parameter equivalence: Full real exponential experiment and reference-preserving finite comparison family (hard)
• Variational potential: analyticity, concavity and derivative: Actual variational potential on the self-adjoint Banach space (hard)
• Canonical correlation: positivity, monotonicity, scalar invariance and kernel: Bogoliubov Hessian of the actual perturbation potential (hard)
• Uniformly dominated states admit bounded potentials: State-to-bounded-potential existence under uniform order domination (hard)
• Theorem 4: compatible perturbation lifts characterize sufficiency: Compatible normalized perturbations for original and induced experiments (hard)
• Exponential-family transport under sufficient coarse-graining: Full-real exponential perturbation transport across a sufficient map (hard)
• Fisher tensor and corrected derivative identities: Smooth state-induced Bogoliubov Fisher tensor and centered scores (hard)
• Theorem 5: Fisher information monotonicity: Original and induced Bogoliubov Fisher matrices (hard)
• Theorem 5: corrected connected-model equivalence: Canonical differentiable induced potentials and connected-model Fisher equality (hard)
• Theorem 6: modular factorization criterion: Compatible spatial derivatives for weights on the common Hilbert space (hard)
• Semifinite relative-commutant modular factor: Affiliated modular operator and relative-commutant dynamics (hard)
• Finite entropy forces countable type-I decomposition: C-star state entropy and countable type-I algebra decompositions (hard)
• Equation (20): parameter-independent density factorization: Canonical affiliated density factors in countable type-I blocks (hard)
• Equation (21): block tensor density factorization: Countable tensor-block decomposition with trace-norm summation (hard)
• Minimal sufficient algebra generated by cocycles: Cocycle-generated von Neumann algebra and maximal density factorization (hard)
• Example 8: sufficient pure-state block structure: Finite block-subalgebra inclusions and common pure right-factor recovery (hard)
• Example 9: permutation block factorization of tensor powers: Schur block-algebra identification, normalized marginals and permutation irreps (hard)

Selected references

• Sufficiency in quantum statistical inference. A survey with examples, arXiv:quant-ph/0604091v1, https://arxiv.org/abs/quant-ph/0604091v1

Motivation

We show that the eigenvalues and eigenfunctions of the stargenvalue equation can be completely expressed in terms of the corresponding eigenvalue problem for the quantum Hamiltonian. Our method makes use of a Weyl-type representation of the star-product and of the properties of the cross-Wigner transform, which appears as an intertwining operator.

This mission is the statement-level formalization of A new approach to the star-genvalue equation (arXiv:0808.0489v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Phase displacement multiplication and commutation (§3, (10)–(11), PDF p. 5). 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

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

• Theorem 4 with Remark 5: A generic tempered symbol only supplies an S-to-Sprime operator, not a domain on the arbitrary L2 eigenvectors in Theorem 4; the fixed-window reverse clause also lacks a nonzero guard. (source-ambiguity)
• §2, (2)–(6): Independent tempered-symbol oscillatory Moyal multiplication and Weyl quantization of the surjective pullback symbol H(x−ζp/2,p+ζx/2). (hard)
• §3, (7)–(9): Weak distributional superposition of phase displacements against the symplectic Fourier transform of a generic tempered symbol. (hard)
• Proposition 2, (15)–(16): Window and adjoint extensions to tempered distributions, together with generic S-to-Sprime Weyl and independent star actions. (hard)
• Corollary 6, (17): False double range membership, missing completeness assumption, and missing generic operator domains. (source-ambiguity)
• §4, H(x,p)=p: Tempered tensor lift of an arbitrary one-variable distribution and multiplication by the quadratic chirp exp(2i(E−p)x/hbar). (hard)
• §4, H(x,p)=x: Tempered tensor lift Phi_x tensor 1_p and multiplication by exp(−2i(E−x)p/hbar), alongside the maximal configuration multiplication graph. (hard)
• §5, (20): Incompatible two-index labels in the displayed Laguerre formula and its conjugate companion. (source-ambiguity)
• §5, metaplectic transport: Inconsistent Williamson inverse and interchange of original and reduced eigenfunction families. (source-ambiguity)
• §6, explicitly stated conjecture: An explicitly unproved conjecture, with no pinned general symplectic capacity or operator domain. (source-ambiguity)

Selected references

• A new approach to the star-genvalue equation, arXiv:0808.0489v1, https://arxiv.org/abs/0808.0489v1

Motivation

Work of Clifford, Munn and Ponizovski{\u\i} parameterized the irreducible representations of a finite semigroup in terms of the irreducible representations of its maximal subgroups. Explicit constructions of the irreducible representations were later obtained independently by Rhodes and Zalcstein and by Lallement and Petrich. All of these approaches make use of Rees's theorem characterizing 0-simple semigroups up to isomorphism. Here we provide a short modern proof of the Clifford-Munn-Ponizovski{\u\i} result based on a lemma of J. A. Green, which allows us to circumvent the theory of 0-simple semigroups. A novelty of this approach is that it works over any base ring.

This mission is the statement-level formalization of On the irreducible representations of a finite semigroup (arXiv:0712.2076v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Every simple semigroup module has an apex (Theorem 5, PDF p. 3). 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

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

• Theorem 7: Full Clifford–Munn–Ponizovskii correspondence, all three clauses and final field classification (hard)
• Lemma 6: Corner restriction and simple-class correspondence with actual induced quotient and coinduced socle (hard)
• Restriction, induction, and coinduction paragraph: Actual module functors, adjunctions, exactness and natural corner isomorphisms (hard)
• Apex characterization and A_J paragraph: Full apex characterization together with quotient-module category identification (hard)
• Induced Schutzenberger paragraph: Free Schutzenberger bimodule realization, exactness, changed-idempotent transport and endomorphism comparison (hard)
• Rees and sandwich-matrix comparison, pp. 6–7: Coordinate comparison of induced quotient and coinduced socle via the sandwich matrix (hard)
• Coinduced Schutzenberger paragraph, pp. 6–7: Right-equivariant function realization and exactness of Coind (hard)

Selected references

• On the irreducible representations of a finite semigroup, arXiv:0712.2076v2, https://arxiv.org/abs/0712.2076v2

Motivation

We present a general dilation scheme for quantum instruments with continuous outcome space in finite dimensions, in terms of an indirect POVM measurement performed on a finite dimensional ancilla. The general result is then applied to a large class of instruments generated by operator frames, which contains group-covariant instruments as a particular case, and allows to construct dilation schemes based on a measurement on the ancilla followed by a conditional feed-forward operation on the output. In the case of tight operator frames our construction generalizes quantum teleportation and telecloning, producing a whole family of generalized teleportation schemes in which the instrument is realized via a joint POVM at the sender combined with a conditional feed-forward operation at the receiver.

This mission is the statement-level formalization of Realization schemes for quantum instruments in finite dimensions (arXiv:0810.3211v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

2 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Equivalent left-tight frame identities (Definition 4 and Eq.(85), PDF p. 17). 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

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

• Theorem 1: minimal finite-dimensional indirect-POVM instrument dilation: Actual conjugate-support ancillary Hilbert space, kernel-zero powers, and a general event-valued CP instrument dilation (hard)
• Proposition 1: two explicit minimal Stinespring formulas: The two canonical CJ-square-root maps into the actual conjugate support and universal Stinespring minimality (hard)
• Proposition 2: finite trace-measure density of every instrument: Event-valued countably additive complex-linear CP instrument and its constructed finite CJ trace measure (hard)
• §3, Eq.(44): every dilation is an isometric extension with compressed POVM: Canonical minimal triple and isometric comparison of actual ancillary Hilbert spaces (hard)
• Lemma 1: normalization criterion and converse for frame-orbit instruments: General frame-orbit instrument with measurable integrable CP-map density and a constructed converse seed (hard)
• §4.1, Eqs.(49)–(51): the two canonical POVM densities: Canonical probability POVM and minimal support-valued ancillary POVM with explicit a.e. densities (hard)
• Corollary 1: minimal feed-forward realization: Computed pre-feed-forward instrument, its actual supported dilation and fixed-channel minimum (hard)
• §5, Eqs.(57)–(59): covariant instruments are frame-orbit instruments: Compact projective unitary actions, quotient measurable sections and general covariant instrument densities (hard)
• §5.1.1, Eqs.(61)–(65): covariant minimal POVM and intertwiner: Covariant action on the actual conjugate support with the canonical minimal instrument dilation (hard)
• §5.1.2, Eqs.(66)–(69): covariant feed-forward and irreducible teleportation: The invalid quotient-to-group twirl replacement in Eq.(66) (source-ambiguity)
• Proposition 3: representation-theoretic nonminimal feed-forward dilation: Projective irreducible direct sums and integrated physical group-outcome feed-forward dilation (hard)
• §5.1.4, Eqs.(80)–(82): explicit L²(G) Naimark compression: Actual L2(G,dg) coefficient embedding, indicator multiplication PVM and adjoint compression (hard)
• §6.1, Eqs.(86)–(89): minimal pure-resource tele-instrument: Supported Moore–Penrose pure-resource joint POVM and fixed-feed-forward minimality (hard)
• §6.2, Eqs.(90)–(92): mixed-resource rank-one-POVM tele-instrument: Kernel-zero inverse square root and support-restricted rank-at-most-one joint POVM (hard)
• §6.3, Eqs.(93)–(94): unitary-frame Bell and minimal realizations: General frame-orbit CP seed and canonical singular pure-resource realization (hard)
• §7, Eqs.(96)–(97): two generalized-teleportation realizations of covariant channels: Both physical covariant-channel realizations, singular output purification and local equivalence for rank-one CJ (hard)
• §7.0.2, Eqs.(100)–(102): two universal tele-cloning realizations: Occupation-basis symmetric Hilbert spaces, cloning CP map, tensor-power group actions and both resources (hard)
• §7.0.3, Eq.(104): universal-NOT measure-and-prepare and Bell realizations: Symmetric N-qubit input, SU(2) orbit measurement, single-qubit preparation and Bell-resource processing (hard)

Selected references

• Realization schemes for quantum instruments in finite dimensions, arXiv:0810.3211v4, https://arxiv.org/abs/0810.3211v4

Motivation

We study analogues of Jucys-Murphy elements in cellular algebras arising from repeated Jones basic constructions. Examples include Brauer and BMW algebras and their cyclotomic analogues.

This mission is the statement-level formalization of On Cellular Algebras with Jucys Murphy Elements (arXiv:0907.3459v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 6.10 (see [4], Lemma 2.3) — degenerate affine skein power identity (Lemma 6.10 (see [4], Lemma 2.3), PDF p. 24). 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

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

• Lemma 2.3 — globalizing arbitrary cell-module bases: CellModule, involution-twisted right module, cell-layer bimodule quotient, and compatible tensor-layer equivalence (hard)
• Lemma 2.9 ([17], Lemma 2.20) — simple modules and filtration multiplicities: Coherent cellular tower, scalar-extended cell modules, cell filtrations and actual inclusion multiplicities (hard)
• Corollary 2.10 — independence and Frobenius reciprocity of cell-filtration multiplicities: Filtrations of the actual induction and restriction modules and their cell-isomorphism counts (hard)
• Corollary 2.12 — strong coherence implies multiplicity-free generic branching: Strong coherence and the actual generic inclusion matrices (hard)
• Proposition 2.18 — restriction rule for the constructed path bases: Inductively constructed path bases, actual branching paths, restriction coefficients and higher-tail spans (hard)
• Corollary 2.19 — restriction rule for globalized cellular path bases: Globalizations of constructed path bases and their cell-ideal quotient action (hard)
• Proposition 3.6 — multiplicative JM triangularity and central product: Multiplicative JM family, scalar actions on constructed cell modules and path-basis triangularity (hard)
• Proposition 3.7 — additive JM triangularity and central sum: Additive JM family and the constructed path-basis action (hard)
• Lemma 3.10 — characterization of Gelfand–Zeitlin idempotents: Finite split semisimple tower, actual branching paths, primitive central idempotents and canonical GZ products (hard)
• Proposition 3.11 — separating JM elements generate the GZ algebra: Scalar-extended separated JM family and the actual GZ subalgebra (hard)
• Theorem 4.1 ([17], Theorem 3.2) — cellularity from basic constructions: All-eight-axiom basic-construction tower and its constructed cellular structure, cell modules and reflected branching diagram (hard)
• Theorem 5.1 — lifting multiplicative JM families (paper headline): Strong-framework pair, quotient maps, multiplicative JM predicates and resulting A-cell structure (hard)
• Corollary 5.2 — constant multiplicative lifting factor: Basic-construction labels and uniquely determined product-action scalars (hard)
• Theorem 5.3 — lifting additive JM families: Strong-framework pair, additive JM predicates and the basic-construction cell action (hard)
• Lemma 6.14 — generic injectivity of multiplication by e_n: Concrete universal admissible integer-polynomial omega sequence and canonical cyclotomic level map (hard)
• Proposition 6.16 — degenerate cyclotomic BMW strong framework: Specific generic admissible degenerate tower, Hecke quotient and full strong framework predicate (hard)
• Corollary 6.17 — strong coherence and path-labelled cells for admissible degenerate cyclotomic BMW algebras: Admissibility as freeness of W_2 e_1 and a strongly coherent multipartition-labelled cellular tower (hard)
• Proposition 6.18 — explicit Temperley–Lieb cell ideals: Temperley--Lieb presentation, specialized basic-construction cellular datum and its named cell ideals (hard)
• Lemma 6.20 — the Hecke quotient is the Temperley–Lieb algebra: Generic Hecke Murphy cell ideal and concrete Temperley--Lieb algebra over the enlarged ring (hard)
• §2.7, unnumbered — existence of path bases and their globalizations: Coherent family of actual restriction-filtration lifts and cell-layer globalizations (hard)
• §5, unnumbered — general multiplicative scalar formula: Lifted product action on basic-construction cell modules with alternating gamma indices (hard)
• §5, unnumbered — additive scalar formula and constant-factor specialization: Lifted additive action on basic-construction cell modules and its scalar (hard)
• §6.2, unnumbered — strongly coherent BMW cellular tower: Generic BMW presentation ring and constructed strongly coherent Young-diagram cellular datum (hard)
• §6.2, unnumbered / (6.1) — BMW JM family and eigenvalues: Concrete BMW recursive L elements and their action on constructed up-down cell bases (hard)
• §6.3, unnumbered — strongly coherent Brauer cellular tower: Brauer diagram algebra with loop-count multiplication and its constructed strongly coherent cell datum (hard)
• §6.3, unnumbered / (6.2) — unshifted Brauer JM family and eigenvalues: Concrete unshifted Brauer recursion and its actual up-down cell-module action (hard)
• §6.4.5, unnumbered — cyclotomic BMW cellular tower: Universal admissible nondegenerate coefficient ring and concrete cyclotomic BMW cellular tower (hard)
• §6.4.6, unnumbered / (6.4) — cyclotomic BMW JM family: Concrete universal-admissible cyclotomic BMW tower, y_1 recursion and up-down cell action (hard)
• §6.5.6, unnumbered / (6.7) — degenerate cyclotomic BMW additive JM family: Specific generic degenerate coefficient polynomials and constructed cell action of x_j (hard)
• §6.6, unnumbered — Temperley–Lieb cellular tower and label order: Generic Temperley--Lieb presentation with specific reversed cell order and strong filtrations (hard)
• §6.6, unnumbered — comparison of the two Temperley–Lieb cellular structures: Both actual Temperley--Lieb cellular structures, Hecke quotient map and cell-module comparison (hard)
• §6.6, unnumbered — Temperley–Lieb JM triangularity, product scalar and local relation: Concrete Hecke-derived Temperley--Lieb L sequence and both identified cell structures (hard)
• Example 3.1 / (3.1) — classical Hecke JM properties (background): Hecke presentation and literal Murphy cell modules and bases (hard)
• §6.3, unnumbered — symmetric-group additive JM family (background): Actual symmetric group algebra, additive JM recursion and q=1 Murphy cell-module specialization (hard)
• §6.4.6 / (6.3), unnumbered — cyclotomic Hecke multiplicative JM family (background): Cyclotomic Hecke presentation in the corrected quadratic convention and actual Murphy-type modules (hard)
• §6.5.6 / (6.6), unnumbered — degenerate cyclotomic Hecke additive JM family (background): Degenerate cyclotomic Hecke quotient and its literal Murphy-type cellular tower and basis action (hard)
• §3.1.1, unnumbered — maximal abelian GZ algebra and canonical idempotents: Actual multiplicity-free split semisimple tower, canonical central projectors and generated GZ algebra (hard)

Selected references

• On Cellular Algebras with Jucys Murphy Elements, arXiv:0907.3459v2, https://arxiv.org/abs/0907.3459v2