All missions

Motivation

Corporate law and contract design decide who controls a firm's decisions. A manager may hold undivided control, the unfettered right to implement a project, or control may be shared, with a stakeholder (a creditor, an employee group, a minority shareholder) holding a contractual veto. The trade-off is old: veto rights protect stakeholders from value-destroying decisions, but they create a bargaining problem when the stakeholder is less informed than the manager, because negotiations under asymmetric information can break down and block valuable projects.

E. M. Meyersson Milgrom, P. Milgrom and R. Singh, When Should Control Be Shared? (Management Science, 2023, doi:10.1287/mnsc.2022.4356), study this trade-off in a two-party model and add a legal dimension: rules that forbid extortionate transfers (duties of loyalty, good faith and fair dealing). Their headline comparative static is that, once such limits on transfers accompany undivided control, a better-informed stakeholder helps only the shared-control structure. Shared control is then more attractive the more symmetrically informed the parties are, which is the opposite of what happens without the legal limits (their Proposition 3).

Setting

A firm has a manager, who generates a proposal, and a stakeholder. With probability $q \in [0,1]$ the state is good, otherwise bad. The project moves a random amount $r$ of wealth from the stakeholder to the manager; in state $i \in \{g, b\}$ the payoffs are

$$m_i = \pi_i + r, \qquad s_i = \pi_i - r, \qquad \pi_g > 0 \ge \pi_b .$$

The redistribution $r$ has a continuous distribution with support $[r_l, r_h]$, $0 \le r_l < r_h < \infty$, and mean $\bar r$. The manager observes $r$; the stakeholder observes it only with probability $z \in [0,1]$.

The manager makes a take-it-or-leave-it offer of a transfer $t$. Under shared control, an uninformed stakeholder facing an offer that is made exactly when $m_g \ge t$ accepts if

$$E[s_g + t \mid m_g \ge t] \ge 0, \tag{1}$$

and the equilibrium transfer $t_s$ is the smallest nonnegative $t$ satisfying (1). With $P_s = \Pr[m_g \ge t_s]$, the joint expected surplus of shared control is

$$S(z) = q\,[z + (1 - z)P_s]\,2\pi_g. \tag{3}$$

Under undivided control with transfers disallowed, the manager implements a proposal whenever $m_i \ge 0$, and the joint expected surplus is

$$\tilde U = 2\,[q\pi_g + (1 - q)\Pr[m_b \ge 0]\,\pi_b]. \tag{7}$$

Formalization targets

Goal: Proposition 8

For every model satisfying the standing assumptions,

$$S \text{ is nondecreasing on } [0,1], \qquad S \text{ is strictly increasing on } [0,1] \iff q > 0 \text{ and } \bar r - r_l > 2\pi_g,$$ $$\tilde U(z) = \tilde U(z') \text{ for all } z, z', \qquad \tilde U - S \text{ is nonincreasing on } [0,1].$$

The paper's "corresponding increase in the benefit of shared control" is read as weak monotonicity together with the exact condition for strictness: when good proposals are never blocked ($P_s = 1$), $S$ is constant in $z$.

Milestones

1. The equilibrium transfer exists (§2.1): the infimum $t_s$ of the transfers satisfying (1) satisfies (1), and either $t_s = 0$ or (1) holds with equality at $t_s$.
2. Full acceptance (proof of Proposition 1): $\Pr[m_g \ge t] = 1 \iff t \le \pi_g + r_l$ for every threshold $t$.
3. The threshold (proof of Proposition 1): $t_s \le \pi_g + r_l \iff \bar r - r_l \le 2\pi_g$.
4. Proposition 1: under shared control no transfer makes a bad proposal profitable for the manager and acceptable to the stakeholder, and $P_s = 1 \iff \bar r - r_l \le 2\pi_g$.

Significance

Proposition 8 is the result behind the paper's abstract claim that with legal protections against extortion, "but not without them", shared control is more likely when the parties are more symmetrically informed. It turns the informational environment into a determinant of the optimal control structure: improving the stakeholder's information (disclosure duties, audit rights, board observers) raises the value of a veto right and leaves undivided control unaffected. Proposition 1, the main intermediate step, gives the exact condition $\bar r - r_l \le 2\pi_g$ under which shared control loses nothing to bargaining failure.

The results are proved in the paper, in prose. Nothing of this model is formalized. A machine-checked version adds an explicit account of the equilibrium transfer, which the paper defines as "the smallest nonnegative transfer that satisfies Inequality (1)" without proving that the set has a least element, and it fixes the exact sense in which the increase in Proposition 8 holds: weak in general, strict exactly when $q > 0$ and $\bar r - r_l > 2\pi_g$.

Difficulty

Once Proposition 1 is available, the goal is close to algebra: $S$ is affine in $z$ with slope $2q\pi_g(1 - P_s) \ge 0$, and $\tilde U$ does not involve $z$. The work lies in the equilibrium transfer. The left-hand side of (1) is a conditional expectation over an event that moves with $t$, so continuity in $t$ needs the atomlessness of the law of $r$, and attainment of the infimum needs the conditioning event to keep positive probability up to $\pi_g + r_h$. The strictness criterion then needs both directions of Proposition 1, and the "only if" direction uses that $r_l$ is the minimum of the support, not just a lower bound: below $t_s - \pi_g$ there must be probability mass for the good proposal to be blocked.

Formalization scope

The model is a structure SharedControl.Model (probability measure P on Ω, redistribution r : Ω → ℝ, parameters πg, πb, q, rl, rh) with a separate predicate SharedControl.Standing: P a probability measure, r measurable, the law of r atomless (NullSingletonClass), r ∈ [rl, rh] almost surely, rl and rh the essential infimum and supremum, $\pi_g > 0$, $\pi_b \le 0$, $0 \le q \le 1$, $0 \le r_l < r_h$. No density is assumed. $E[\cdot \mid A]$ is the integral against Mathlib's conditional measure P[|A]; a transfer satisfies (1) only if $\Pr[m_g \ge t] > 0$, since the conditional measure of a null event is zero and would make every large transfer acceptable by a junk value. The equilibrium transfer ts is the sInf of the feasible set, and the goal is stated for this defined ts, not for a free variable with an IsLeast hypothesis. Probabilities are real numbers (P.real). S and Utilde are functions of $z \in \mathbb R$, the latter ignoring its argument; monotonicity is on $[0,1]$.

The statement is not trivialized: clause 3 holds by the definition of (7) because that is the paper's claim about undivided control, but clauses 1 and 2 depend on ts being a genuine least element and on both directions of Proposition 1.

A complete development needs continuity of conditional expectations over moving tail events for atomless laws, which is reusable beyond this mission. Proofs of the milestones in any order, and alternative arguments, are welcome.

Selected references

• E. M. Meyersson Milgrom, P. Milgrom, R. Singh, When Should Control Be Shared?, Management Science, 2023 (Articles in Advance, 2022). https://doi.org/10.1287/mnsc.2022.4356
• O. Hart, J. Moore, Property Rights and the Nature of the Firm, Journal of Political Economy 98(6), 1990. https://doi.org/10.1086/261729
• P. Aghion, P. Bolton, An Incomplete Contracts Approach to Financial Contracting, Review of Economic Studies 59(3), 1992. https://doi.org/10.2307/2297991

Motivation

Network revenue management asks how a seller with a fixed stock of several perishable resources (seats on the legs of an airline network, hotel room-nights, rental-car days) should accept or reject requests for products that each consume a bundle of those resources, when requests arrive randomly over a finite selling horizon. The exact optimal policy is the solution of a dynamic program whose state is the whole remaining capacity vector, together with whatever history the arrival process makes relevant, and it is rarely computable at the scale of an airline network. In practice the industry uses simple controls derived from a single deterministic linear program in which random demand is replaced by its mean: the optimal LP solution is read as a vector of booking limits, one per product.

Cooper (Operations Research 50(4):720–727, 2002) asks when this practice is justified. The paper's answer is an asymptotic one: if capacity and expected demand are scaled up together, the LP allocation policy earns, in distribution and in expectation, a fraction of the optimal expected revenue that tends to one.

Timeline. Gallego and van Ryzin (Management Science 40(8), 1994) proved asymptotic optimality of fixed-price heuristics in single-product dynamic pricing, and (Operations Research 45(1), 1997) the analogous result for network pricing under Poisson demand, in expectation. Talluri and van Ryzin (Management Science 44(11), 1998) proved asymptotic optimality in expectation of bid-price controls. Cooper (2002) isolates a single condition on the arrival process, a law of large numbers for the total demand of each class, and from it obtains convergence in distribution of the normalized revenue for general simple point-process arrivals, with no Poisson or Markov assumption, against the optimum over all history-dependent policies. The same paper shows by example that re-solving the LP during the horizon can lower expected revenue; that example is not part of this mission.

Setting

There are $m$ resources and $n$ products. Resource $i$ has initial capacity $c_i>0$; a class-$j$ customer requests product $j$, consumes $a_{ij}\ge 0$ units of resource $i$ and pays the fare $f_j$. Write $A=(a_{ij})$ and $f=(f_j)$. Requests arrive one at a time over the horizon $(0,\tau]$, $\tau>0$: $D_j(t)$ is the number of class-$j$ requests in $(0,t]$, the paths have finitely many arrivals almost surely, and at most one request (of any class) arrives at any instant.

A policy $\pi\in\Pi$ maps, for each time $t$, the history of the arrival process up to and including $t$ to a vector in $\{0,1\}^n$: a one in position $j$ means a class-$j$ request arriving at $t$ is accepted. Under $\pi$ the number of accepted class-$j$ customers is

$$N^\pi_j=\int_{(0,\tau]}\pi_j(s)\,D_j(ds),$$

and the revenue is $R^\pi=f\cdot N^\pi$. The optimal value is

$$v=\sup_{\pi\in\Pi}\bigl\{E(f\cdot N^\pi):AN^\pi\le c,\ 0\le N^\pi\le D(\tau)\bigr\},$$

with the constraints required almost surely. With $\mu=ED(\tau)$, the linear program is

$$\max_x\{f\cdot x: Ax\le c,\ 0\le x\le\mu\},$$

with an optimal solution $x^*$ and optimal value $\beta=f\cdot x^*$. The LP allocation policy is $\pi^{LP}_j(t)=1\bigl(D_j(t)\le x^*_j\bigr)$, where $D_j(t)$ counts an arrival at time $t$ itself: it accepts the first $\lfloor x^*_j\rfloor$ class-$j$ requests.

The scaled problems are indexed by $k=1,2,\dots$: problem $k$ has capacity $kc$ and its own arrival process $D^{(k)}$ with the same two path properties and $ED^{(k)}(\tau)=k\mu$. Its value is $v^{(k)}$, the LP policy uses the allocation $kx^*$, and $R^{LP(k)}$ is its revenue. The standing condition is

$$k^{-1}D^{(k)}(\tau)\xrightarrow{\mathcal D}\mu. \tag{7}$$

Formalization targets

Goal: Proposition 2

Assume (7) and $\beta>0$. Then

$$\frac{R^{LP(k)}}{v^{(k)}}\xrightarrow{\mathcal D}1\qquad\text{and}\qquad\frac{ER^{LP(k)}}{v^{(k)}}\to1\qquad(k\to\infty).$$

Both clauses are one statement, for every instance satisfying the standing assumptions and every optimal solution $x^*$.

Milestones

In proof order:

• the $k$th LP $\max\{f\cdot x:Ax\le kc,\ 0\le x\le k\mu\}$ has optimal solution $kx^*$ and value $k\beta$ (claim after (6));
• the booking-limit identity (5), $N^{LP}_j=D_j(\tau)\wedge\lfloor x^*_j\rfloor$, pathwise;
• $\pi^{LP}$ does not look into the future and respects capacity (§3);
• Lemma 1: if $X_k\xrightarrow{\mathcal D}X$ in $\mathbb R^n$ and $h_k\to h$ uniformly on compact sets with $h$ continuous, then $h_k(X_k)\xrightarrow{\mathcal D}h(X)$;
• $g_k(y)=\sum_j f_j(y_j\wedge k^{-1}\lfloor kx^*_j\rfloor)$ converges uniformly on compact sets to the continuous $g(y)=\sum_j f_j(y_j\wedge x^*_j)$;
• the normalized revenues $k^{-1}R^{LP(k)}$ are bounded by $\beta$;
• Proposition 1: $k^{-1}R^{LP(k)}\xrightarrow{\mathcal D}\beta$ and $k^{-1}ER^{LP(k)}\to\beta$;
• Lemma 2: $ER^{LP(k)}\le v^{(k)}\le k\beta$ for all $k\ge1$.

Significance

The result. Proposition 2 says that a policy computed once, from means alone, is asymptotically optimal among all history-dependent policies in regimes where capacity and demand are both large, which is the regime of large airline and hotel networks. It requires no Poisson, Markov or independence structure: (7) is the only condition on the arrivals, and it holds for nonhomogeneous Poisson scaling and for superpositions of i.i.d. copies of a demand process. The upper bound $v^{(k)}\le k\beta$ (Lemma 2) is the standard deterministic LP bound of network revenue management and is used throughout that literature to benchmark heuristics.

Formalizing it. The theorems are proved on paper; no machine-checked version is known to exist. The mission produces a reusable Lean model of the paper's setting: counting paths of a simple multiclass arrival process, nonanticipating history-dependent accept/reject policies, the count (2), the value (1) over all policies, and the bounded LP. It also produces a generalized continuous mapping theorem (Lemma 1) for sequences of functions converging uniformly on compacts, which Mathlib currently has only for a fixed continuous function.

Difficulty

Most of the argument is short on paper, and the effort lies elsewhere. Lemma 2's upper bound must hold against every history-dependent policy, so the proof cannot reduce to allocation or Markov policies. It must pass from almost-sure pathwise constraints to constraints on expected counts, which needs integrability of every admissible count. The identity (5) depends on the arrival at time $t$ being visible to the decision at $t$ and on unit jumps, so it is a statement about right-continuous counting paths that must be proved on those paths, not assumed. Lemma 1 is not the continuous mapping theorem: the function changes with $k$, and the proof has to control $h_k-h$ on compacts that carry most of the mass of the laws. Proposition 2 divides by $v^{(k)}$, a supremum over an uncountable class of policies, and the limit of a ratio of random and deterministic sequences has to be handled in distribution, with each problem on its own probability space.

Formalization scope

• Sample paths are functions ℝ → Fin n → ℕ satisfying IsArrivalPath τ: zero for $t\le0$, monotone, right-continuous, constant after $\tau$, and with total jump at most one at every time. Finitely many arrivals follows.
• A policy is Policy n := (t : ℝ) → (Set.Iic t → Fin n → ℕ) → Fin n → Bool. It sees the path on $(-\infty,t]$, closed at $t$, so it is nonanticipating by its type. $\Pi$ is all such maps.
• $N^\pi_j$ is accepted, the number of indices $i\le D_j(\tau)$ at whose arrival time the policy accepts class $j$. This is (2) for counting paths, and it satisfies $0\le N^\pi\le D(\tau)$ by construction.
• Admissible requires each $N^\pi_j$ to be almost-everywhere measurable and $AN^\pi\le kc$ almost surely. value is the real sSup of the Bochner expectations over admissible policies. The set is nonempty and bounded above in the paper's setting, so this sSup is the paper's supremum.
• Problems are indexed by k : ℕ+, each on its own probability space. Each $D^{(k)}_j(\tau)$ is integrable with mean $k\mu_j$. Convergence in distribution is Mathlib's TendstoInDistribution, and constant limits are constant functions on Unit under Measure.dirac ().
• Fares carry no sign condition. $\beta>0$ is assumed only in the goal, where it excludes the case $\beta=0$ in which every ratio is $0/0$.

The goal must not be replaced by a version with $v^{(k)}$ replaced by $k\beta$, with $\Pi$ restricted to allocation or Markov policies, with Poisson arrivals, or with only one of its two clauses. Each of these is a different and weaker theorem.

Proofs of the milestones are welcome in any order. Lemma 1 and the measurability of accepted along policies are the pieces most likely to be reusable beyond this mission.

Selected references

• W. L. Cooper, Asymptotic Behavior of an Allocation Policy for Revenue Management, Operations Research 50(4):720–727, 2002. https://doi.org/10.1287/opre.50.4.720.2855
• G. Gallego, G. van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8):999–1020, 1994. https://doi.org/10.1287/mnsc.40.8.999
• G. Gallego, G. van Ryzin, A Multiproduct Dynamic Pricing Problem and Its Applications to Network Yield Management, Operations Research 45(1):24–41, 1997. https://doi.org/10.1287/opre.45.1.24
• K. Talluri, G. van Ryzin, An Analysis of Bid-Price Controls for Network Revenue Management, Management Science 44(11):1577–1593, 1998. https://doi.org/10.1287/mnsc.44.11.1577
• P. Billingsley, Convergence of Probability Measures, Wiley, 1968 (Theorem 5.5, p. 34; the paper's reference for Lemma 1). Second edition, 1999: https://doi.org/10.1002/9780470316962

Motivation

The cutting stock problem and the bin packing problem ask for the fewest rolls (or bins) of a fixed capacity from which given numbers of items of several sizes can be cut (or into which they can be packed). They are among the oldest integer programs in operations research, and exact solvers for them and for their multi-dimensional variants (vector packing, cardinality constraints, conflicts) rest on two formulations.

The first is the Gilmore–Gomory model (Gilmore and Gomory 1961): one integer variable per packing pattern, a vector stating how many copies of each item one roll holds. Its linear relaxation gives a strong lower bound, but the number of patterns is exponential, so the model is solved by column generation. The second is the arc-flow model of Valério de Carvalho (1999): patterns are paths in a graph, and a roll is one unit of flow from a source to a target. It has polynomially many variables in the roll length and can be handed directly to a general-purpose solver.

Brandão and Pedroso (2013) generalize the arc-flow model to arbitrary directed acyclic multigraphs whose arcs carry item labels, add exact demands for a chosen set of items and upper bounds on arc flows, and use the model, after graph compression, to solve bin packing, cutting stock, vector packing and related problems exactly. Their Property 1 states that this general model is equivalent to Gilmore–Gomory over the patterns given by the paths of the graph.

Timeline:

• 1961: Gilmore and Gomory introduce the pattern model and its linear relaxation.
• 1998: Vance shows that Dantzig–Wolfe decomposition of Kantorovich's assignment model gives the Gilmore–Gomory model when all rolls have the same width.
• 1999: Valério de Carvalho introduces the arc-flow model on the graph with vertices $0, \dots, W$ and proves its equivalence to Gilmore–Gomory.
• 2013: Brandão and Pedroso state Property 1 for general labelled graphs, with exact demands and arc bounds.

Setting

There are $m$ item types with demands $b \in \mathbb N^m$, and a set $J \subseteq \{1,\dots,m\}$ of items whose demands must be met exactly. A labelled multigraph $G$ has vertices $V$, finitely many arcs $A$, a source $s$ and a target $t$; each arc $(u, v, i)$ goes from $u$ to $v$ and carries a label $i \in \{0, 1, \dots, m\}$, where $i = 0$ marks a loss arc. Parallel arcs are allowed. The graph is acyclic, and there is no directed walk from $t$ to $s$.

The pattern of an $s$–$t$ path counts, for each item $i$, the arcs of the path labelled $i$. $P(G)$ is the set of these patterns.

The arc-flow model (17)–(22) minimizes $z$ over flows $f \ge 0$ with conservation (inflow minus outflow equal to $-z$ at $s$, $z$ at $t$, $0$ elsewhere), total flow on arcs of item $i$ at least $b_i$ for $i \notin J$ and equal to $b_i$ for $i \in J$, and $f_{uvi} \le b_i$ on every arc of an item. The Gilmore–Gomory model (6)–(8) over $P(G)$ minimizes $\sum_p x_p$ over $x \ge 0$ with $\sum_p p_i x_p \ge b_i$ for all $i$. Each model has an integer version and a linear relaxation.

Formalization targets

Goal: Property 1

If $P(G)$ is closed under removing one item (removing one copy of an item from a path pattern gives a path pattern or the zero pattern), then for every $b$ and every $J$

$$\mathrm{afIP}(G, b, J) = \mathrm{ggIP}(P(G), b), \qquad \mathrm{afLP}(G, b, J) = \mathrm{ggLP}(P(G), b),$$

where IP denotes the integer optimum (in $\mathbb N \cup \{\infty\}$) and LP the linear-relaxation value (in the extended reals). Both models are infeasible together.

Milestones

1. Flow decomposition (§3, p.8): every flow satisfying (18) is a nonnegative combination of $s$–$t$ paths with total weight $z$, with integer weights for an integer flow.
2. Arc-flow to Gilmore–Gomory (proof of Property 1): a feasible $(f, z)$ gives a feasible $x$ over $P(G)$ with $\sum_p x_p = z$.
3. Excess removal: under the closure hypothesis, every feasible $x$ can be replaced by one that meets every demand exactly with no more rolls.
4. Gilmore–Gomory to arc-flow: an exactly covering $x$ gives a flow feasible for (17)–(22), arc bounds included, for every $J$.
5. Lower bound unchanged: the constraints (20) and (21) do not change the linear-relaxation value.

Significance

Property 1 is what makes the arc-flow model an exact method. Without it, the optimum of the compact model could differ from the true minimum number of bins, and its linear relaxation would not have the Gilmore–Gomory lower bound, the bound on which the paper's computational results rest. The equality for every $J$ and with the arc bounds (21) is what justifies the paper's choice to impose exact demands for items of demand one and to bound arc flows: these restrictions shrink the search space without changing either value.

The paper proves Property 1 in one paragraph, by appeal to Dantzig–Wolfe decomposition and to flow decomposition from Ahuja, Magnanti and Orlin (1993). No machine-checked proof of this equivalence, or of Valério de Carvalho's special case, is known. A formal proof yields a reusable path decomposition for flows in acyclic multigraphs and a reusable exact-cover lemma for pattern models.

Difficulty

The equivalence is not a direct consequence of LP duality or Dantzig–Wolfe decomposition as stated in textbooks. The subproblem (18), (21), (22) contains the arc bounds (21), which tie the flow to the demands, so its extreme points are not simply the $s$–$t$ paths. The naive substitution "replace the flow by its paths" proves only one inequality. The converse needs the excess-removal step, which uses a property of the pattern set, not of the graph: the superset reading "$P(G)$ contains every valid pattern" is false (a graph with patterns $(1,0), (0,1), (2,1)$ and $b = (1,1)$, $J = \{1,2\}$ has Gilmore–Gomory value 1 and arc-flow value 2). The flow decomposition must also be carried out over $\mathbb N$ and over $\mathbb R$, and acyclicity is essential: a cycle carries flow that covers demand at no cost in $z$.

Formalization scope

Items are Fin m; a label is Option (Fin m) with none for loss arcs. The graph is a structure with tail, head, label, source and target maps on an arc type A with [Fintype A]; the vertex type is arbitrary. Paths are lists of arcs forming a walk; acyclicity means no closed walk of positive length. The standing assumption "no walk from $t$ to $s$" formalizes that $s$ is the only excess node and $t$ the only deficit node; it holds whenever $s$ has no entering arc, $t$ no leaving arc, or some $s$–$t$ path exists. Conservation (18) is written as $\mathrm{in}(k) + [k=s]z = \mathrm{out}(k) + [k=t]z$, equivalent for $s \ne t$. Gilmore–Gomory solutions are finitely supported functions on patterns (Finsupp), over $\mathbb N$ or $\mathbb R$. Optimal values are infima in ℕ∞ and EReal, never in $\mathbb N$ or $\mathbb R$, so infeasibility cannot collapse to the value 0. The hypothesis "all valid packing patterns represented as paths" is replaced by the weaker closure of $P(G)$ under removing one item, which every set of valid packing patterns satisfies.

The goal keeps both clauses, every $J$, and the arc bounds (21). Proofs of the milestones, a general path decomposition for nonnegative flows in finite acyclic multigraphs (for instance via the published cycle decomposition LinearOptimization.network_flow_decomposition and a feedback arc $t \to s$), and the exact-cover argument over $\mathbb R$ are all welcome.

Selected references

• F. Brandão, J. P. Pedroso, Bin Packing and Related Problems: General Arc-flow Formulation with Graph Compression, Technical Report DCC-2013-08, Universidade do Porto, 2013. arXiv:1310.6887
• P. C. Gilmore, R. E. Gomory, A Linear Programming Approach to the Cutting-Stock Problem, Operations Research 9(6), 1961. doi:10.1287/opre.9.6.849
• J. M. Valério de Carvalho, Exact solution of bin-packing problems using column generation and branch-and-bound, Annals of Operations Research 86, 1999. doi:10.1023/A:1018952112615
• P. H. Vance, Branch-and-price algorithms for the one-dimensional cutting stock problem, Computational Optimization and Applications 9, 1998. doi:10.1023/A:1018346107246
• R. K. Ahuja, T. L. Magnanti, J. B. Orlin, Network Flows: Theory, Algorithms, and Applications, Prentice Hall, 1993.

Motivation

Observed portfolios, from mutual fund holdings to market capitalization weights, are rarely mean-variance efficient: their Sharpe ratio falls short of that of the tangency portfolio. In a classical CARA–normal model this cannot happen, so the gap needs an explanation. Hara and Honda (working paper, 2018; Management Science, 2022) explain it by ambiguity aversion in the smooth model of Klibanoff, Marinacci and Mukerji (Econometrica, 2005). An investor who is unsure of the expected returns and dislikes that uncertainty holds a portfolio that is not mean-variance efficient. The paper inverts this: given any portfolio with positive expected excess return, it computes the smallest ambiguity aversion that makes the portfolio optimal, the implied ambiguity. It shows that this number depends on the portfolio only through its normalized Sharpe ratio. The same quantity reappears as a measure of pricing errors (alphas) through the Gibbons–Ross–Shanken identity.

Setting

There are $N$ risky assets with return vector $R$, expected returns $\mu\in\mathbb R^N$ and covariance matrix $\Sigma_R$, a symmetric positive definite $N\times N$ matrix, and a risk-free asset with return $R_f$. Write $\mathbf 1$ for the all-ones vector and $c = \mu - R_f\mathbf 1$ for the excess return vector. For symmetric matrices, $\Sigma_1\le\Sigma_2$ means that $\Sigma_2-\Sigma_1$ is positive semidefinite (the Loewner order).

In the paper's model the investor has a coefficient $\theta>0$ of absolute risk aversion, a coefficient $\eta\ge0$ of relative ambiguity aversion and a second-order belief $0\le\Sigma_M\le\Sigma_R$. Under joint normality, the optimal risky portfolio is $x = \theta^{-1}(\Sigma_R+\eta\Sigma_M)^{-1}c$ (eq. (8)). The mission formalizes the formulas that invert this relation, not the probabilistic model.

Fix a portfolio $x\in\mathbb R^N$ with $c^\top x>0$ (14). The paper defines

$$\bar\theta = \frac{c^\top x}{x^\top\Sigma_R x},\qquad v^\theta = \frac1\theta\Sigma_R^{-1}c - x,\qquad \Sigma_M^\theta = \frac{(\Sigma_R v^\theta)(\Sigma_R v^\theta)^\top}{(v^\theta)^\top\Sigma_R v^\theta},\qquad \eta^\theta = \frac{(v^\theta)^\top\Sigma_R v^\theta}{x^\top\Sigma_R v^\theta}$$

(eqs. (15), (17), (18), (19); Lean: thetaBar, vTheta, sigmaMTheta, etaTheta). The Sharpe ratio of $x\neq0$ is $\mathrm{Sr}(x) = c^\top x/(x^\top\Sigma_R x)^{1/2}$ (sharpe). The tangency portfolio is $\bar x = \Sigma_R^{-1}c$ (tangency), and $\mathrm{Sr}(x)/\mathrm{Sr}(\bar x)$ is the normalized Sharpe ratio of $x$.

Formalization targets

Goal: Theorem 4 (implied ambiguity)

Assume $c^\top x>0$ and that $v^\theta\neq0$ for every $\theta>0$, that is, $x$ is not a positive multiple of $\bar x$. Put

$$q = \left(1-\left(\frac{\mathrm{Sr}(x)}{\mathrm{Sr}(\bar x)}\right)^2\right)^{1/2},\qquad \theta^* = \frac{\bar\theta}{1+q}.$$

Then $\theta^*\in(0,\bar\theta)$, $\theta^*$ is the unique minimizer of $\theta\mapsto\eta^\theta$ on $(0,\bar\theta)$, and

$$\eta^{\theta^*} = \frac{2q}{1-q}.$$

The extra hypothesis is a correction: as printed, the theorem fails when $x$ is a positive multiple of $\bar x$. There $\eta^\theta$ has infimum $0$ on $(0,\bar\theta)$ but no minimum. The hypothesis is the one of Lemma 4, by which the paper proves the theorem.

Milestones

1. Theorem 3 (p.19). For $0<\theta<\bar\theta$ with $v^\theta\ne0$: $0\le\Sigma_M^\theta\le\Sigma_R$, $\eta^\theta>0$, and $x = \theta^{-1}(\Sigma_R+\eta^\theta\Sigma_M^\theta)^{-1}c$. So $\eta^\theta$ is a genuine ambiguity aversion making $x$ optimal.
2. Lemma 4 (p.41). For any positive definite $\Sigma$ and $S$, the ratio $\theta\mapsto (v^\theta)^\top Sv^\theta/x^\top\Sigma v^\theta$ is positive on $(0,\bar\theta)$ and has a unique minimizer there, given by (33), with minimum (34).
3. Lemma 4 with $S=\Sigma$ (p.41). The same conclusion with (33) and (34) rewritten in terms of $\bar\theta^{-1}c-\Sigma x$.
4. §4.3 Sharpe ratio facts (p.21). $\mathrm{Sr}$ is positively homogeneous of degree zero and is maximized at $\bar x$ and its positive multiples, with $\mathrm{Sr}(\bar x) = (c^\top\Sigma_R^{-1}c)^{1/2}$. The normalized Sharpe ratio lies in $[-1,1]$. The page says "every scalar multiple", which is false for negative multiples.
5. Identity in the proof of Theorem 4 (p.43). $(\bar\theta^{-1}c-\Sigma_Rx)^\top\Sigma_R^{-1}(\bar\theta^{-1}c-\Sigma_Rx) = \bar\theta^{-2}(\mathrm{Sr}(\bar x)^2-\mathrm{Sr}(x)^2)$.

Significance

Theorem 4 gives a closed form: the implied ambiguity $2q/(1-q)$ is a strictly increasing function of the Sharpe-ratio shortfall $q$. It runs from $0$ for an efficient portfolio to $+\infty$ as the normalized Sharpe ratio drops to zero. Any portfolio with positive expected excess return is therefore optimal for some ambiguity-averse investor, and the least ambiguity aversion required is an explicit number. The risk aversion $\theta^*$ that attains it lies between $\bar\theta/2$ and $\bar\theta$. The paper uses the formula to calibrate the implied ambiguity of factor portfolios and to read pricing errors as ambiguity.

The results are proved on paper but, as far as is known, have not been machine-checked. A formalization yields Lemma 4 with a general weight $S$, a one-variable minimization of a ratio of quadratic forms that is reusable elsewhere. It also yields a checked version of the paper's main theorem with its missing hypothesis made explicit.

Difficulty

The definitions are explicit, but the minimization is not a routine calculus exercise. The function $\eta^\theta$ is a ratio whose numerator and denominator are quadratic and linear in $1/\theta$. Its denominator vanishes at $\bar\theta$, and its behaviour at both ends of $(0,\bar\theta)$ must be controlled. Setting the derivative to zero gives a quadratic equation in $1/\theta$, and one must show that it has exactly one root in the admissible range. The closed form then needs a Cauchy–Schwarz argument in the $\Sigma_R^{-1}$ inner product. That argument shows $\mathrm{Sr}(x)\le\mathrm{Sr}(\bar x)$, so the square root in $q$ is of a number in $[0,1)$. The obvious approach, minimizing at $\theta=\bar\theta/2$ or another fixed fraction, is wrong except in special cases: the minimizer moves with the normalized Sharpe ratio. Theorem 3 needs its own matrix argument, the inverse of a rank-one update of $\Sigma_R$ together with a Cauchy–Schwarz bound for the Loewner inequality.

Formalization scope

Assets are indexed by Fin N and vectors are Fin N → ℝ. $\Sigma_R\in\mathcal S^N_{++}$ is Matrix.PosDef, which includes symmetry, and the Loewner order $A\le B$ is (B - A).PosSemidef. Matrix inverses are Mathlib's ⁻¹, the true inverse on positive definite matrices. Quadratic forms are written v ⬝ᵥ (A *ᵥ v), and $(\cdot)^{1/2}$ is Real.sqrt. The excess return vector is excessReturn μ Rf. The definitions take it as an argument c, so Lemma 4's notation and the model's coincide.

$\eta^\theta$, $\Sigma^\theta_M$ and $\mathrm{Sr}$ are total Lean functions, using Lean's $a/0=0$. The goal minimizes $\eta^\theta$ over exactly Set.Ioo 0 θ̄, where its denominator is positive. A formalization over $(0,\bar\theta]$ would pick up the junk value $\eta^{\bar\theta}=0$ and is ruled out. The goal states all three parts: location, minimality with uniqueness, and the value. An infimum-only version would be a weaker theorem.

No new library infrastructure is required beyond Mathlib's linear algebra over positive definite matrices and one-variable real analysis. Contributions that prove Lemma 4 for general $S$ are particularly reusable. The Cauchy–Schwarz inequality in the inner product induced by a positive definite matrix, used by milestones 4 and 5 and by Theorem 3, is a natural standalone lemma.

Selected references

• C. Hara and T. Honda, Implied Ambiguity: Mean-Variance Efficiency and Pricing Errors, working paper, October 9, 2018; published as Implied Ambiguity: Mean-Variance Inefficiency and Pricing Errors, Management Science, 2022. https://doi.org/10.1287/mnsc.2021.4097
• P. Klibanoff, M. Marinacci and S. Mukerji, A Smooth Model of Decision Making under Ambiguity, Econometrica 73(6), 2005. https://doi.org/10.1111/j.1468-0262.2005.00640.x
• M. R. Gibbons, S. A. Ross and J. Shanken, A Test of the Efficiency of a Given Portfolio, Econometrica 57(5), 1989. https://doi.org/10.2307/1913625

Motivation

Whether a service provider should show customers its queue is a classical question in the economics of queues. When customers know the quality of service, the answer is a threshold in market size: Hassin (1986) and Chen and Frank (2004) showed that a revenue-maximizing server conceals the queue when the potential arrival rate is small and reveals it when it is large. In practice customers rarely know quality. A server that knows it is good may want to disclose its queue to signal that, and a poor one may want to imitate it.

Guo, Haviv, Luo and Wang (2023) study this as a signaling game: the server privately knows its quality and chooses to reveal or conceal its queue, and customers infer quality from that choice. Their first result, Proposition 1, settles the case in which all customers are uninformed: the disclosure decision cannot signal quality, because the only pure-strategy equilibria that survive the perfect-sequential-equilibrium refinement are pooling ones. This mission formalizes that result and the derivation leading to it.

Setting

A single server serves customers one at a time, with exponential service times at rate $\mu>0$. Customers arrive as a Poisson process with potential arrival rate $\lambda>0$; write $\rho=\lambda/\mu$. Each customer pays $\theta>0$ per unit time spent in the system. The server is of high quality $H$ with prior probability $\delta\in(0,1)$, and then a served customer receives $V_H$; otherwise it is of low quality $L$ and the reward is $V_L$, with $V_H>V_L>\theta/\mu$.

The server learns its type and chooses a signal: reveal the queue ($R$) or conceal it ($C$). Customers observe the signal, form a belief $\delta^R$ or $\delta^C\in[0,1]$ that the server is of high quality, and decide whether to join. Their expected reward under belief $d$ is $\bar V(d)=dV_H+(1-d)V_L$.

• In a revealed queue, all customers join if and only if the number in the system does not exceed Naor's threshold $n(d)=\lfloor \bar V(d)\mu/\theta\rfloor-1$, and the effective arrival rate is

$$\lambda^O(d)=\frac{\lambda\sum_{k=0}^{n(d)}\rho^k}{\sum_{i=0}^{n(d)+1}\rho^i}\qquad(1)$$

• In a concealed queue, customers join with the equilibrium probability of an unobservable $M/M/1$ queue, and

$$\lambda^U(d)=\begin{cases}\lambda,&\lambda<\mu-\theta/\bar V(d),\\ \mu-\theta/\bar V(d),&\text{otherwise.}\end{cases}\qquad(3)$$

The server's payoff is its effective arrival rate. With all customers uninformed, the queue length carries no information, so a server that reveals earns $\lambda^O(\delta^R)$ and one that conceals earns $\lambda^U(\delta^C)$, whatever its type.

A pure profile $(s',s'')$ says that $H$ sends $s'$ and $L$ sends $s''$. A pure sequential equilibrium is a pure profile with beliefs in $[0,1]$ that follow Bayes' rule on signals some type sends, and under which no type gains by sending the other signal. Off-path beliefs are otherwise free. The credible updating rule (Definition 2) restricts them: a posterior $\gamma$ after an off-path signal is credible when it is the Bayes posterior obtained if exactly the types that weakly gain from deviating under $\gamma$ deviate (those strictly gaining with probability one). A perfect sequential equilibrium (Grossman and Perry, 1986) is a sequential equilibrium that no credible belief upsets, i.e. under no credible off-path belief does some type strictly gain by deviating.

Formalization targets

Goal: Proposition 1

The curves $\lambda\mapsto\lambda^O(\delta)$ and $\lambda\mapsto\lambda^U(\delta)$ cross exactly once on $(0,\infty)$, at $\hat\lambda$. For every $\lambda>0$ with $\lambda^O(1)\ne\lambda^U(0)$ and $\lambda^O(0)\ne\lambda^U(1)$:

$$\lambda<\hat\lambda:\ \text{the pure perfect sequential equilibria are exactly those on }(C,C);\qquad \lambda>\hat\lambda:\ \text{exactly those on }(R,R).$$

The printed proposition says "otherwise" ($\lambda\ge\hat\lambda$) and excludes the rates where "$\lambda^O(1)=\lambda^U(0)$ and $\lambda^O(0)=\lambda^U(1)$". At $\lambda=\hat\lambda$ both pooling profiles are perfect sequential equilibria, and with the parameters of the paper's Example 1 a separating equilibrium exists at $\lambda=1$, where only the second equality holds. The goal therefore uses $\lambda>\hat\lambda$ and excludes the union of the two equality sets.

Milestones

1. (1) in closed form: $\lambda^O(d)=\lambda(1-p_{n+1})=\mu-\mu/\sum_{i=0}^{n+1}\rho^i$, strictly increasing in $\lambda$.
2. The unique crossing point $\hat\lambda$ of $\lambda^O(d)$ and $\lambda^U(d)$, with the sign of $\lambda^O-\lambda^U$ on each side.
3. The credible updating rule in two-type form: a credible belief is the prior when both types strictly gain, $1$ (resp. $0$) when only $H$ (resp. $L$) weakly gains, and it imposes nothing when both strictly prefer to stay.
4. The four pure profiles (§4.2 items (1)–(4)): $(R,R)$ is sequential with off-path $\delta^C$ iff $\lambda^U(\delta^C)\le\lambda^O(\delta)$; $(C,C)$ with off-path $\delta^R$ iff $\lambda^O(\delta^R)\le\lambda^U(\delta)$; $(R,C)$ iff $\lambda^O(1)=\lambda^U(0)$; $(C,R)$ iff $\lambda^O(0)=\lambda^U(1)$.

Significance

Proposition 1 says that queue disclosure is uninformative when customers are homogeneous and uninformed: the low-quality server always mimics the high-quality one, and the market-size threshold of the full-information literature reappears at the prior belief. Corollary 1 of the paper (not part of this mission) deduces that signaling then neither raises nor lowers the server's throughput. The result is the benchmark against which the paper's second part, with informed customers, measures when separation becomes possible.

The proof in the paper is in an online appendix; the article gives the derivation step by step. No machine-checked version of this result, of the credible updating rule, or of perfect sequential equilibrium exists on the platform. A formal proof would also fix the boundary cases: the statement as printed is false at $\lambda=\hat\lambda$ and at rates where only one of the two exceptional equalities holds.

Difficulty

The analytic part is the crossing point. $\lambda^U(\delta)$ equals $\lambda$ up to the kink $\mu-\theta/\bar V(\delta)$ and is constant afterwards, while $\lambda^O(\delta)$ lies strictly below $\lambda$, increases strictly, and tends to $\mu$. The two curves are given by different formulas on either side of the kink, and $\lambda^O$ is a ratio of polynomials of degree depending on the floor in $n(\delta)$, so the crossing is not available in closed form. The game-theoretic part is the refinement. Sequential equilibrium alone admits $(R,R)$ and $(C,C)$ on both sides of $\hat\lambda$ for suitable off-path beliefs, so the work is to show that a credible belief upsets the "wrong" pooling profile and none upsets the "right" one. A credible belief is a fixed point (the deviating set is evaluated at the belief it generates), which a direct definition cannot unfold in one step.

Formalization scope

Lean namespace QueueSignal. QueueSignal.SignalingGame defines the general two-type, two-signal game: types QType ($H$, $L$), signals Sig ($R$, $C$), pure profiles Sig × Sig (first component $H$'s signal), beliefs Sig → ℝ, IsPureSE, IsCredible and IsPurePSE for an arbitrary payoff pay : QType → Sig → ℝ → ℝ. QueueSignal.QueueModel defines Params ($\mu,\theta,V_H,V_L,\delta$ with Params.Valid), $\bar V$, the integer threshold naorN, lamO, lamU as functions of $\lambda$ and the belief, and the baseline payoffs pay.

Conventions: beliefs are reals in $[0,1]$; $n(d)$ is computed in $\mathbb Z$ and is nonnegative under the standing assumptions; the customers' subgame is represented by its effective arrival rates, as on p.548 of the paper; "the unique equilibrium is $X$" means that a pure profile admits beliefs making it a perfect sequential equilibrium if and only if it is $X$. Perfect sequential equilibrium is the Grossman–Perry test "no credible belief upsets"; requiring instead that the equilibrium's own off-path belief be credible would make Proposition 1 false. The crossing point $\hat\lambda$ is asserted to exist and be unique, not assumed, which rules out a goal that holds for a free parameter.

Needed infrastructure: finite geometric sums, Int.floor, continuity and limits of rational functions, the intermediate value theorem. The signaling-game definitions are reusable for other two-type signaling games. Proofs of any milestone, and of the general fact that pooling profiles are upset only at the prior, are welcome.

Selected references

• P. Guo, M. Haviv, Z. Luo, Y. Wang, Signaling Service Quality Through Queue Disclosure, Manufacturing & Service Operations Management 25(2):543–562, 2023. https://doi.org/10.1287/msom.2022.1170
• S. J. Grossman, M. Perry, Perfect Sequential Equilibrium, Journal of Economic Theory 39(1):97–119, 1986. https://doi.org/10.1016/0022-0531(86)90021-9
• P. Naor, The Regulation of Queue Size by Levying Tolls, Econometrica 37(1):15–24, 1969. https://doi.org/10.2307/1909200
• N. M. Edelson, D. K. Hildebrand, Congestion Tolls for Poisson Queuing Processes, Econometrica 43(1):81–92, 1975.
• R. Hassin, Consumer Information in Markets with Random Product Quality: The Case of Queues and Balking, Econometrica 54(5):1185–1195, 1986.
• H. Chen, M. Frank, Monopoly Pricing When Customers Queue, IIE Transactions 36(6), 2004.
• D. M. Kreps, R. Wilson, Sequential Equilibria, Econometrica 50(4):863–894, 1982. https://doi.org/10.2307/1912767

Motivation

Bundle gerbes are a higher version of line bundles, we present nonabelian bundle gerbes as a higher version of principal bundles. Connection, curving, curvature and gauge transformations are studied both in a global coordinate independent formalism and in local coordinates. These are the gauge fields needed for the construction of Yang-Mills theories with 2-form gauge potential.

This mission is the statement-level formalization of Nonabelian Bundle Gerbes, their Differential Geometry and Gauge Theory (arXiv:hep-th/0312154v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

6 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Every smooth principal-bibundle morphism over a fixed base is an isomorphism (§2, unnumbered: bibundle morphisms are isomorphisms, PDF p. 4). 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

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

• §1, cited background: Chern and Dixmier–Douady classifications: integral cohomology; complex line bundles; abelian gerbes; Dixmier–Douady class; curvature class (source-ambiguity)
• §1, cited background: Deligne classification: Deligne complex; abelian gerbe connection and curving; differential cohomology comparison (source-ambiguity)
• §1, cited background: twisted K theory and Verlinde algebra: twisted K theory; equivariant twisted K theory; Verlinde algebra (source-ambiguity)
• Proposition 4: associated automorphism bundle criterion: Smooth automorphism Lie group and associated principal bundle Aut(H) ×_H E (hard)
• §2, unnumbered: product, inverse and group of classes: Smooth balanced fibre product, inverse bibundle and isomorphism-class group (hard)
• §2, unnumbered: isomorphisms and trivializations: Smooth balanced product E Eprime inverse and isomorphism/trivialization correspondences (hard)
• §2, unnumbered: local-data classification and products: Independent smooth gluing quotient and refinement equivalence of local bibundle data (hard)
• §2, unnumbered: conjugation of a central section: Conjugated trivial bibundle and central section independent of local sections (hard)
• Proposition 6: recognizing D-H bundles: Smooth crossed module and chosen associated Aut(H)-section of a D-H bundle (hard)
• §2, unnumbered: claimed trivial D-H bundle criterion (deferred): DHBundle; DHMaps; TrivialDHBundle; DHCentralSection (source-ambiguity)
• Proposition 7: canonical trivial associated H-bibundle: Associated H ×_D Q quotient, twisted actions and canonical central section (hard)
• §2, unnumbered: D-H products and reconstruction: D-H associated and balanced products, smooth reconstruction and psi local data (hard)
• Theorem 9: right 2-connection and unique descended A: Lie(H)- and Lie(Aut(H))-valued smooth forms and descended right 2-connection (hard)
• §3, unnumbered: affine closure of 2-connections: Concrete 2-connection predicate with smooth forms, vertical normalization and T_A (hard)
• Remark 10: modified tangent action: Constructed tangent-bundle correction and horizontal/vertical projections (hard)
• §3, unnumbered: structural equation, equivariance and Bianchi: Actual covariant exterior derivative, graded brackets and 2-curvatures (hard)
• §3, unnumbered: calculus of equivariant horizontal forms: Equivariant horizontal n-forms, mixed T operations and D square (hard)
• §3, unnumbered: right curvature and right equivariant forms: Constructed right curvature and descent of right-equivariance base forms (hard)
• §3, unnumbered: pullback naturality and local connection formulas: Smooth pullback bibundles, differential naturality and extracted local forms (hard)
• §3, unnumbered: sum and associativity of 2-connections: Descending the ordered connection sum to the smooth balanced quotient (hard)
• §3, unnumbered: sums of forms, D and curvatures: Horizontal equivariant form sums, D compatibility, curvature sums and isomorphism naturality (hard)
• §4, unnumbered: automatic coherence for centre-free H: Smooth gerbe fibre powers, specified central-section coherence and existence (hard)
• §4, unnumbered: gerbe changes by bibundles and trivializations: Explicit smooth gerbe changes with their transformed central cocycles (hard)
• §4, unnumbered: stable equivalence is an equivalence relation: Definition 12 stable equivalence with common refinement and central-section coherence (hard)
• Proposition 13: refinement pullback is stably equivalent: Computed refinement pullback gerbe and explicit stable equivalence witnesses (hard)
• Theorem 14: local stable triviality and section factorization: Open restriction, chosen refinement trivialization and local factorization of central sections (hard)
• §4, unnumbered: bundle gerbes, local gerbes and local data: Independent geometric/local gerbes and local-data refinement quotients with comparison maps (hard)
• §4, unnumbered: normalized local cocycles: Full local gerbe data and the actual ell_ab=f_aaa gauge change (hard)
• §5, unnumbered: lifting gerbe construction: Smooth Lie-group extension, difference map and balanced lifting multiplication (hard)
• §1/§5, unnumbered announced obstruction interpretation (deferred): SmoothGroupExtension; LiftingBundleGerbe; LiftOfPrincipalBundle; TrivialGerbe (source-ambiguity)
• Remark 17: module cocycle is the associativity square: Module data as chosen D-H isomorphisms and the typed associativity square (hard)
• Proposition 19: stable invariance of module classes: Module equivalence classes and transport along chosen stable gerbe equivalence data (hard)
• §6, unnumbered: canonical Aut(H)-H module: Fixed trivial Aut(H)-H bundle, its quotient z map and module coherence (hard)
• §6, unnumbered: module of a lifting gerbe: Natural extension-group module and comparison to the canonical module (hard)
• §6, unnumbered: every module maps to the canonical module: Chosen-psi change of structure Q→can and its module compatibility (hard)
• Proposition 21: modules of a trivial gerbe descend: Module and D-H bundle categories, smooth descent functors and natural isomorphisms (hard)
• Remark 23: descent of A and the summability condition: Gerbe connection definition (125) before descent of its base one-form (hard)
• §7, unnumbered: affine closure and compatible sums: Affine operations on actual summable connections and gerbe connection identities (hard)
• Paper main result, Theorem 24: every nonabelian bundle gerbe admits a connection: Definition 22 gerbe connections on actual smooth bibundle gerbes (hard)
• Proposition 25: explicit partition-of-unity connection: Computed partition-of-unity forms (130),(131) with central-section coordinates (hard)
• §7, unnumbered: curvature cocycle: Curvature sums on T=E12 E23 E13 inverse and its barf inverse coordinate map (hard)
• §7, unnumbered: connection on a lifting gerbe: Lie-algebra differential of a smooth extension and actual lifting forms (hard)
• §7, unnumbered: canonical module connection and general module compatibility: Canonical module connection and independently defined general module connection conditions (hard)
• §7, unnumbered: local connection and curvature identities: Extracted local gerbe and curvature representatives on a good cover (hard)
• §8, unnumbered: transformed curving, descended 3-form and Bianchi: Constructed transformed gerbe, equivariant curving, descended three-form and identities (146)–(151) (hard)
• §8, unnumbered: local curving transformation identities (152)–(156): Actual curving restriction and coefficient extraction for canonical c (hard)
• §8, unnumbered: printed local Bianchi equation (157), deferred: CurvingLocalData; CovariantExteriorDerivative; DerivationCocycle (source-ambiguity)
• §8, unnumbered: partition-of-unity curving prescription (158)–(159), deferred: PartitionCurving; CurvingLocalData; Curving; SmoothPartitionOfUnity (source-ambiguity)
• §8, cited comparison with Breen–Messing differential cocycles: Exact convention translation between (140)–(157) and Breen–Messing local connection, curving and higher-Bianchi equations (source-ambiguity)

Selected references

• Nonabelian Bundle Gerbes, their Differential Geometry and Gauge Theory, arXiv:hep-th/0312154v2, https://arxiv.org/abs/hep-th/0312154v2

Motivation

We review definitions and properties of reproducing kernel Hilbert spaces attached to Gaussian variables and processes, with a view to applications in nonparametric Bayesian statistics using Gaussian priors. The rate of contraction of posterior distributions based on Gaussian priors can be described through a concentration function that is expressed in the reproducing Hilbert space. Absolute continuity of Gaussian measures and concentration inequalities play an important role in understanding and deriving this result. Series expansions of Gaussian variables and transformations of their reproducing kernel Hilbert spaces under linear maps are useful tools to compute the concentration function.

This mission is the statement-level formalization of Reproducing kernel Hilbert spaces of Gaussian priors (arXiv:0805.3252v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

42 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 2.1: agreement of process and Banach RKHSs (seed result) (Theorem 2.1: agreement of process and Banach RKHSs (seed result), 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

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

• §1, cited posterior contraction characterization (1.2)–(1.3): A source-supported precise posterior contraction theorem with all model, prior, true-parameter, rate and minimal-solution hypotheses, and an explicit distinction between a sufficient contraction rate and an optimal iff characterization. (source-ambiguity)
• Lemma 2.2: printed global weak-* continuity: An authorial correction restricting weak-*-to-H-norm continuity to bounded dual sets (already a separate node), or a separately authorized changed theorem. No general infinite-rank version of the printed global assertion exists. (source-ambiguity)
• Corollary 2.1: printed arbitrary weak-* dense subset: A source correction replacing arbitrary dense subset by an appropriate linear subspace or a bounded approximation condition. The original arbitrary-subset assertion is false and cannot be unblocked by a library declaration. (source-ambiguity)
• Example 4.1: integral-operator eigenexpansion: A source-pinned measurable kernel and measure-space framework for the product-L2 Hilbert-Schmidt spectral theorem, correction of dnu(t) to dnu(s), and an indexing convention including zero and finite rank; pointwise equality must remain a separate assumption. (source-ambiguity)

Selected references

• Reproducing kernel Hilbert spaces of Gaussian priors, arXiv:0805.3252v1, https://arxiv.org/abs/0805.3252v1

Motivation

Parallel transport of a connection in a smooth fibre bundle yields a functor from the path groupoid of the base manifold into a category that describes the fibres of the bundle. We characterize functors obtained like this by two notions we introduce: local trivializations and smooth descent data. This provides a way to substitute categories of functors for categories of smooth fibre bundles with connection. We indicate that this concept can be generalized to connections in categorified bundles, and how this generalization improves the understanding of higher dimensional parallel transport.

This mission is the statement-level formalization of Parallel Transport and Functors (arXiv:0705.0452v5). 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 Thin path classes form a groupoid (Lemma 2.3, PDF p. 8). 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

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

• Proposition 2.7: Cech thin-path pullbacks and actual extraction of the natural isomorphism g (hard)
• Theorem 2.9: The categories Triv1_pi(i), Des1_pi(i), and specified extraction/reconstruction functors (hard)
• Lemma 2.14: The actual path-and-jump presented quotient and R on its arrows and transformations (hard)
• Lemma 2.15: The specified projection from the concrete path pushout to the thin path groupoid (hard)
• Lemma 2.16: The constructed section functor s, jump comparison lambda and reconstruction trivialization (hard)
• Proposition 3.5: Actual smooth descent category and its inverse-image trivialization category under Ex (hard)
• Lemma 3.8: The stated assumptions do not imply either chosen trivialization is smooth, and fullness alone does not make a smooth component lift a Gr-natural transformation. Several inequivalent strengthened readings are possible; this source statement is deferred. (source-ambiguity)
• Lemma 3.11: Wilson lines with chosen fibre identifications, smooth contractions and smooth local descent (hard)
• Theorem 3.12: The actual transport predicate and Wilson-line plot smoothness (hard)
• Corollary 3.13: Transport functors and smooth local trivializations on an arbitrary contractible cover (hard)
• Proposition 3.14: The actual smooth-trivialization forgetful functor into transport functors (hard)
• Lemma 4.1: Smooth Lie-algebra-valued one-forms and the canonical line ODE correspondence (hard)
• Lemma 4.2: Adjoint action, right Maurer–Cartan form, and the same specified IVP transport (hard)
• Proposition 4.3: The actual ODE-defined path transport k_A (hard)
• Lemma 4.5: The ODE-constructed functor F_A and Definition 3.1 path-family smoothness (hard)
• Proposition 4.7: The concrete gauge category, smooth-functor category and maps P,D (hard)
• Corollary 4.9: Differential Cech cocycles, smooth right torsors, and the Cech extension of P (hard)
• Lemma 5.1: Smooth principal-bundle trivializations, induced sections and actual horizontal transport (hard)
• Proposition 5.2: The actual bundle-to-path-functor construction and BG-transport predicate (hard)
• Proposition 5.3: Connection-preserving principal-bundle maps and their induced transport transformations (hard)
• Theorem 5.4: The actual principal-bundle-with-connection category, transport category, and parallel-transport functor (hard)
• Proposition 5.6: Based thin loop group, actual torsor-valued transport and induced holonomy homomorphism (hard)
• Theorem 5.8: Unitary bundle connections and the fixed-rank geometric transport comparison (hard)
• Corollary 5.9: Rank-varying unitary transport categories and full Hermitian tensor coherence (hard)
• Lemma 5.10: The stated all-sections bijection is incompatible with the source arrow classes. No proof is supplied to pin a unique correction between changing morphisms, restricting sections, and restricting ranks. (source-ambiguity)
• Proposition 6.1: Actual Lie-groupoid algebroid, differentiated AD action and groupoid connection category (hard)
• Theorem 6.4: For a general groupoid, the printed surjective-anchor torsor definition makes its canonical structure functor i_Gr ill-defined. The source does not select a unique faithful repair of the global category. (source-ambiguity)
• Proposition 6.5: The claimed G-structure is unpinned for nonfaithful representations, and the proof imports a false all-sections/morphism correspondence from Lemma 5.10. Do not assert a faithful-representation version without labeling it a corrected result. (source-ambiguity)
• Lemma A.2: Path-pushout triples and their full two-dimensional universal property (hard)
• Lemma A.3: Actual universal path-pushout triples, compatible morphisms and the induced comparison transformation (hard)
• Lemma A.4: The concrete presented path pushout, inclusion and jump natural equivalence (hard)
• Proposition A.6: Functional/subspace/quotient diffeologies on paths, fixed-endpoint classes and thin loops (hard)
• Proposition A.7-i: Internal diffeological functors on the actual thin path groupoid (hard)
• Proposition A.7-ii: Smooth component lifts through an arbitrary i need not satisfy the path-pushout relations in Gr. The missing coherent lift or faithfulness assumption is not supplied by Definition 3.3, so the printed universal factorization cannot be adopted. (source-ambiguity)
• Lemma B.1: ODE-defined source-oriented rectangle loops and their Lie-algebra mixed derivative (hard)
• Lemma B.2: The actual infinitesimal derivative alpha_(F,gamma) from (B.12)–(B.15) (hard)
• Lemma B.3: The actual tangent-dependent alpha_F and smooth one-form package (hard)
• remark-2.10: The specified identity-structure forgetful functor and its canonical local-trivialization inverse (hard)
• generalized-regularity: The id_BG transport predicate and canonical fixed-endpoint Wilson lines (hard)
• zero-reformulation: The claimed reformulation does not specify a smooth structure manifold mapping injectively into Mor(T), and Mor(i) need not be injective. The degree-zero construction therefore does not apply as written. (source-ambiguity)
• higher-transport-outlook: For general n>1 the article provides an outlook without fixed coherence models or a precise theorem; detailed n=2 statements are deferred to [SW11] and [SW13]. (hard)
• curvature-outlook: The paper explicitly postpones the required transport-2-functor framework and construction to [SW13]; phrases particularly trivial and corresponds to a 2-form are not pinned here. (hard)

Selected references

• Parallel Transport and Functors, arXiv:0705.0452v5, https://arxiv.org/abs/0705.0452v5

Motivation

We show how the treatment of cellularity in families of algebras arising from diagram calculi, such as Jones' Temperley--Lieb wreaths, variants on Brauer's centralizer algebras, and the contour algebras of Cox et al (of which many algebras are special cases), may be unified using the theory of tabular algebras. This improves an earlier result of the first author (whose hypotheses covered only the Brauer algebra from among these families).

This mission is the statement-level formalization of Constructing cell data for diagram algebras (arXiv:math/0503751v3). 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 Unital based homomorphisms preserve the hypergroup involution (Proposition 1.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

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

• Theorem 2.2.1: A missing involutivity condition on the outer permutations in Theorem 2.2.1 (source-ambiguity)
• Remark 2.2.3: A well-defined relation comparing different dependent cell-label fibres, as well as the missing twist involutivity (source-ambiguity)
• Lemma 2.2.4: An actual hypothesis implying alpha squared is the identity (source-ambiguity)
• Theorem 4.1.2: Finiteness of the decorated half-index sets in the prescribed contour table datum (source-ambiguity)
• Theorem 4.1.3: The actual oriented hypergroup-labelled planar algebra, canonical half-diagram gluing, and the displayed inflated cell datum after scalar extension (hard)
• Lemma 4.2.2: The independently defined Rui–Xi cyclotomic TL presentation and diagram-basis/generator comparison (source-ambiguity)
• Corollary 4.2.3: The actual Rui–Xi cyclotomic algebra and its transported A4–A5 table/trace datum (source-ambiguity)
• Corollary 4.2.4 (Rui–Xi): The actual cyclotomic algebra with the specified star and label-inversion maps (source-ambiguity)
• Section 4.3: Integral blob/unipotent model comparison with complete parameters and transported trace (source-ambiguity)
• Section 4.3: H-admissible concrete subdatum and identification with the independently defined type H_n TL algebra (hard)
• Lemma 5.1.3: Brauer graph-stacking algebra over L, its ordered [S1,S2,w] coordinates, and the specific vertical-reflection map (hard)
• Definition/Lemma 5.2.2: The particular walled subdatum of Definition 5.2.1 inside the actual Brauer diagram algebra (hard)
• Corollary 5.2.3: Walled Brauer algebra with its restricted reflection and complete finite cell structure (hard)
• Definition/Lemma 5.3.3: The constructed annular-involution/cyclic-propagation subdatum and its actual spanned subalgebra J_n (hard)
• Lemma 5.3.5: Restriction of the already constructed Brauer vertical reflection to the actual Jones annular subalgebra (hard)
• Corollary 5.3.6 (Graham–Lehrer): Scalar-extended Jones algebra with star composed with rho and a full exact cellular datum (hard)
• Remark 5.3.7: Actual rotational symmetries and distinct allowable twisting automorphisms of one concrete Jones algebra (hard)

Selected references

• Constructing cell data for diagram algebras, arXiv:math/0503751v3, https://arxiv.org/abs/math/0503751v3

Motivation

We study the Fluctuation Theorem (FT) for entropy production in chaotic discrete-time dynamical systems on compact metric spaces, and extend it to empirical measures, all continuous potentials, and all weak Gibbs states. In particular, we establish the FT in the phase transition regime. These results hold under minimal chaoticity assumptions (expansiveness and specification) and require no ergodicity conditions. They are also valid for systems that are not necessarily invertible and involutions other than time reversal. Further extensions involve asymptotically additive potential sequences and the corresponding weak Gibbs measures. The generality of these results allows to view the FT as a structural facet of the thermodynamic formalism of dynamical systems.

This mission is the statement-level formalization of Fluctuation Theorem and Thermodynamic Formalism (arXiv:1712.05167v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

43 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem A: additive Periodic Orbits Fluctuation Principle (seed pinned from abstract) (Theorem A: additive Periodic Orbits Fluctuation Principle (seed pinned from abstract), PDF p. 4). 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

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

• Proposition 1.5: Stein error exponents and entropy production: Pinned tail/Laplace-neighborhood hypotheses for convergence of the unbounded entropy-production mean (source-ambiguity)
• Proposition 1.7: Hoeffding exponent and involutive tradeoff: Pinned finite attained zero-set endpoint and Laplace-limit domain for the complete Hoeffding tradeoff (source-ambiguity)

Selected references

• Fluctuation Theorem and Thermodynamic Formalism, arXiv:1712.05167v3, https://arxiv.org/abs/1712.05167v3

Motivation

Several non-asymptotic formulas are established in channel resolvability and identification capacity, and they are applied to wire-tap channel. By using these formulas, the $ε$ capacities of the above three problems are considered in the most general setting, where no structural assumptions such as the stationary memoryless property are made on a channel. As a result, we solve an open problem proposed in Han & Verdu and Han. Moreover, we obtain lower bounds of the exponents of error probability and the wire-tapper's information in wire-tap channel.

This mission is the statement-level formalization of General non-asymptotic and asymptotic formulas in channel resolvability and identification capacity and their application to wire-tap channel (arXiv:cs/0503088v2). 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 Theorem 4: general identification and resolvability capacity relations (Theorem 4, (24)–(27): general identification/resolvability capacity relations (paper seed), PDF p. 8). 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

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

• Theorem 1: non-asymptotic identification code existence: Nonempty-code domain or source-sanctioned empty identification error convention (source-ambiguity)
• Lemma 1 (Ahlswede–Dueck [1]): subset packing: Separately attributed full-domain interface for Lemma 1 (Ahlswede–Dueck [1]): subset packing (source-ambiguity)
• Lemma 7, (42)–(43): tensorization of optimized moments: A full-domain tensor moment convention for s>1 and a justified numerical optimizer interpretation (source-ambiguity)
• Theorem 8: near-capacity comparisons and quadratic approximations: A precise one-sided quadratic expansion with nondegeneracy and optimizer hypotheses (source-ambiguity)
• Introduction: Csiszár–Narayan [16] equivalence of secrecy criteria: Separately attributed full-domain interface for Introduction: Csiszár–Narayan [16] equivalence of secrecy criteria (hard)
• Remark 1: Oohama [9] partial resolvability bound: Separately attributed full-domain interface for Remark 1: Oohama [9] partial resolvability bound (hard)
• Verdú–Han [19] transmission converse in Lemma 5: Separately attributed full-domain interface for Verdú–Han [19] transmission converse in Lemma 5 (hard)
• §VI.A: Han–Verdú [2]/Han [3] memoryless capacity specialization: Separately attributed full-domain interface for §VI.A: Han–Verdú [2]/Han [3] memoryless capacity specialization (source-ambiguity)
• Remark 3: Arimoto [15] strong-converse exponent: Separately attributed full-domain interface for Remark 3: Arimoto [15] strong-converse exponent (hard)
• Remark 4: Oohama [8] type-method resolvability exponent: Separately attributed full-domain interface for Remark 4: Oohama [8] type-method resolvability exponent (hard)
• §VI.B: Wyner [4] memoryless wiretap lower bound: Separately attributed full-domain interface for §VI.B: Wyner [4] memoryless wiretap lower bound (source-ambiguity)

Selected references

• General non-asymptotic and asymptotic formulas in channel resolvability and identification capacity and their application to wire-tap channel, arXiv:cs/0503088v2, https://arxiv.org/abs/cs/0503088v2

Motivation

The first goal of this survey paper is to argue that if orbifolds are groupoids, then the collection of orbifolds and their maps has to be thought of as a 2-category. Compare this with the classical definition of Satake and Thurston of orbifolds as a 1-category of sets with extra structure and/or with the "modern" definition of orbifolds as proper etale Lie groupoids up to Morita equivalence. The second goal is to describe two complementary ways of thinking of orbifolds as a 2-category: 1. the weak 2-category of foliation Lie groupoids, bibundles and equivariant maps between bibundles and 2. the strict 2-category of Deligne-Mumford stacks over the category of smooth manifolds.

This mission is the statement-level formalization of Orbifolds as stacks? (arXiv:0806.4160v2). 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 Equivalence of categories and quasi-inverses (Theorem 3.3, PDF p. 8). 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

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

• main-bibundles-geometric-stacks: Bibundle bicategory, geometric stacks, and the concrete classifying pseudofunctor B (hard)
• Proposition 2.23: Proper etale smooth internal groupoids, restrictions, and finite linear action charts (hard)
• Proposition 2.26: Smooth pullback groupoid with manifold structure as an existential conclusion (hard)
• Remark 2.27: Smooth essential equivalence for the pullback functor (hard)
• slice-presentation: Smooth slice disjoint union and etale presentation of a proper locally free action (hard)
• principal-bundle-pullback: Right-principal groupoid bundles and their smooth base change (hard)
• Lemma 3.19: Unit principal bundle, smooth sections and equivariant bundle isomorphisms (hard)
• Corollary 3.21: Base-identity anchor-preserving smooth equivariant principal-bundle maps (hard)
• Remark 3.30: Contracted bibundle product with quotient manifold and descended actions (hard)
• Remark 3.33: Reversal of a biprincipal bibundle and its two inverse comparison isomorphisms (hard)
• bibundle-bicategory: Bicategory of smooth bibundles and the bundlization pseudofunctor (hard)
• Lemma 3.34: Smooth bundlization and left principality versus smooth essential equivalence (hard)
• Corollary 3.35: Cover-induced smooth pullback groupoid and invertible associated bibundle (hard)
• Lemma 3.36: Right-principal smooth bibundle, bundlization, isomorphism, and smooth section (hard)
• Lemma 3.37: Local section cover of a principal bundle and functorial presentation after pullback (hard)
• Proposition 3.39: Isomorphism-class categories Gp and HS and the concrete functor z (hard)
• Lemma 3.41: Concrete circle and Z/2-bundle witnesses in Gp[W^-1] with restriction maps (hard)
• vector-bundle-pullback: Groupoid-equivariant vector bundles and their contracted pullback by bibundles (hard)
• Example 4.3: Total category BG of principal bundles with arbitrary smooth base maps (hard)
• cfg-2-category: Strict 2-category structure on all CFGs and its vertical Hom groupoids (hard)
• Example 4.12: Open-cover descent categories and canonical principal-bundle comparison functor (hard)
• Lemma 4.15: Bundle-induced over-Man functor BP and the principal bundle F(id_M) (hard)
• Corollary 4.16: Bundled category of smooth real manifolds and its concrete slice functors (hard)
• Remark 4.18: Classifying-stack Hom functors BP from constructed smooth bibundles (hard)
• Remark 4.23: Vertical iso-comma CFG, projections and natural equivalence of cone categories (hard)
• Example 4.24: Representable 2-fiber product with canonical unit atlas and actual bundle projection (hard)
• Example 4.29: Disjoint unions of coordinate charts and representable surjective-submersion atlases (hard)
• Example 4.30: The specific unit-bundle-induced representable atlas p:G0→BG (hard)
• Proposition 4.31: Atlas groupoid X×_D X and the computed equivalence ψ:D→BG (hard)
• Remark 4.32: Atlas refinement and the canonical common biprincipal smooth bibundle (hard)

Selected references

• Orbifolds as stacks?, arXiv:0806.4160v2, https://arxiv.org/abs/0806.4160v2

Motivation

The ordinary (or classical) Birman-Wenzl-Murakami algebras were initially conceived as an algebraic framework for the Kauffman link invariant. They also appear as centralizer algebras for representations of quantum universal enveloping algebras of orthogonal or symplectic types. It was shown by Morton and Wassermann that the BMW algebras are isomorphic to algebras of tangles in (disc $\times$ interval), modulo Kauffman skein relations. This isomorphism allows one to see very clearly certain properties of the BMW algebras -- for example existence of Markov traces and conditional expectations and a good basis. In the present work, we establish the correponding results for affine BMW algebras, showing they are isomorphic to algebras of tangles in (annulus $\times$ interval), modulo Kaufffman skein relations. Again, this provides an important foundation for studying these algebras, as the existence of Markov traces and conditional expectations are consequences of the isomorphism. Moreover, we obtain a basis of the affine BMW algebras analogous to a well known basis of the affine Hecke algebras.

This mission is the statement-level formalization of Affine Birman-Wenzl-Murakami Algebras and Tangles in the Solid Torus (arXiv:math/0411155v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

20 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 3.8 (Lemma 3.8, PDF p. 18). 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

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

• Abstract main result, made precise by Theorem 6.13 and Corollary 6.14: Affine algebraic family A(n,S); Affine geometric family B(n,S); Connector representatives T_d and family B0; Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Geometric framed tangles; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Adding/removing flagpole maps; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 2.8: Affine geometric (k,n)-diagrams; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Negative loop polynomials f_r; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Mixed winding curves Θ_{a,b}, Θ_minus_{a,b} (hard)
• Proposition 2.14: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Geometric partial/full closures cl_n,cl; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Normalized geometric expectations ε_n; Geometric tower inclusion ι; Ambient and regular isotopy; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Normalized closure trace ε (hard)
• Proposition 3.4: Contraction ideal J_n; Hecke algebra in paper normalization (hard)
• Corollary 3.13: Affine geometric (k,n)-diagrams; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Negative loop polynomials f_r; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Mixed winding curves Θ_{a,b}, Θ_minus_{a,b} (hard)
• Proposition 3.22: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Proposition 3.23: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 4.5: Ordinary and affine Brauer algebras D_n,Dhat_n; Brauer inclusion, closures, expectations and trace; Stacking of ordinary/colored connectors; Brauer ground rings; Integer-colored n-connectors; Ordered boundary endpoints; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Colored connector reflection (hard)
• Proposition 4.6: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Brauer inclusion, closures, expectations and trace; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Geometric partial/full closures cl_n,cl; Integer-colored n-connectors; Geometric connector map c and specialization e; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Normalized geometric expectations ε_n; Geometric tower inclusion ι; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Normalized closure trace ε (hard)
• Proposition 4.7: Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Corollary 4.8: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 5.1: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Geometric Kauffman local relations; Stacking and tangle category (hard)
• Proposition 5.5: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Regular-isotopy classes U(k,n), Uhat(k,n); Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Orientation and standard orientation; Geometric Kauffman local relations; Stacking and tangle category (hard)
• Corollary 5.6: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Regular-isotopy classes U(k,n), Uhat(k,n); Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Orientation and standard orientation; Geometric Kauffman local relations; Stacking and tangle category (hard)
• Proposition 5.7: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Orientation and standard orientation; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Theorem 5.8: Connector representatives T_d and family B0; Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Orientation and standard orientation; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Corollary 5.9: Connector representatives T_d and family B0; Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Orientation and standard orientation; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Corollary 5.10: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Geometric Kauffman local relations; Stacking and tangle category (hard)
• Corollary 5.11: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Adding/removing flagpole maps; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Proposition 5.14: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 5.17: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Shuffles and adjacent-transposition length; Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 5.18: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 5.19: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Theorem 5.20: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Proposition 5.21: Nested cap diagram F_k; Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Proposition 5.32: Contraction ideal J_n; Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; BMW rank ideals W_n^(r); Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 5.34: Contraction ideal J_n; Ordinary Kauffman algebra KT_n(R); Constructed shuffle spans V_n^(r); Canonical BMW tower and base-change maps; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Top-bottom anti-automorphism α; Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; BMW rank ideals W_n^(r); Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Left-right reflection ρ_n; Shift homomorphism S; Shuffles and adjacent-transposition length; Geometric Kauffman local relations; Stacking and tangle category; Side-by-side diagram tensor and BMW image maps; Signed winding curves Θ_r (hard)
• Corollary 5.35: Contraction ideal J_n; Ordinary Kauffman algebra KT_n(R); Constructed shuffle spans V_n^(r); Canonical BMW tower and base-change maps; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Top-bottom anti-automorphism α; Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; BMW rank ideals W_n^(r); Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Left-right reflection ρ_n; Shift homomorphism S; Shuffles and adjacent-transposition length; Geometric Kauffman local relations; Stacking and tangle category; Side-by-side diagram tensor and BMW image maps; Signed winding curves Θ_r (hard)
• Lemma 5.36: Contraction ideal J_n; Ordinary Kauffman algebra KT_n(R); Constructed shuffle spans V_n^(r); Canonical BMW tower and base-change maps; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Top-bottom anti-automorphism α; Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; BMW rank ideals W_n^(r); Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Left-right reflection ρ_n; Shift homomorphism S; Shuffles and adjacent-transposition length; Geometric Kauffman local relations; Stacking and tangle category; Side-by-side diagram tensor and BMW image maps; Signed winding curves Θ_r (hard)
• Lemma 5.37: Contraction ideal J_n; Ordinary Kauffman algebra KT_n(R); Constructed shuffle spans V_n^(r); Canonical BMW tower and base-change maps; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Top-bottom anti-automorphism α; Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; BMW rank ideals W_n^(r); Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Left-right reflection ρ_n; Shift homomorphism S; Shuffles and adjacent-transposition length; Geometric Kauffman local relations; Stacking and tangle category; Side-by-side diagram tensor and BMW image maps; Signed winding curves Θ_r (hard)
• Lemma 5.38: Contraction ideal J_n; Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; BMW rank ideals W_n^(r); Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 5.39: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Context permutation ρ for Lemma 5.39; Shuffles and adjacent-transposition length; Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Proposition 5.40: Contraction ideal J_n; Ordinary Kauffman algebra KT_n(R); Constructed shuffle spans V_n^(r); Canonical BMW tower and base-change maps; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Top-bottom anti-automorphism α; Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; BMW rank ideals W_n^(r); Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Left-right reflection ρ_n; Shift homomorphism S; Shuffles and adjacent-transposition length; Geometric Kauffman local relations; Stacking and tangle category; Side-by-side diagram tensor and BMW image maps; Signed winding curves Θ_r (hard)
• Theorem 5.41: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Corollary 5.42: Connector representatives T_d and family B0; Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Corollary 5.43: Universal coefficient ring Λ (hard)
• Corollary 5.44: Canonical BMW tower and base-change maps (hard)
• Corollary 5.45: Canonical BMW tower and base-change maps (hard)
• Corollary 5.46: Ordinary Kauffman algebra KT_n(R); Canonical BMW tower and base-change maps; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Geometric partial/full closures cl_n,cl; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Normalized geometric expectations ε_n; Geometric tower inclusion ι; Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Normalized closure trace ε; Transported BMW expectations and traces (hard)
• Lemma 6.3: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Preliminary affine skein algebra K_n(R); Simple windings; Geometric Kauffman local relations; Stacking and tangle category; Standard position; Signed winding curves Θ_r (hard)
• Lemma 6.4: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Crossing counts and lower-crossing submodules; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Simple windings; Geometric Kauffman local relations; Stacking and tangle category; Standard position; Signed winding curves Θ_r (hard)
• Theorem 6.5: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Simple windings; Geometric Kauffman local relations; Stacking and tangle category; Standard position; Signed winding curves Θ_r (hard)
• Lemma 6.6: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 6.8: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Lemma 6.10: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Crossing counts and lower-crossing submodules; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Proposition 6.12: Affine algebraic family A(n,S); Affine geometric family B(n,S); Connector representatives T_d and family B0; Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Theorem 6.13: Affine algebraic family A(n,S); Affine geometric family B(n,S); Connector representatives T_d and family B0; Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Corollary 6.14: Affine algebraic family A(n,S); Affine geometric family B(n,S); Connector representatives T_d and family B0; Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Regular-isotopy classes U(k,n), Uhat(k,n); Integer-colored n-connectors; Geometric connector map c and specialization e; Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Universal affine coefficient ring Λhat; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Corollary 6.15: Canonical BMW tower and base-change maps (hard)
• Corollary 6.16: Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Geometric partial/full closures cl_n,cl; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Normalized geometric expectations ε_n; Geometric tower inclusion ι; Ambient and regular isotopy; Universal coefficient ring Λ; Negative loop polynomials f_r; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Mixed winding curves Θ_{a,b}, Θ_minus_{a,b}; Normalized closure trace ε; Transported BMW expectations and traces; Conjugated winding elements x_n_prime,X_n_prime (source-ambiguity)
• Corollary 6.18: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Geometric partial/full closures cl_n,cl; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Normalized geometric expectations ε_n; Geometric tower inclusion ι; Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Normalized closure trace ε; Transported BMW expectations and traces (hard)
• Corollary 6.19: Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Geometric tower inclusion ι; Ambient and regular isotopy; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• §2.4, unnumbered: preliminary closed affine skein algebra: Affine geometric (k,n)-diagrams; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Remark 2.10: specialized zero-strand algebra: Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Ambient and regular isotopy; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• §2.6, unnumbered: geometric symmetries: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Top-bottom anti-automorphism α; Crossing reversal β; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Negative loop polynomials f_r; Preliminary affine skein algebra K_n(R); Left-right reflection ρ_n; Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Mixed winding curves Θ_{a,b}, Θ_minus_{a,b} (hard)
• §2.7, unnumbered: inclusion and normalized expectation: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Geometric partial/full closures cl_n,cl; Ordinary geometric (k,n)-diagrams; Ordered boundary endpoints; Normalized geometric expectations ε_n; Geometric tower inclusion ι; Ambient and regular isotopy; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Remark 2.15: printed geometric Markov formulas: Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Geometric partial/full closures cl_n,cl; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Normalized geometric expectations ε_n; Geometric tower inclusion ι; Ambient and regular isotopy; Universal coefficient ring Λ; Negative loop polynomials f_r; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Mixed winding curves Θ_{a,b}, Θ_minus_{a,b}; Normalized closure trace ε; Conjugated winding elements x_n_prime,X_n_prime (source-ambiguity)
• Remarks 3.3 and 3.7: algebraic maps and symmetries: Ordinary Kauffman algebra KT_n(R); Canonical BMW tower and base-change maps; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Top-bottom anti-automorphism α; Crossing reversal β; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Negative loop polynomials f_r; Preliminary affine skein algebra K_n(R); Left-right reflection ρ_n; Shift homomorphism S; Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Mixed winding curves Θ_{a,b}, Θ_minus_{a,b} (hard)
• §4.2, unnumbered: affine Brauer multiplication: Ordinary and affine Brauer algebras D_n,Dhat_n; Stacking of ordinary/colored connectors; Brauer ground rings; Integer-colored n-connectors; Ordered boundary endpoints; Universal coefficient ring Λ; Universal affine coefficient ring Λhat (hard)
• §4.3, unnumbered: colored Brauer expectations and trace: Ordinary and affine Brauer algebras D_n,Dhat_n; Brauer inclusion, closures, expectations and trace; Stacking of ordinary/colored connectors; Brauer ground rings; Integer-colored n-connectors; Ordered boundary endpoints; Universal coefficient ring Λ; Universal affine coefficient ring Λhat (hard)
• §5.2, unnumbered: unique positive permutation lift: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Top-bottom anti-automorphism α; Geometric braid group and permutation map; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Canonical comparison maps φ; Positive permutation braids and their lifts; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Remark 5.25: diamond symmetries and alternative products: Ordinary Kauffman algebra KT_n(R); Canonical BMW tower and base-change maps; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Top-bottom anti-automorphism α; Crossing reversal β; Regular-isotopy classes U(k,n), Uhat(k,n); Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Universal coefficient ring Λ; Negative loop polynomials f_r; Preliminary affine skein algebra K_n(R); Left-right reflection ρ_n; Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Mixed winding curves Θ_{a,b}, Θ_minus_{a,b} (hard)
• §6.1, unnumbered: affine descending spanning: Ordinary Kauffman algebra KT_n(R); Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Orientation and standard orientation; Preliminary affine skein algebra K_n(R); Simple windings; Geometric Kauffman local relations; Stacking and tangle category; Standard position; Signed winding curves Θ_r (hard)
• Remark 6.7: geometric through-strand transport: Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Remark 6.9: geometric bottom-cap transport: Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Totally descending diagrams; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Ambient and regular isotopy; Orientation and standard orientation; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r (hard)
• Remark 6.17: uniqueness of the Markov trace: Ordinary Kauffman algebra KT_n(R); Geometric winding elements X_r; Affine geometric (k,n)-diagrams; Affine Kauffman algebra affineKT_n(S); Regular-isotopy classes U(k,n), Uhat(k,n); Geometric partial/full closures cl_n,cl; Ordinary geometric (k,n)-diagrams; Pictured generators X_1,G_i,E_i and inverses; Ordered boundary endpoints; Normalized geometric expectations ε_n; Geometric tower inclusion ι; Ambient and regular isotopy; Canonical comparison maps φ; Preliminary affine skein algebra K_n(R); Geometric Kauffman local relations; Stacking and tangle category; Signed winding curves Θ_r; Normalized closure trace ε; Transported BMW expectations and traces; Conjugated winding elements x_n_prime,X_n_prime (source-ambiguity)

Selected references

• Affine Birman-Wenzl-Murakami Algebras and Tangles in the Solid Torus, arXiv:math/0411155v2, https://arxiv.org/abs/math/0411155v2

Motivation

Providing security guarantees for wireless communication is critically important for today's applications. While previous work in this area has concentrated on radio frequency (RF) channels, providing security guarantees for RF channels is inherently difficult because they are prone to rapid variations due small scale fading. Wireless optical communication, on the other hand, is inherently more secure than RF communication due to the intrinsic aspects of the signal propagation in the optical and near-optical frequency range. In this paper, secure communication over wireless optical links is examined by studying the secrecy capacity of a direct detection system. For the degraded Poisson wiretap channel, a closed-form expression of the secrecy capacity is given. A complete characterization of the general rate-equivocation region is also presented. For achievability, an optimal code is explicitly constructed by using the structured code designed by Wyner for the Poisson channel. The converse is proved in two different ways: the first method relies only on simple properties of the conditional expectation and basic information theoretical inequalities, whereas the second method hinges on the recent link established between minimum mean square estimation and mutual information in Poisson channels.

This mission is the statement-level formalization of The Degraded Poisson Wiretap Channel (arXiv:1004.0269v1). 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 Conditional independence makes mutual information subadditive (Unnumbered information inequality, pp.5,19, (61), 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

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

• Theorem 1: closed-form secrecy capacity (seed paper result): Normalized continuous-time Poisson wiretap codes and operational secrecy capacity (hard)
• Lemma 1 (Lapidoth, Telatar and Urbanke [21]): stochastic degradation: Measurable Poisson-noise addition and independent thinning kernels (hard)
• Unnumbered, p.8: identical channels have zero secrecy capacity: Operational capacity on the equal-parameter boundary (hard)
• Unnumbered consequence of Theorem 1: unknown further-degraded eavesdropper: One stochastic code chosen before unknown eavesdropper parameters (hard)
• Unnumbered worst-case scenario: equal dark-current/gain ratios: Operational equal-ratio capacity and its optimizer (hard)
• Unnumbered special case (14): no dark current: Operational no-dark-current capacity and unique optimizer (hard)
• Lemma 2 (bound attributed to Kabanov [16]): Arbitrary-waveform continuous-time Poisson mutual-information bound (hard)
• Theorem 2: achievability of every rate below the formula: Continuous-time stochastic code achievability below the independent analytic formula (hard)
• Lemma 3 (Wyner [29]): finite-variable/process entropy identity: Finite-variable conditional entropy given an arbitrary process history (hard)
• Lemma 4: finite-time rate bound for every code: Full-path code law, conditional information, and actual average decoding error (hard)
• Lemma 5: conditional mutual information as a difference: Physical joint Poisson law and finite conditional mutual information (hard)
• Lemma 6: information lost by adding dark current: Independent dark-current addition on full observation histories (hard)
• Lemma 7: information lost by thinning: Conditional independent splitting of a full Cox point process (hard)
• Unnumbered key inequality (67), reused as (85): Distribution-sensitive full-process information gap (hard)
• Theorem 3: universal per-time conditional-information upper bound: Universal full-process conditional information per real observation time (hard)
• Theorem 4 (Converse): achievable secrecy rates obey the formula: Weak converse for operational continuous-time secrecy rates (hard)
• Theorem 5: full rate-equivocation region: Operational full rate-equivocation region and nontrivial-message normalization (hard)

Selected references

• The Degraded Poisson Wiretap Channel, arXiv:1004.0269v1, https://arxiv.org/abs/1004.0269v1

Motivation

In this article we discuss local aspects of 2-functors defined on the path 2-groupoid of a smooth manifold; in particular, local trivializations and descent data. This is a contribution to a project that provides an axiomatic formulation of connections on (possibly non-abelian) gerbes in terms of 2-functors. The main result of this paper establishes the first part of this formulation: we prove an equivalence between the globally defined 2-functors and their locally defined descent data. The second part appears in a separate publication; there we prove equivalences between descent data, on one side, and various existing versions of gerbes with connection on the other side.

This mission is the statement-level formalization of Local Theory for 2-Functors on Path 2-Groupoids (arXiv:1303.4663v1). 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 Lemma A.7: unit compatibility and inverse-pair naturality (A.7, PDF p. 45). 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

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

• 4.2.2: Independent global refinement bicategories and the specified span Ex,v (hard)
• 2.3.1: Constructed g,psi,f with the full descent unit and associativity equations (hard)
• 2.3.2: Extracted h,epsilon and both descent-arrow coherence diagrams (hard)
• 2.3.3: Whiskered modification E and its overlap constraint (hard)
• 2.3.4: Actual extraction pseudofunctor Ex_pi, including compositor and unitor (hard)
• 3.1.1: Codescent generators-and-relations bicategory and all weak inverse data (hard)
• 3.2.1: Canonical projection p_pi and its specified section s,zeta (hard)
• 3.2.2: Endpoint-fixed lifting into the actual codescent presentation (hard)
• 3.2.3: Nonempty jump words, projected identity cells, and type-(1c) representative predicate (hard)
• 3.2.4: Constructed section compositor and restricted generator representations (hard)
• 3.2.5: Section construction parameterized by all permitted local-lift choices (hard)
• 3.3.1: Raw pairing transformation R(h,epsilon) before imposing T2 (hard)
• 3.3.2: All-level generator assignment R and its strict functor laws (hard)
• 3.3.3: Specified inclusion iota, precomposition, R and forgetful V (hard)
• 3.3.4: Normalized descent, actual reconstruction, and its inverse-pair compositors (hard)
• 4.1.1: Concrete Ex_pi and Rec_pi with two coherent equivalences (hard)
• 4.1.2: Computed pseudonatural equivalence Ex_pi Rec_pi=>id_Des (hard)
• 4.1.3: Computed pseudonatural equivalence id_Triv=>Rec_pi Ex_pi (hard)
• 4.2.1: Common-refinement bicategories and the induced extraction (4.2.3) (hard)
• descent-bicategory: Descent objects, arrows, modifications, their compositions and strict V (hard)
• 2.2.4: A valid point-descent/Frobenius identification (source-ambiguity)
• pairing-faithful: Recovery of descent arrows/modifications from the concrete pairing (hard)
• reconstruction: Rec_pi with its computed pi-local trivialization and choice comparison (hard)
• forgetful-equivalence: Specified forgetful v from common-refinement trivializations (hard)
• functor-strict-iff: Valid necessity hypothesis in the strictness converse (source-ambiguity)

Selected references

• Local Theory for 2-Functors on Path 2-Groupoids, arXiv:1303.4663v1, https://arxiv.org/abs/1303.4663v1

Motivation

A version of group cohomology for locally compact groups and Polish modules has previously been developed using a bar resolution restricted to measurable cochains. That theory was shown to enjoy analogs of most of the standard algebraic properties of group cohomology, but various analytic features of those cohomology groups were only partially understood. This paper re-examines some of those issues. At its heart is a simple dimension-shifting argument which enables one to `regularize' measurable cocycles, leading to some simplifications in the description of the cohomology groups. A range of consequences are then derived from this argument. First, we prove that for target modules that are Fréchet spaces, the cohomology groups agree with those defined using continuous cocycles, and hence they vanish in positive degrees when the acting group is compact. Using this, we then show that for Fréchet, discrete or toral modules the cohomology groups are continuous under forming inverse limits of compact base groups, and also under forming direct limits of discrete target modules. Lastly, these results together enable us to establish various circumstances under which the measurable-cochains cohomology groups coincide with others defined using sheaves on a semi-simplicial space associated to the underlying group, or sheaves on a classifying space for that group. We also prove in some cases that the natural quotient topologies on the measurable-cochains cohomology groups are Hausdorff.

This mission is the statement-level formalization of Continuity properties of measurable group cohomology (arXiv:1004.4937v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem A: Frechet continuous and measurable comparison (Theorem A: continuous/measurable Frechet comparison (paper seed), 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

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

• Theorem B: compact base inverse-limit continuity: Compact inverse systems, their actual inflation maps and direct-limit comparison (hard)
• Theorem D: Hausdorff quotient topologies and structure: Convergence-in-probability cochain topology and actual cohomology quotient groups (source-ambiguity)
• Theorem E: measurable, sheaf, Segal and classifying comparisons: Canonical semi-simplicial sheaf, Segal and classifying-space cohomology and comparison maps (hard)
• Lemma 32: compact quotient lifting (cited background): Compact lifting for a closed Polish Abelian subgroup quotient (hard)
• Lemma 52: converting regularity: A full epsilon-dependent witness modulus for uniform and smallness regularity (source-ambiguity)
• Lemma 53: clopen coboundaries (corrected): Cocycle-subspace probability topology, clopen boundaries and the topological quotient (source-ambiguity)
• Proposition 54: inverse limits with common regularity data: Compact inverse-limit inflation comparison with common complete regularity witnesses (source-ambiguity)
• Corollary 55: compact discrete/toral quotient topology: The measurable cohomology quotient topology for compact discrete/toral modules (source-ambiguity)
• Proposition 58: degree-three inflation non-surjectivity: Torus-product inflation maps and their degree-three cohomology classes (source-ambiguity)
• Proposition 61: compact/discrete comparison: Natural compact/discrete sheaf and classifying-space comparisons (hard)
• Proposition 62: connected-group comparison: The natural degree-preserving sheaf-to-measurable comparison alpha (hard)
• Proposition 71: Euclidean quotient cohomology: Probability-topology cocycles/boundaries and finite-dimensional quotient topology (hard)
• Proposition 72: countable discrete quotient cohomology: Closed boundary subgroup and countable discrete quotient cohomology (hard)
• Proposition 75: toral quotient cohomology: Toral topological cohomology quotient and its discrete-times-Euclidean structure (source-ambiguity)
• Corollary 76: trivial-action locally contractible coefficients: Locally contractible trivial-action coefficient class and actual quotient decomposition (source-ambiguity)
• Lemma 77: non-Hausdorff example: The explicit twisted real module and its non-Hausdorff quotient cohomology (hard)
• Proposition 91: totally disconnected measurable singular comparison: Staged Borel singular cochains on BG and their cohomology comparison (hard)
• Proposition 94: semi-algebraic representatives: Finite-image semi-algebraic cochains factoring through unitary representations (hard)
• Unnumbered §1.3: compact coefficient counterexample: Countable torus identity cocycle and its finite-projection inflation classes (hard)
• Unnumbered remark after C: varying kernel invariants: Kernel-fixed coefficient submodules with descended actions and mixed inflation/inclusion map (hard)
• Unnumbered §4: circle/integer comparison failure: Computed measurable circle/integer cohomology group and continuous quotient (hard)
• Unnumbered §5.2: degree-one limit remark (scope deferred): Unspecified coefficient scope for the degree-one inflation assertion (source-ambiguity)
• Unnumbered §6.1: natural comparison diagram: All actual natural maps in the continuous/sheaf/measurable/classifying diagram (hard)
• Unnumbered §6.2: totally disconnected comparison: Actual continuous/measurable/sheaf comparison maps for arbitrary Polish actions (hard)
• Unnumbered §8: compact comparison counterexample: The explicit coordinate-doubling extension class and its finite-stage images (hard)
• Unnumbered §9.1: invariant singular comparison and map: Staged invariant Borel singular complex, actual chain maps and chain homotopies (hard)
• Unnumbered §9.2: ordinary singular theory loses topology: Milnor classifying spaces and ordinary versus measurable singular cohomology (hard)
• Unnumbered §9.2: circle with real coefficients: Actual ordinary spatial H^2 of BT alongside Moore cohomology (hard)
• Unnumbered §9.2: discrete-real coefficient exception: Non-Polish Borel-cochain quotient for discrete real coefficients (hard)
• Unnumbered final refinement: Lie scope deferred: Unpinned compactness and algebraic-model scope of the final display (source-ambiguity)

Selected references

• Continuity properties of measurable group cohomology, arXiv:1004.4937v4, https://arxiv.org/abs/1004.4937v4

Motivation

We establish a relation between smooth 2-functors defined on the path 2-groupoid of a smooth manifold and differential forms on this manifold. This relation can be understood as a part of a dictionary between fundamental notions from category theory and differential geometry. We show that smooth 2-functors appear in several fields, namely as connections on (non-abelian) gerbes, as curvatures of smooth functors and as critical points in BF theory. We demonstrate further that our dictionary provides a powerful tool to discuss the transgression of geometric objects to loop spaces.

This mission is the statement-level formalization of Smooth Functors vs. Differential Forms (arXiv:0802.0663v4). 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 2.4: bigon quotient plot criterion (Lemma 2.4, 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

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

• Proposition 1.7: naturality under smooth pullback: The particular degree-one differentiation/integration functors, smooth-map pullbacks, and their action on morphisms (hard)
• Section 2.1, unnumbered: the actual path 2-groupoid: Rank-one path quotient, rank-two cube quotient with rank-one boundary faces, and descended gluing (hard)
• Lemma 2.6: extraction is smooth and independent of the parametrizing surface: Canonical standard-plane bigon family, smooth strict transport 2-functor, and identity-based mixed tangent derivative (hard)
• Lemma 2.7: the extracted map is a two-form: Raw extraction map alpha_F from the negative mixed derivative on the tangent fibre product (hard)
• Proposition 2.8: extracted forms satisfy fake-flatness: Actual extracted smooth forms A,B, their manifold exterior derivative, and differentiated crossed-module map (hard)
• Lemma 2.9: the auxiliary semidirect functor: Actual smooth pseudonatural transformation and the specific inverse-H semidirect path assignment (hard)
• Proposition 2.10: differentiated pseudonatural gauge equations: Differentiation of pseudonatural transformations, right Maurer-Cartan form, and bilinear infinitesimal action wedge (hard)
• Proposition 2.11: differentiated modification equations: Differentiation of genuine modifications and the derivative of right-translated alpha_a (hard)
• Section 2.2.4: differentiation respects the complete 2-category structure: The independently defined smooth-functor and differential-form 2-categories and the specific extraction at all three levels (hard)
• Proposition 2.14: smooth surface transport and its infinitesimal value: The iterated right-invariant ODE-defined surface transport k_A,B (hard)
• Lemma 2.15: vertical and auxiliary horizontal composition: Specific integrated k_A,B and auxiliary horizontal bigon gluing star (hard)
• Lemma 2.16: thin-invariance of integrated surface transport: Actual integrated k_A,B and the rank-two cube thin relation with rank-one boundary faces (hard)
• Proposition 2.17: reconstruction is a smooth 2-functor: The particular reconstructed F_A and k_A,B descended to actual path/bigon quotients (hard)
• Lemma 2.18: reconstructed transformation has the right target: ODE-reconstructed h as the H-projection of P(A_prime,phi) (hard)
• Lemma 2.19: reconstructed transformation respects every bigon: The particular reconstructed h components and surface transports at the two endpoints (hard)
• Lemma 2.20: reconstructed modification respects every path: Actual reconstructed transformation components and a differential modification with common target connection (hard)
• Section 2.3.4: integration respects the complete 2-category structure: The specific iterated integration 2-functor on objects, transformations and modifications (hard)
• Theorem 2.21: smooth 2-functors and differential forms are isomorphic 2-categories: Complete specified D and P between independently constructed full 2-categories (hard)
• Example 3.2: the trivial abelian specialization: The actual smooth 2-functor space for BBU(1) and its extracted/integrated two-form (hard)
• Example 3.3 and unnumbered three-way surface-holonomy criterion: Actual Lie automorphism group and independently defined Breen-Messing connection data and 2-functorial holonomy (hard)
• Section 3.2, unnumbered: the canonical derivative 2-functor: The actual path 2-groupoid, delooping BEG, and canonical extension of each path functor (hard)
• Theorem 3.4: non-abelian Stokes for functors, corrected boundary order: The canonical derivative functor and corrected target-based boundary on actual bigon classes (hard)
• Lemma 3.5: the derivative 2-form is ordinary curvature: Forms extracted from the actual derivative dF and from its given F (hard)
• Corollary 3.6: path-ordered curvature expression for holonomy: Corollary 3.6: path-ordered curvature expression for holonomy with a consistent source statement (source-ambiguity)
• Proposition 3.7: BF critical points versus smooth 2-functors: Proposition 3.7: BF critical points versus smooth 2-functors with a consistent source statement (source-ambiguity)
• Lemma 4.2: rank detected by vanishing pullbacks: Global smooth manifold (k+1)-forms and their actual pullback (hard)
• Lemma 4.5: diffeological path groupoid laws: Plotwise differential two-forms, all-form thin homotopy and its actual equivalence relation (hard)
• Lemma 4.6: plotwise integration is a smooth functor: Plotwise one-form data, actual path quotient, and locally smooth ODE transport on families (hard)
• Theorem 4.7: diffeological functors and one-forms: Full diffeological one-form and smooth-functor categories and their specified plotwise D,P (hard)
• Section 4.2, unnumbered: loop evaluation is holonomy: The functional loop diffeology, sitting loop-to-path map, and ODE/bundle holonomy comparison (hard)
• Lemma 4.9: loop-path bigons vary diffeologically: Functional loop/path diffeologies and the computed quotient bigon m(gamma) (hard)
• Section 4.2, unnumbered: the loop-space path functor: The actual loop-space path quotient, relative arrow category, and ell on all levels (hard)
• Section 4.2, unnumbered: the asserted arrow-groupoid trivialization: Section 4.2, unnumbered: the asserted arrow-groupoid trivialization with a consistent source statement (source-ambiguity)
• Section 4.2, unnumbered: induced loop-space structure: The actual square-to-semidirect projection q and its differentiated loop-space forms (hard)
• Proposition 4.10: explicit transgression formulas: Actual induced H2 one-forms and the cut-interval twisted transgression integral (hard)
• Section 4.2, unnumbered: abelian transgression by the loop functor: The actual abelian loop transport functor and untwisted oriented-circle fibre integral (hard)
• Example A.10: the smooth automorphism crossed module: The finite-dimensional smooth Lie structure on the actual automorphism group of connected H (hard)
• Lemma A.11: cube-boundary holonomy and three-curvature: Lemma A.11: cube-boundary holonomy and three-curvature with a consistent source statement (source-ambiguity)

Selected references

• Smooth Functors vs. Differential Forms, arXiv:0802.0663v4, https://arxiv.org/abs/0802.0663v4

Motivation

A host algebra of a topological group G is a C^-algebra whose representations are in one-to-one correspondence with certain continuous unitary representations of G. In this paper we present an approach to host algebras for infinite dimensional Lie groups which is based on complex involutive semigroups. Any locally bounded absolute value αon such a semigroup S leads in a natural way to a C^-algebra C^(S,α), and we describe a setting which permits us to conclude that this C^-algebra is a host algebra for a Lie group G. We further explain how to attach to any such host algebra an invariant weak-*-closed convex set in the dual of the Lie algebra of G enjoying certain nice convex geometric properties. If G is the additive group of a locally convex space, we describe all host algebras arising this way. The general non-commutative case is left for the future.

This mission is the statement-level formalization of A complex semigroup approach to group algebras of infinite dimensional Lie groups (arXiv:0709.1062v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

8 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 4.1 (Proposition 4.1, 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

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

• Theorem 1.5: Canonical weighted semigroup C*-completion and its delta map (hard)
• Lemma 1.8: Complex locally convex manifold holomorphy into operator-norm Banach spaces (hard)
• Proposition 2.3: Holomorphic semigroup multiplier monoid and canonical C*-completion (hard)
• Proposition 2.9: Locally exponential complex Lie groups with real-form conjugation and host axioms (hard)
• Proposition 2.19: Constructed host-semigroup action and host-algebra H1/H2 (hard)
• Example 2.10: Complexified locally convex tube with its actual translation host structure (hard)
• Remark 3.1: Full locally compact group C*-algebra and strict integrated-action correspondence (hard)
• Remark 3.3: Finite-dimensional strict smoothness through genuine Lie orbit maps (hard)
• Remark 3.5: Smooth-vector transport by canonical multiplier representations (hard)
• Lemma 3.6: Derived operators on the actual smooth domain, unbounded adjoints and generators (hard)
• Lemma 3.7: Momentum set and spectrum of the unbounded selfadjoint Stone generator (hard)
• Proposition 3.10: Spectral quotient factorization, smooth-state momentum and strict half-plane extension (hard)
• Remark 3.11: Continuous multiplier subalgebra and induced holomorphic half-plane extension (hard)
• Proposition 3.12: Canonical host momentum support and continuous Exp (hard)
• Lemma 4.3: Convention for a compact equicontinuous base of the zero cone (source-ambiguity)
• Theorem 5.1: Canonical tube completion and character isomorphism with C0(C) (hard)
• Tube classification, unnumbered: All-tube character classification and host representation correspondence (hard)
• Theorem 6.2: Full group C*-quotient and momentum-annihilator quotient with polar diffeomorphism (hard)

Selected references

• A complex semigroup approach to group algebras of infinite dimensional Lie groups, arXiv:0709.1062v1, https://arxiv.org/abs/0709.1062v1

Motivation

In their seminal work on authentication, Wegman and Carter propose that to authenticate multiple messages, it is sufficient to reuse the same hash function as long as each tag is encrypted with a one-time pad. They argue that because the one-time pad is perfectly hiding, the hash function used remains completely unknown to the adversary. Since their proof is not composable, we revisit it using a composable security framework. It turns out that the above argument is insufficient: if the adversary learns whether a corrupted message was accepted or rejected, information about the hash function is leaked, and after a bounded finite amount of rounds it is completely known. We show however that this leak is very small: Wegman and Carter's protocol is still $ε$-secure, if $ε$-almost strongly universal$_2$ hash functions are used. This implies that the secret key corresponding to the choice of hash function can be reused in the next round of authentication without any additional error than this $ε$. We also show that if the players have a mild form of synchronization, namely that the receiver knows when a message should be received, the key can be recycled for any arbitrary task, not only new rounds of authentication.

This mission is the statement-level formalization of Key recycling in authentication (arXiv:1202.1229v3). 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 One-message authentication with arbitrary key recycling (Theorem 5, PDF p. 11). 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

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

• Section 1.2, unnumbered QKD composition consequence: A compatible QKD resource interface and an executed bit-reserve converter routing fresh authentication pads, feeding subsequent QKD rounds, and retaining unused outputs with abort/length histories. (hard)

Selected references

• Key recycling in authentication, arXiv:1202.1229v3, https://arxiv.org/abs/1202.1229v3

Motivation

We prove that the center of each degenerate cyclotomic Hecke algebra associated to the complex reflection group of type B_d(l) consists of symmetric polynomials in its commuting generators. The classification of the blocks of the degenerate cyclotomic Hecke algebras is an easy consequence. We then deduce that the center of an integral block of parabolic category O for the Lie algebra gl_n(C) is generated by the center of its universal enveloping algebra.

This mission is the statement-level formalization of Centers of degenerate cyclotomic Hecke algebras and parabolic category O (arXiv:math/0607717v3). 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 Symmetric-polynomial center and explicit multipartition basis (Theorem 1, 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

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

• Theorem 2: Integral parabolic category O and its natural center multiplication map (hard)
• Lemma 3.1: Filtered PBW symbol interface (hard)
• Theorem 3.2: Filtered PBW symbol interface (hard)
• Lemma 4.1: Generic complete-local deformation and modular dual Specht modules (hard)
• Lemma 4.2: Evaluation central characters and repeated shape-residue multisets (hard)
• Theorem 4.3: Primitive central idempotents and unital block corner centers (hard)
• Lemma 5.1: Ordered determinant central coefficients and actual comultiplication delta (hard)
• Lemma 5.2: Cyclic highest-weight modules and the concrete right affine-Hecke tensor action (hard)
• Corollary 5.3: Natural central and right Murphy actions in the same opposite endomorphism algebra (hard)
• Lemma 5.4: Character-difference multiset map and blockwise staircase multipartition map (hard)
• Lemma 5.5: Projective tensor modules for reordered compositions and action-compatible endomorphism isomorphism (hard)
• Theorem 5.6: Actual Schur-Weyl tensor representation and residue-selected block sum (hard)
• Corollary 5.7: Central determinant actions in the concrete tensor endomorphism algebra (hard)
• Lemma 5.8: Generalized-character tensor projection and represented block idempotent (hard)
• Corollary 5.9: Restricted block tensor action with center generators and O-simple count (hard)
• Lemma 5.10: Parabolic Verma flags and injective hulls internal to the O block (hard)
• Theorem 5.11: All three natural center maps and evaluation on the projected tensor module (hard)
• §1, unnumbered: central-character subcategories are blocks: Actual nonsplit-extension linkage in integral parabolic O (hard)
• §4, unnumbered: residue classification of blocks: Actual simple-module extension linkage and residue-selected block summands (hard)
• §4, unnumbered: central character of dual Specht modules: Modular induced dual Specht modules and their central actions (hard)
• §5, unnumbered: constituents of the projective tensor module: Simple highest-weight subquotients of the concrete projective tensor module (hard)
• §5, unnumbered: determinant translation to tensor blocks: Actual determinant tensor functor and transported central-character action (hard)

Selected references

• Centers of degenerate cyclotomic Hecke algebras and parabolic category O, arXiv:math/0607717v3, https://arxiv.org/abs/math/0607717v3

Motivation

We give the first composable security proof for continuous-variable quantum key distribution with coherent states against collective attacks. Crucially, in the limit of large blocks the secret key rate converges to the usual value computed from the Holevo bound. Combining our proof with either the de Finetti theorem or the Postselection technique then shows the security of the protocol against general attacks, thereby confirming the long-standing conjecture that Gaussian attacks are optimal asymptotically in the composable security framework. We expect that our parameter estimation procedure, which does not rely on any assumption, will find applications elsewhere, for instance for the reliable quantification of continuous-variable entanglement in finite-size settings.

This mission is the statement-level formalization of Composable security proof for continuous-variable quantum key distribution with coherent states (arXiv:1408.5689v3). 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 Lemma 7: Haar complex half-projection norm concentration (Lemma 7, E2–E3, PDF p. 20). 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

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

• Seed paper result pinned to Theorem 1: collective-attack composable security: Complete finite-precision E0 CPTP protocol and full transcript leakage/error budget (source-ambiguity)
• Theorem 2: PE acceptance and Holevo underestimation: Outcome-indexed residual quantum state and PE underestimation event (source-ambiguity)
• Theorem 3: appendix restatement of the finite-key security bound: Complete finite-precision E0 CPTP protocol and full transcript leakage/error budget (source-ambiguity)
• Theorem 4: AEP for a conditional state: Separable-memory optimized purified-distance smooth conditional min-entropy and actual commuting postselection (hard)
• Theorem 12: virtual-PE bad-event union bound: Well-defined conditioning and valid nonnegative-variable application for signed correlations (source-ambiguity)
• Corollary 13: PE passes but Eve information is underestimated: The same actual PE residual-state bad-event probability space as Theorem 2 (source-ambiguity)
• Unnumbered main result: asymptotic Gaussian Holevo key rate: Complete protocol family with discretization, reconciliation, transcript and robustness limit (source-ambiguity)
• Unnumbered main result: general-attack upgrade: Instantiated CV energy-test/postselection protocol, dimension, shortening and joint budget (source-ambiguity)
• Appendix G: direct reconciliation without active symmetrization: Complementary cross energy-test instruments and combined key operation (source-ambiguity)
• Unnumbered result: coherent-state PM/EB equivalence: One consistent TMSV/coherent/heterodyne quadrature and modulation normalization (source-ambiguity)
• Unnumbered result: PE simulation without optical symmetrization or extra parties: Exact virtual-PE simulation algorithm, output law and complexity model (source-ambiguity)
• D24–D25: positive AEP correction with lower-bounded passing probability: The same complete separable-memory postselection entropy interface, at block size 2n (hard)
• D30–D33: entropy inference conditioned on acceptance: Consistent conditional word entropy normalization and concentration failure parameter (source-ambiguity)
• D34–D38: Gaussian phase invariance and three-parameter heterodyne Holevo comparison: Actual two-mode Gaussian purification, continuous heterodyne instrument and measured Eve Holevo comparison (hard)
• E63: Holevo bound after PE acceptance: Outcome-indexed Holevo quantity after PE acceptance, not fixed-state exceptional probability (source-ambiguity)
• F6: smooth min-entropy bound after EC and PE acceptance: Complete accepted-protocol conditional cq entropy and full transcript leakage accounting (source-ambiguity)
• Appendix C: expected rate and claimed 0.99 robustness: Rigorous joint robustness quantile and consistent SNR/key-length model (source-ambiguity)

Selected references

• Composable security proof for continuous-variable quantum key distribution with coherent states, arXiv:1408.5689v3, https://arxiv.org/abs/1408.5689v3

Communication in two-sided marketplaces

A platform may know the services its users seek and offer while still lacking the preferences that determine whether a particular match is worthwhile. Learning those preferences requires communication. A lower bound on that communication would distinguish a limitation of one search algorithm from a limitation shared by every platform design. Peng Shi's Optimal Matchmaking Strategy in Two-Sided Marketplaces studies this question through assignment markets with privately known benefits and costs. The present target is Proposition 12, which supplies the communication lower bounds summarized in the paper's Table 4. Its two numbered supporting lemmas are included; independent upper bounds are outside this mission.

The targets preserve the source's literal communication model. A finding about that model is consequential: observing boundaries between arbitrarily short messages can reveal information that is not charged as bits. The printed unrestricted lower bounds and their supporting information lemmas are therefore retained as source claims to be assessed, rather than presented as established machine-checked results. The detailed counterexamples and source locations accompany the mission in its findings.

Assignment outcomes and private messages

An assignment game has a set of customers $I$ and a distinct set of providers $J$, both of size $n$. Customer $i$ receives benefit $b_{ij}$ from provider $j$'s service, whose cost is $c_{ij}$. Each agent can have at most one partner. A transaction outcome consists of a binary matching $x$ and real prices $p_i$ paid by customers. Unmatched customers pay zero. In a matched pair, the customer's surplus is $u_i=b_{ij}-p_i$ and the provider's is $v_j=p_i-c_{ij}$; unmatched agents have zero surplus.

For a tolerance $\epsilon>0$, an outcome is $\epsilon$-stable when every agent's surplus is nonnegative and

$$u_i+v_j+2\epsilon\ge b_{ij}-c_{ij}\qquad(i\in I,\ j\in J).$$

The condition concerns every pair, including pairs absent from the matching. It expresses that a pair cannot deviate and improve both participants' surpluses by more than $\epsilon$. These are the transaction and stability conventions of §§2.1–2.3, pages 7–9 of the supplied artifact.

The binary market $M(n,d^I,d^J)$ draws every benefit independently as $.99$ with probability $d^I$, and zero otherwise. Independently, every cost is $.01$ with probability $d^J$, and one otherwise. Customer $i$ initially knows only her benefit row; provider $j$ knows only his cost column. The distributions and market size are public. A blackboard protocol starts with a fixed speaker. Each message is a finite binary string determined by its sender's private input and the history of complete messages. A public deterministic controller uses that history to select the next speaker or terminate with a transaction outcome.

Only the bits in the messages are charged. Messages may be empty, and there is no limit on rounds or computation. Protocols must terminate on every supported input. The per-agent communication cost is the maximum total bit count on this support divided by $2n$. A one-round protocol requires each agent's single message to depend only on that agent's private input, with the output determined by the tuple of messages. These definitions follow Definitions 3–5, pages 23–25.

Formalization targets

Proposition 12 asserts the existence of universal constants $\kappa_1,\kappa_2,\kappa_3>0$. For every $n\ge64$ and $0<\epsilon<.49$, a protocol with probability at least $.99$ of returning an $\epsilon$-stable outcome must satisfy all applicable bounds:

$$\begin{aligned} \operatorname{cost}(P)&\ge\kappa_1\log n &&\text{in }M(n,1/n,1),\\ \operatorname{cost}(P)&\ge\kappa_2/d^J &&\text{in }M(n,1/(nd^J),d^J),\quad d^J\in[1/\sqrt n,1/2],\\ \operatorname{cost}(P)&\ge\kappa_3\log n &&\text{in }M(n,.5,.5)\text{ for one-round }P. \end{aligned}$$

The constants precede all market and protocol quantifiers. The entire conjunction is the goal, as printed on page 26.

For the milestones, let $\Pi$ be the concatenation of all bits communicated before termination. A pair is good when its benefit is $.99$ and cost $.01$, and perfect when it is good and no other good pair shares either endpoint. Write their indicators as $G_{ij},P_{ij}$, and let $x_{ij}$ be the run's output matching indicator. A low-error pair satisfies

$$\mathbb E[P_{ij}(1-x_{ij})+(1-G_{ij})x_{ij}]\le .04/n.$$

The expectation is unconditional; the set of low-error pairs is fixed before the profile is sampled.

Lemma D.3, page 43, considers the laws $\pi_{11},\pi_{10},\pi_{01},\pi_{00}$ of $\Pi$ conditional on the pair's two flags. In the second market regime it asserts

$$\tfrac12\|\pi_{11}-\pi_{00}\|_1\le\|\pi_{10}-\pi_{00}\|_1+\|\pi_{01}-\pi_{00}\|_1.$$

Here the norm is the full sum of absolute mass differences. The formal statement covers every protocol and pair in that regime, so it specializes to the successful protocol and low-error pair in the source's application.

Lemma D.2, page 41, fixes a low-error pair in a protocol with success probability at least $.99$ and $d^Id^J=1/n$. It asserts both strict inequalities:

$$I(b_{ij},c_{ij};\Pi)>.05\log_2(n)/n\quad(d^J=1),$$ $$I(b_{ij},c_{ij};\Pi)>.0004/(nd^J)\quad(d^J\in[1/\sqrt n,1/2]).$$

Mutual information is measured in bits. The milestone order is D.3, then D.2; the one-round clause uses the separate argument in Appendix D.6.

Significance and status

The claimed bounds distinguish markets where one side has easy-to-describe preferences, sparse reciprocal interest, and simultaneous communication. In particular, setting $d^J=1/\sqrt n$ in the second clause gives the claimed square-root worst-case scale. Their universal protocol quantifiers are central to the paper's near-optimality comparison.

The formalization makes the protocol's information access, transfer feasibility, and cost accounting explicit. Its general communication and assignment objects are reusable independently of the binary market. Definitions are concrete, and the theorem declarations are unproved statement targets. Compilation checks their well-formedness; it does not establish their truth. The literal-model finding remains relevant to resolving those targets.

The coding-model difficulty

The observable message history and its flattened bit transcript are different random variables. The source defines the latter explicitly in Appendix D.5, but treats it as if it also determines the output and has the information properties of a fully observable history. Under Definition 3, arbitrary empty messages can encode private information at no additional bit cost. The recorded instance yields cost one and exact stability, while its concatenated transcript is constant. This contradicts the unrestricted claims and the positive information bounds. A related instance makes the rectangle inequality read $1\le0$.

Adding prefix-free or nonempty-message restrictions would change the targets' domain. The mission therefore retains the printed class and records the defect. This finding does not disprove the one-round clause. Separately, the proof's use of $L/n$ conflicts with Definition 3's $L/(2n)$; the formal cost follows the definition.

Formalization scope

The two populations are tagged copies of Fin n. Boolean profiles are exact encodings of the binary preferences, while prices, tolerance, and density parameters remain real. The distribution is its full independent product mass. Finite sums compute probabilities, conditional laws, and mutual information over the distinct transcript values. Zero-mass profiles affect neither probability nor the supported maximum cost. All conditioning events used in D.3 are positive.

The controller observes lists of messages, and outcomes are computed from actual terminating runs. No entropy bound, factorization property, or transcript decoder is an admissibility assumption. Natural logarithms in Proposition 12 only rescale its existential constants; D.2 uses base two with its exact explicit constants. Every $n\ge64$ and both density interval endpoints are included.

Selected references

• Peng Shi, Optimal Matchmaking Strategy in Two-Sided Marketplaces, Management Science, 2023. DOI: 10.1287/mnsc.2022.4444. Published citation basis; supplied 65-page artifact, Proposition 12 on page 26 and Lemmas D.2–D.3 on pages 41 and 43. PDF and printed page numbers coincide.

Why characterize the Shannon entropy

The Shannon information function $H(p) = -\sum_i p_i \ln p_i$ measures the average information gained when one samples a discrete probability distribution $p$. Its use as a measure of distinguishability (the mutual information of Chapter 2 of C. A. Fuchs's thesis, arXiv:quant-ph/9601020) is only as convincing as the reasons for the formula itself. Section 2.4.1 of the thesis derives the formula from two requirements on an information function: it depends only on the probabilities and not on how outcomes are labelled (symmetry), and the expected information gained does not depend on the order in which an observer asks about the outcome (objectivity). The derivation follows Z. Daróczy (Information and Control 16, 1970), who embeds the problem in a one-parameter family of functional equations whose solutions are explicit, and recovers Shannon's formula as the limit $\alpha \to 1$.

Characterizations of this kind go back to Shannon (1948), Khinchin (1953) and Faddeev (1956), who used continuity or monotonicity assumptions. Daróczy's route needs no regularity hypothesis on $H$ at all: symmetry and the recursion of type $\alpha$ already force a closed form, and the regularity enters only through the limit in $\alpha$. This mission formalizes that derivation as Fuchs presents it (Theorem 2.7, printed pp.32–35).

Setting

For $n \ge 1$ let

$$\Gamma_n = \Big\{ (p_1,\dots,p_n) \;\Big|\; p_k \ge 0,\ \sum_{i=1}^n p_i = 1 \Big\}$$

be the $n$-point probability distributions and $\Gamma = \bigcup_n \Gamma_n$. In Lean, IsDist p says that p : Fin n → ℝ lies in $\Gamma_n$.

A function $H : \Gamma \to \mathbb R$ is a family $H_n$ of functions of $n$ real arguments. It is symmetric (IsSymmetric H) if $H(p_{\sigma(1)},\dots,p_{\sigma(n)}) = H(p_1,\dots,p_n)$ for every permutation $\sigma$ and every $p \in \Gamma_n$.

Fix a real parameter $\alpha > 0$, $\alpha \ne 1$. A function $H_\alpha$ satisfies the recursion of type $\alpha$ (SatisfiesRecursion α H), Eq. (2.111), if for every $n \ge 2$ and $p \in \Gamma_n$ with $p_1 + p_2 > 0$,

$$H_\alpha(p_1,\dots,p_n) = H_\alpha(p_1+p_2, p_3,\dots,p_n) + (p_1+p_2)^{\alpha}\, H_\alpha\!\Big(\frac{p_1}{p_1+p_2}, \frac{p_2}{p_1+p_2}\Big).$$

At $\alpha = 1$ this is the objectivity requirement (2.110). Throughout the proof, $f(x) = H_\alpha(x, 1-x)$ for $0 \le x \le 1$ (2.114), and $s_i = p_1 + \dots + p_i$.

Formalization targets

Goal: Theorem 2.7 (Daróczy)

Let $(H_\alpha)_{\alpha > 0,\ \alpha \ne 1}$ be symmetric solutions of the recursion of type $\alpha$, and suppose $H_\alpha(\tfrac12,\tfrac12) \to C$ as $\alpha \to 1$. Then for every $n$ and $p \in \Gamma_n$,

$$\lim_{\alpha \to 1} H_\alpha(p_1,\dots,p_n) = -\frac{C}{\ln 2}\sum_{i=1}^n p_i \ln p_i, \qquad 0 \ln 0 = 0.$$

The constant $C$ fixes the units: $C = 1$ for bits, $C = \ln 2$ for nats.

Milestones (fixed $\alpha > 0$, $\alpha \ne 1$; $H_\alpha$ symmetric and satisfying (2.111))

1. (2.115) $H_\alpha(p_1,\dots,p_n) = \sum_{i=2}^n s_i^\alpha f(p_i/s_i)$.
2. (2.119) $f(x) + (1-x)^\alpha f\big(\tfrac{y}{1-x}\big) = f(y) + (1-y)^\alpha f\big(\tfrac{x}{1-y}\big)$ for $x, y \in [0,1)$, $x + y \le 1$.
3. (2.120) $f(0) = f(1) = 0$.
4. (2.122) $F(p,q) = f(p) + [p^\alpha + (1-p)^\alpha] f(q)$ satisfies $F(p,q) = F(q,p)$ on $[0,1]^2$.
5. (2.124) $f(p) = C(2^{1-\alpha}-1)^{-1}[p^\alpha + (1-p)^\alpha - 1]$ on $[0,1]$, $C = f(\tfrac12)$.
6. (2.130) $H_\alpha(p) = C(2^{1-\alpha}-1)^{-1}\big(\sum_{i=1}^n p_i^\alpha - 1\big)$ on every $\Gamma_n$, $C = H_\alpha(\tfrac12,\tfrac12)$.

Significance

The result singles out the Shannon entropy among all symmetric information functions by a purely algebraic requirement, with no continuity, monotonicity or measurability assumption on $H_\alpha$. Milestone (2.130) is of independent interest: it shows that the symmetric solutions of the recursion of type $\alpha$ are exactly the multiples of the Daróczy information of type $\alpha$, $(2^{1-\alpha}-1)^{-1}(\sum_i p_i^\alpha - 1)$ (known in physics as the Tsallis entropy), which is related to the Rényi information of order $\alpha$ by (2.132). The goal then identifies the Shannon entropy as its $\alpha \to 1$ limit, which fixes the information function used for the mutual-information distinguishability measure in the rest of the thesis.

The theorem is classical and its proof in the thesis is complete; none of these statements is formalized on the platform, and Mathlib contains the Shannon entropy only in the form of Real.negMulLog and binary entropy, without a characterization theorem. This mission produces a machine-checked characterization of the Shannon and Daróczy entropies from symmetry and recursivity, reusable by any development that needs to justify an entropy formula axiomatically.

Difficulty

Each step is elementary, but several are easy to get wrong. The reduction (2.115) iterates the recursion, which only applies when the first two entries are not both zero; distributions that begin with zeros must first be permuted using symmetry. The symmetry of $F$ (2.122) needs the substitution $p = 1 - x$, $q = y/(1-x)$ and then a second substitution $z = (1-p)/(1-pq)$ (2.127), each valid only away from the endpoints, so the boundary cases $p, q \in \{0, 1\}$ must be handled separately with $f(0) = f(1) = 0$. The final limit is a $0/0$ form in $\alpha$; the thesis applies l'Hôpital's rule (its display (2.131) prints $\alpha \to 0$, a misprint for $\alpha \to 1$), and entries $p_i = 0$ must be checked to contribute $0$ on both sides.

Formalization scope

• A function on $\Gamma$ is H : (n : ℕ) → (Fin n → ℝ) → ℝ; its values off $\Gamma_n$ are irrelevant. The family in the goal is H : ℝ → (n : ℕ) → (Fin n → ℝ) → ℝ, with symmetry and the recursion assumed for every $\alpha > 0$, $\alpha \ne 1$.
• Indices are 0-based: the source's $p_1, p_2$ are p 0, p 1, and the merged vector $(p_1+p_2, p_3,\dots,p_n)$ is Fin.cons (p 0 + p 1) (fun i => p i.succ.succ).
• The recursion is required only where its right side is defined, $p_1 + p_2 > 0$; Lean's 0 / 0 = 0 imposes no extra condition on $H$.
• Powers are Real.rpow, so $0^\alpha = 0$ for $\alpha > 0$; logarithms are natural (Real.log), and Real.log 0 = 0 gives $0 \ln 0 = 0$.
• The limit is along 𝓝[≠] 1. "Up to a constant $C$" is read as: if $H_\alpha(\tfrac12,\tfrac12) \to C$ then $H_\alpha(p) \to -(C/\ln 2)\sum_i p_i \ln p_i$; a family with constant $H_\alpha(\tfrac12,\tfrac12) = C$ is a special case.
• A trivial formalization is ruled out: the hypotheses are satisfied by the nonzero Daróczy family for every $\alpha$ (checked in a verification file), and the constant function $1$ violates the recursion.

Needed infrastructure: finite sums over Fin n with Fin.cons/Fin.succ reindexing, permutations of Fin n, Real.rpow identities $(st)^\alpha = s^\alpha t^\alpha$ for $s, t \ge 0$, and one-sided derivatives of $\alpha \mapsto a^\alpha$ for the limit. Proofs of any milestone, and alternative routes to the goal through (2.130), are welcome.

Selected references

• C. A. Fuchs, Distinguishability and Accessible Information in Quantum Theory, PhD dissertation, University of New Mexico, 1995. arXiv:quant-ph/9601020v1
• Z. Daróczy, Generalized information functions, Information and Control 16 (1970) 36–51. doi:10.1016/S0019-9958(70)80040-7
• J. Aczél and Z. Daróczy, On Measures of Information and Their Characterizations, Academic Press, 1975.
• C. E. Shannon, A mathematical theory of communication, Bell System Technical Journal 27 (1948) 379–423. doi:10.1002/j.1538-7305.1948.tb01338.x