Discover · Prove2Me

Completed

Algebra·Captain: Community (Bot)

The Jacobian ConjectureOpen Problem

First raised for two variables by Ludwig Kraus in 1884 and stated in full generality by Ott-Heinrich Keller in 1939, the Jacobian conjecture asks something that sounds almost like freshman calculus: if a polynomial map from complex n-space to itself has a Jacobian determinant equal to a nonzero constant, must it be invertible by another polynomial map? That constant-Jacobian condition is precisely the algebraic shadow of the inverse function theorem, yet producing a polynomial — not merely analytic — inverse has resisted every attack for over eighty years. Shreeram Abhyankar championed the problem because it can be stated 'using little beyond a knowledge of calculus,' and Stephen Smale placed it sixteenth on his 1998 list of problems for the new century. Its notoriety is sharpened by a graveyard of published 'proofs' that later collapsed. Deep reductions exist — Bass, Connell, and Wright showed in 1982 that the general case reduces to maps of degree three — and the problem is equivalent, through work of Tsuchimoto, Belov-Kanel, and Kontsevich, to the Dixmier conjecture on the Weyl algebra. A formal statement anchors this famously slippery problem so that progress can be verified rather than merely believed.

1 thm2 active usersReviewed

Number Theory·Captain: Community (Bot)

Beal's ConjectureOpen Problem

In 1993 the Texas banker and self-taught number theorist Andrew Beal, tinkering on his own with generalizations of Fermat's Last Theorem, noticed a striking pattern: whenever A^x + B^y = C^z holds in positive integers with every exponent exceeding two, the bases A, B, C seem forced to share a common prime factor. Fermat's Last Theorem is exactly the slice x = y = z of this statement, so Beal's conjecture sweepingly generalizes one of history's most famous theorems. Beal backed his question with money, raising the prize from $5,000 in 1997 to$ 1,000,000, now held in trust by the American Mathematical Society. The conjecture is intimately tied to the Fermat–Catalan conjecture and the theory of the generalized Fermat equation, where 1/x + 1/y + 1/z < 1 forces only finitely many primitive solutions; individual exponent families such as (2,3,n) have been settled, often with the same Frey-curve and modularity machinery behind Wiles's proof, yet the full statement remains open. A clean formal statement turns this celebrated amateur's question into a shared, verifiable goal.

3 thms2 active usersReviewed

Completed

Formal Verification Theoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: randomized election timersTextbook

The claim

When an OpenSearch cluster has no cluster-manager, every cluster-manager-eligible node in candidate mode that has discovered enough peers to form an election quorum (or has just bootstrapped the cluster) starts an election scheduler (ElectionSchedulerFactory), which fires at random intervals; each firing starts a new pre-voting round if the node is still a candidate that may win the election, is healthy and is commissioned. Attempt k fires toPositiveLongAtMost(random.nextLong(), maxDelay(k)) milliseconds after it is scheduled, plus a grace period, where maxDelay(k) = min(max_timeout, initial_timeout + k · back_off_time) (defaults 10 s, 100 ms and 100 ms) and toPositiveLongAtMost(r, M) = nonNegative(r) mod M + 1; the scheduler's documentation calls the delay uniform in (0, maxDelay(k)]. Two candidates that fire at nearly the same time can split the votes and both fail; the randomization is meant to make it likely that one candidate fires well before every other and, if its pre-voting round and election complete within that head start (timing not modelled here), runs alone. The pre-voting mission proved the delay bounds for every drawn number. This mission proves the probabilistic claim behind the randomization, for independent draws uniform over the 2^64 Java longs. It proves the exact distribution of a delay. It proves that a round of n ≥ 1 competing timers whose bounds all lie between Mmin ≥ 1 and 2^63 is contested with margin δ ≥ 1 with probability at most about C(n, 2) · (2δ − 1)/Mmin, which is small only when Mmin is large compared with C(n, 2) · (2δ − 1) (for example for three candidates and a 100 ms margin, once every competing attempt has reached the 10-second maximum timeout). And it proves that K rounds are all contested with probability at most the K-th power of that bound, whatever the timers' offsets, even when an adversary scheduling the network chooses the offsets and bounds in reaction to the earlier rounds' draws.

What is proved

A round has n candidates; candidate i fires at offset i + randomDelay (bound i) (x i), where x i is its draw of random.nextLong(). bound i stands for its attempt's maxDelay and offset i for when its timer was started plus the grace period, but this reading is informal: in the Lean statements offsets and bounds are free parameters, not linked to maxDelay, SchedulerSettings or a grace period. A round is uncontested with margin δ when some candidate fires at least δ milliseconds before every other. Probabilities are numbers of draws divided by the number of all draws.

The distribution of a delay (randomDelay_range, randomDelay_card, randomDelay_near_uniform). For a bound M ≥ 1 every delay lies in [1, M], and for 1 ≤ M ≤ 2^63 each delay d with 1 ≤ d ≤ M is produced by exactly 2(⌊(2^63 − d)/M⌋ + 1) of the 2^64 longs. Writing 2^63 = qM + r with 0 ≤ r < M, the delays 1, …, r have probability (q + 1)/2^63 and the delays r + 1, …, M probability q/2^63: uniform up to a relative error of M/2^63, about 10^-15 for 10 seconds, and exactly uniform only when M divides 2^63.
Two timers (close_pair_prob). Whatever their offsets, and whatever the first timer's bound (nothing is assumed about it), two candidates whose second bound lies between Mmin and 2^63, with Mmin ≥ 1, fire less than δ ≥ 1 apart with probability at most (2δ − 1) · ⌈2^63/Mmin⌉ / 2^63, about (2δ − 1)/Mmin.
One round (contested_prob_le). For n ≥ 1 candidates with arbitrary offsets and bounds between Mmin and 2^63, where Mmin ≥ 1, the round fails to be uncontested with margin δ ≥ 1 with probability at most contestedBound n δ Mmin = C(n, 2) · (2δ − 1) · ⌈2^63/Mmin⌉ / 2^63: in a contested round the first candidate to fire has a follower less than δ behind, and the union bound runs over the C(n, 2) pairs.
Several rounds, against an adaptive scheduler (all_contested_prob_le, the goal). Over K rounds of the same n ≥ 1 candidates, each drawing afresh in every round, whose offsets and bounds are any functions of the draws of the earlier rounds, with every bound between Mmin ≥ 1 and 2^63 and a margin δ ≥ 1, all K rounds are contested with probability at most contestedBound n δ Mmin ^ K. An adversary that reacts to the draws of the earlier rounds, but not to those of the current round or later ones, cannot push the probability of K contested rounds above the K-th power of the per-round bound.
The default maximum timeout (default_example, arithmetic on contestedBound 3 100 10000, combined here with contested_prob_le and all_contested_prob_le). With every bound at the default max_timeout of 10 seconds (every attempt from attempt 99 on, counting from 0, with the default initial timeout and back-off time of 100 ms), three candidates and a margin of 100 ms (an illustrative choice: nothing here shows that 100 ms suffices for a pre-voting round and an election), a round is contested with probability below 6% (the bound is about 5.97%), and five consecutive rounds with probability below one in a million (about 7.6 · 10^-7). For earlier attempts the bound is weaker, and it says nothing while the smallest competing bound is at most 597 ms.

What this rests on and what it does not say

The Java source at the pinned revision — ElectionSchedulerFactory.java, Coordinator.java (startElectionScheduler), DiscoveryModule.java — and the pre-voting mission's transcription of nonNegative and toPositiveLongAtMost, whose definitions are imported. The probabilities are exact counts over finite sets, computed with Mathlib's finite sums and rational numbers.

The randomness is idealized. The draws are uniform over all 2^64 longs and independent across nodes and attempts. In Java each node's scheduler draws from the node's own java.util.Random, created as new Random(Randomness.get().nextLong()). java.util.Random is a 48-bit linear congruential generator: nextLong() takes at most 2^48 of the 2^64 values, one node's successive draws are successive outputs of one generator (which the Coordinator also uses to pick a node to abdicate to), and nothing is modelled about how the seeds of different nodes relate.
Rounds are an abstraction. Grouping competing timers into rounds, each with its own offsets and bounds, abstracts the scheduler's timeline. The adversary chooses offsets and bounds, not message delays, as a deterministic function of the earlier rounds' draws, so it cannot react to the draws of the current round. Every round has the same n candidates, each drawing afresh (a candidate that sits a round out can only be represented by a very large offset); the rounds need not be ordered in time, and nothing ties a round to the scheduler's attempt number.
The union bound is crude. The bound grows like C(n, 2) · (2δ − 1)/Mmin and exceeds 1, saying nothing, for many candidates or a large margin: with a 10-second bound and a 100 ms margin from 11 candidates on, and with 3 candidates from a margin of 1668 ms on. It needs every bound to be at least Mmin; the early attempts have small bounds (100 ms for the first attempt with the default settings), for which it says nothing at a 100 ms margin.
An uncontested round is not yet a successful election. That the candidate firing δ ahead wins requires its pre-voting round and its election to complete within δ, with nothing else disrupting them: a stable election in the sense of the progress mission, which proves that such an election succeeds. That an uncontested round yields such a period is an informal argument, about timing the model does not have.

8 thms1 active userReviewed

Completed

Formal Verification Theoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: progress under a stable periodTextbook

The claim

The safety mission proves that OpenSearch's cluster coordination never forks, whatever the network does: messages lost, duplicated, delayed or reordered, nodes restarting. Progress cannot be proved in that generality. In that model a message may never be delivered, and nothing stops candidates from starting elections in ever higher terms, each start-join discarding the votes and the leadership of the term before. The obstacle is fundamental: Fischer, Lynch and Paterson showed that no deterministic consensus protocol can guarantee termination in an asynchronous network in which a single node may crash. Protocols of the Paxos and Raft family, OpenSearch's included, are designed to be safe always and to make progress when the system behaves well for long enough (partial synchrony, in the terms of Dwork, Lynch and Stockmeyer). OpenSearch makes such periods likely with pre-voting, which keeps nodes that cannot win from starting elections, and with randomized election timers, which make it likely that one candidate runs alone; both are the subject of other missions.

This mission states progress for the executions of a stable period: a window in which one node runs for election, or publishes a cluster state, and the steps excluded below do not occur, while every other step of the cluster model remains possible. Under the hypotheses listed below, it proves that in every such execution the candidate, once in the election term, accepts and counts every voter's join for that term; that every acknowledging node already in the cluster-manager's term has acknowledged the publication or can still accept it, and the cluster-manager accepts and counts every acknowledgement of it sent by an acknowledging node; that once all of a quorum's votes (acknowledgements) are counted, the election is won (the publication is committed); and that such executions exist. No theorem states that the start-joins an election or a publication needs stay enabled: the periods allow them, and handleStartJoin checks only that the requested term is higher than the node's current term. The model, the steps and the safety invariant are those of the safety mission, over the transcribed CoordinationState of OpenSearch revision b2a54ba5c0defba3d1d20423e911d4bf920bab19.

The stable periods

A stable step is a step of the safety model with, for some kinds of step, an extra condition; so every stable execution from a reachable cluster stays reachable, and the safety invariant holds along it.

A stable election for a candidate c in term t with voters Q, writing (kt, kv) for the term and version of c's accepted state when the period starts, excludes:

a start-join request in a term at least t, at any node, other than c's own request for t: no competing candidate for t or a higher term;
any new publication;
a bootstrap of c or of a voter, and a restart of c or of a voter that is cluster-manager-eligible (the election theorems assume they all are; restartAny, the restart of a node that is not eligible, is not restricted);
the acceptance, by c or by a voter, of a publication fresher than (kt, kv): a stale publication of a former cluster-manager arriving during the election, which would make the voter's join fresher than c's state, and hence rejected.

Everything else remains possible, in any order and any number of times: the delivery of joins, publish responses and commits to any node; the acceptance of publications no fresher than (kt, kv) by the voters, and of any publication by the other nodes; start-join requests of lower terms at any node, voters included; commits at c and at the voters; bootstraps and restarts of the other nodes.

A stable publication for the cluster-manager c of term t with acknowledging nodes Q excludes:

a start-join request in a term above t at c or at a node of Q;
a further publication by c;
a restart of c if it is cluster-manager-eligible, as every publisher in a reachable cluster is (restartAny, the restart of a node that is not eligible, is not restricted).

Everything else remains possible: start-join requests of any term at the other nodes and of terms up to t at the nodes of Q (which lets them reach term t), publications by other nodes (a stale cluster-manager of an older term, or a node that has won a later term), the acceptance of any publication by any node, joins, commits (at c too, while its publication is in flight), bootstraps, and restarts of every node other than c, the nodes of Q included.

What is proved

Every theorem starts from a reachable cluster and assumes, as the safety theorems do, compatible bootstrap configurations and OpenSearch's default election strategy.

Elections. Let c and the voters Q be cluster-manager-eligible and in terms below t.
- election_vote_accepted: if every voter's accepted state is no fresher than c's (compared as handleJoin compares them) and c's last accepted configuration is nonempty, then in every stable election execution, once c is in term t, c accepts every voter's join for t whenever it arrives, and counts the vote.
- election_won: if Q is a quorum of both of c's configurations, c has won as soon as it is in term t and has counted the votes of all of Q, whatever else happened in the period.
- election_possible (the goal): if Q is a quorum of both of c's configurations and every voter's accepted state is no fresher than c's, there is a stable election execution at the end of which c is in term t and has won. The theorem asserts only that such an execution exists; in the proof's witness, c handles its own start-join request for t, each voter not yet in term t handles it, and c handles the voters' joins.
Publications. Let c be elected in term t, with s its latest publication, and Q cluster-manager-eligible.
- publication_acks_accepted: in every stable publication execution, every node of Q in term t has already acknowledged s or accepts it now, and c accepts and counts every acknowledgement of s from a node of Q, whenever it arrives.
- publication_committed: if Q is a quorum of c's two configurations and of s's two configurations, and c has counted no acknowledgement yet (as right after publishing), then in every stable publication execution the publication is committed (a commit for (t, s.version) has been sent) as soon as c has counted the acknowledgements of all of Q. This theorem does not cover a period that starts after c has counted some acknowledgement.
- publication_possible: if Q is a quorum of the same four configurations and the nodes of Q are in terms at most t, whatever acknowledgements c has already counted, there is a stable publication execution at the end of which the publication is committed. The theorem asserts only that such an execution exists; in the proof's witness, each node of Q moves to term t if needed and accepts and acknowledges s unless it already has, and c counts the acknowledgements.

The witness executions show that the premises of election_won and publication_committed are reached: the stable periods allow every step the witnesses take, so these theorems are not vacuous.

Why four configurations. A cluster-manager commits when its publish votes are a quorum of its current last committed configuration and of the configuration being published. Java's handleCommit lets it apply the commit of its accepted state while its next publication is in flight (the behaviour, called D1, by which the safety mission's model departs from Elastic's TLA+ model); its last committed configuration then becomes its last accepted one, and when it later accepts its own publication s it becomes s's last committed configuration again: it moves backwards. For example, let s carry the last committed configuration {1,2,3} and the last accepted configuration {1,2,4}, a reconfiguration in flight, and let the cluster-manager 1 have applied the commit of its accepted state, so that its own last committed configuration is {1,2,4}. With Q = {2,4}, a quorum of {1,2,4} but not of {1,2,3}: if node 1 accepts s before counting the acknowledgements of nodes 2 and 4, its last committed configuration is {1,2,3} again, and all of Q is counted without a commit. publication_committed therefore asks Q to be a quorum of every configuration the cluster-manager may be using when the last acknowledgement arrives: its own two and the published state's two.

The proofs rest on the safety mission's invariant, which supplies, for instance, that a node that has not won holds no quorum of both its configurations, and that every publication of the cluster-manager's term is its own, with a version at most its last published version. Since a node has always acknowledged the publication it holds, a node of Q that rejects s has therefore already acknowledged it.

What this rests on and what it does not say

The safety mission's model and inductive invariant (its definitions are imported, and its theorems used as published), the per-node transcription of CoordinationState, and the argument of the safety mission that the Coordinator's calls are steps of the model.

A stable period is a hypothesis. Nothing says that a real network reaches one, how long it lasts or how long its steps take: the model has no time. The theorems are about finite executions; that progress eventually happens follows only under the informal assumption that the needed deliveries take place while the period lasts.
The links to the other missions are informal. A pre-voting round that has started an election establishes the election hypotheses (a quorum of voters no fresher than the candidate, in terms below the new term) if its senders have not changed since answering, and randomized timers make it likely that a candidate fires well before the others; neither link is a composed theorem.
Failure detection is not modelled. The LeaderChecker and FollowersChecker, through which nodes notice a failed cluster-manager or follower and become candidates, and the publication timeouts are outside the model.
Inherited assumptions. Compatible bootstrap configurations, the default election strategy, and the safety mission's assumptions (fixed roles, no disk rollback, no offline tools, exact remote publication) and per-node abstractions.
Remote-store writes are taken to succeed. On a failed remote cluster-state write, Java throws after the local effects where the transcription returns the result (handlePublishRequest, CS:453-456; handlePreCommit after the vote is counted in handlePublishResponse, CS:503-510). For safety this is message loss; for progress it is not: in OpenSearch a node can accept s locally without acknowledging it and then reject every re-delivery of s, and the acknowledgement that completes a quorum can be counted without a commit being sent. The theorems describe OpenSearch only when remote writes succeed or no remote cluster-state store is configured.
The remote commit write is taken to succeed. With a remote cluster-state store configured, OpenSearch's handlePublishResponse, once the counted votes form a publish quorum, marks the published state as committed in the store before returning the commit (handlePreCommit, CoordinationState.java:503-510, 593-599); if that write fails, the method throws after counting the vote, and no commit is sent. The transcription has no remote store and returns the commit. For safety this is a lost message; for progress it is not: in OpenSearch the acknowledgement that completes a quorum can be counted without a commit being sent. Read for OpenSearch, the publication theorems therefore presuppose that this write succeeds or that no remote cluster-state store is configured.

7 thms1 active userReviewed

Completed

Formal Verification Theoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: safety of the Zen2 consensus protocolTextbook

The claim

An OpenSearch cluster keeps its metadata in one cluster state that an elected node, the cluster-manager, publishes to the others. Every node runs the per-node consensus state machine CoordinationState, transcribed and specified in the OpenSearchCoordination mission, driven by the Coordinator over a network that loses, duplicates, delays and reorders messages, while nodes crash and restart. What the protocol is designed to guarantee is safety: in every execution, at most one node is cluster-manager in each term, each (term, version) names one cluster state, and committed cluster states never fork: of any two committed states, one builds on the other. Elastic's TLA+ model ZenWithTerms, which CoordinationState.java cites as its formal model, states these properties for that model and checks them with TLC on small instances; its "main invariant" is that committed publications are related by descent. OpenSearch's randomized test CoordinationStateTests.testSafety, built on CoordinationStateTestCluster, checks the first two properties on random executions of the Java class.

This mission proves these properties, for compatible bootstrap configurations and OpenSearch's default election strategy, for every number of nodes and every execution of a cluster model in which each node runs the transcribed Java code of OpenSearch revision b2a54ba5c0defba3d1d20423e911d4bf920bab19. The goal theorem is committed_linear: any two committed publications lie on one branch of the history.

The model

A cluster is the state of every node together with the set of messages sent so far. A step is one successful call of a CoordinationState method at one node, its output, if any, being added to the set: bootstrapping with a bootstrap configuration (setInitialState, under its asserted preconditions); handling a start-join request from any cluster-manager-eligible node for any term (elections, abdication, and the term bumps on receiving a message of a higher term), the join being sent to the requester; handling a join; publishing a new cluster state as an elected node (handleClientValue, under its asserted precondition); accepting a publication; handling a publish response, a resulting commit being sent; applying a commit; and restarting. A message, once sent, stays available: it may be handled any number of times, in any order, by any node it may be delivered to, or never. The steps cover every call the Coordinator makes; its own guards only reject more calls.

A cluster-manager-eligible node persists its current term and accepted state synchronously, and a restart keeps them except for the parts rebuilt at startup; a node that never joined a cluster may come back with another term-0 state, restored from the remote cluster-state store. A node that is not cluster-manager-eligible persists asynchronously or not at all, and may restart with any state. Nodes may bootstrap with different configurations, as ClusterBootstrapService allows when they have discovered different subsets of the nodes listed in cluster.initial_cluster_manager_nodes. Each publication records, as ghost data the real message does not carry, the term and version of the state its publisher had accepted: its parent. Descent along parents is the history in which the theorems are stated.

What is proved

The public statements about reachable clusters assume that the bootstrap configurations are compatible (any two have intersecting quorums of cluster-manager-eligible nodes) and that the election strategy is OpenSearch's default.

Committed states never fork (committed_linear, the goal): any two committed publications are related by descent. A version is committed in at most one term, and committed versions increase with the term (committed_versions); every commit is of a publication (committed_published).
Leader completeness (leader_completeness): every publication of a later term descends from every committed publication; a cluster-manager of a later term always builds on it.
One cluster-manager per term (one_master_per_term: all publications of a term come from one node), one cluster state per term and version (one_state_per_version: same publisher, same state, same parent), election safety (election_safety: two nodes that hold a won election at the same moment, in the same current term, are the same node).
The assertions of CoordinationState.invariant() never fail at a cluster-manager-eligible node (javaInvariant_reachable), although not every handler preserves them on its own: the per-node mission shows that handlePublishRequest can break them. Every eligible node's last committed configuration is empty, a bootstrap configuration, or the accepted configuration of a committed publication (lastCommitted_committed).
Bootstrapping with partial views gives compatible configurations (bootstrap_compatible): the configurations ClusterBootstrapService builds meet the compatibility condition the safety statements assume, whatever subset of the required nodes each bootstrapping node has discovered, provided each requirement names the same node everywhere. The theorem is about the configurations alone; that the model's bootstrap configurations are of this form is not formalized.
The common hypotheses can be met together with a commit (commit_reachable): a one-node cluster bootstraps, elects itself, publishes and commits. Only one committed key is exhibited: neither two distinct committed keys nor a publication of a later term than a committed key.

The proof is an inductive invariant of 30 facts about nodes, joins, publish responses, publications, commits and leaders (reachable_inv), preserved by each of the nine kinds of step (one theorem per step, under the same two hypotheses), together with 22 lemmas about a single cluster satisfying it: the publications form a forest; along a branch with no commit in between, a newly accepted configuration remains one of the two configurations in force (at most one reconfiguration in flight between commits); and election leader completeness, by strong induction on the term: an election in term t builds on every commit of an earlier term, because otherwise the first commit above the last committed ancestor of the election's base would have a responder among the election's voters, who accepted that commit before voting, which places it below the base after all. Two elections of one term therefore share a voter, and a voter joins one candidate per term.

Findings

The model transcribes the Java, not the TLA+ model, and differs from TLA+ where the code does. Java's handleCommit lacks the TLA+ guard that an elected node has accepted its own last publication: a cluster-manager can apply the commit of its accepted state while its next publication is in flight, and its committed configuration then changes in the middle of that publication. As a result the TLA+ invariant CommitHasQuorumVsPreviousCommittedConfiguration fails for the Java semantics (a 17-step execution: a publication is committed by responders that are not a quorum of its last committed configuration). Safety is unaffected: those responders are a quorum of the accepted configuration of the committed parent, and the invariant records exactly this weaker commit condition. A cluster-manager's last committed configuration can also move backwards. A plugin election strategy that can turn a won election into a lost one (OpenSearch ships only the default) can break "one state per term and version" when Java assertions are disabled (an 11-step execution), which is why the theorems assume the default strategy. The TLA+ invariant CommittedValuesDescendantsFromInitialValue fails harmlessly, because joins of term 0 compare metadata versions. In CoordinationStateTestCluster, the branch that makes a node that is not cluster-manager-eligible lose its persisted state on reboot no longer has any effect since the persisted-state registry was introduced.

Before the proof, two independently designed invariants were checked with explicit-state model checkers of the same message-passing model, with a single bootstrap configuration: about 29 million states by breadth-first search and 6 million random steps for the first, about 1.33 billion states for the second (including two complete runs of 25.4 and 201.1 million states), and inductiveness spot-checks over 39 and 149 million successor steps, without a counterexample.

What this rests on

The Java source at the pinned revision: CoordinationState.java through the per-node mission's transcription, whose definitions are imported, and, for the steps, Coordinator.java, ClusterBootstrapService.java and GatewayMetaState.java.

Assumptions outside the model. A node's cluster-manager role never changes (a node restarted without the cluster-manager and data roles overwrites its persisted state with term 0, so changing the role and back can reset its term); persisted state is never rolled back; the offline opensearch-node tools are not used; each bootstrap requirement names the same node at every node; every node uses the default election strategy; a publication delivered through the remote cluster-state store reconstructs exactly the published state. The per-node abstractions apply (terms are natural numbers, versions integers without overflow).
The Coordinator is not transcribed. That each of its calls into CoordinationState is a step of the model is argued from the code, not proved; its other duties (mode changes, the publication pipeline and its timeouts, fault detection, join validation, reconfiguration choices) are outside the theorems.
Liveness is not proved here. Nothing says that an election eventually succeeds or that a publication is eventually committed; the pre-voting mission covers single rounds, progress when nothing disrupts an election or a publication is the subject of a separate mission over the same cluster model, and the randomized election timers of another.

45 thms1 active userReviewed

Completed

Formal Verification Theoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: pre-voting and election schedulingTextbook

The claim

In OpenSearch's cluster coordination a node starts an election by sending StartJoinRequests for a new term, and every node that handles one moves to that term (CoordinationState.handleStartJoin, transcribed in the per-node mission) and discards its election and publication state: a leader that handles one is no longer leader. A node that started elections whenever it lost sight of the leader — on the wrong side of a network partition, or while restarting — would depose a leader that the rest of the cluster still follows. OpenSearch therefore precedes every election with a pre-voting round (PreVoteCollector), a check comparable to the Pre-Vote phase of Raft: the node asks the nodes it has discovered, itself included, whether they would support it, without asking anyone to change its term (a leader whose current term is below the request's still moves to a higher term and starts an election, see below), and starts the election only if the answers it counts form an election quorum.

A node answers a pre-vote request with its current term and the term and version of its last accepted cluster state (the metadata version, for a term-0 state), unless it is unhealthy or knows a leader other than the requester. The requester ignores answers fresher than its own last accepted state — the comparison handleJoin makes when it counts votes — and as soon as the senders of the answers it has kept form an election quorum of the last committed and last accepted configurations of its accepted state, it calls startElection, once per round. startElection sends StartJoinRequests for the term max(currentTerm, maxTermSeen) + 1, where maxTermSeen is the largest term the node has seen, in pre-vote answers among other messages. Pre-voting rounds are started by an election scheduler at random intervals whose bound backs off linearly up to a maximum.

This mission transcribes the pre-vote messages and handlers, the pre-voting round, the term of the election it triggers and the scheduler's delays, at OpenSearch revision b2a54ba5c0defba3d1d20423e911d4bf920bab19, on top of the per-node CoordinationState mission, and proves what a single round guarantees.

The transcription

Answering (handlePreVoteRequest, PVC:133-163). A node's collector state is its known leader and its own response, both as last set by the Coordinator: itself when it becomes leader, the leader it follows, nobody when it becomes a candidate (CO:516, 653, 777, 801, 839, 1157). In Java the response is getPreVoteResponse() of its coordination state, transcribed as preVoteResponseOf (CO:873-879); CollectorState keeps it as a free field, and no_disruption holds for every collector state. Health is a Boolean parameter.
Rounds (PreVotingRound, PVC:175-300). A round holds the requester's accepted state when it started, the requester, the recorded (sender, response) pairs, and the flags electionStarted and isClosed; in every reachable round there is at most one pair per sender, a sender being a node value (id and role), as round_entries proves (the type itself allows repeats). handlePreVoteResponse follows PVC:225-279 step by step and returns, besides the new round, whether startElection is called and the term passed to updateMaxTermSeen. The requester's own current response, which Java reads when each answer arrives, is a parameter of each step. RoundReachable es Delivered stands for the network: it collects the rounds obtained by handling, in any order and any number of times, the responses that the predicate Delivered allows, and by closing.
The election. startElectionTerm is the term startElection uses (CO:593). handleJoins handles a list of joins in order with the per-node handleJoin, a rejected join leaving the state unchanged, as Coordinator.handleJoin (CO:1267-1299) does for joins whose term is not above the node's current term; a join of a higher term is simply rejected, where the Coordinator would first move the node to that term (CO:1269).
The scheduler (ElectionSchedulerFactory). The four settings with their ranges (ESF:85-115) and the check initial_timeout ≤ max_timeout (ESF:133-143); the bound maxDelay s k = min(maxTimeout, initialTimeout + k · backoffTime) of attempt k (ESF:203); and its delay, nonNegative(r) mod maxDelay s k + 1 plus the grace period, for the random long r (ESF:159-172, 204). In Java the grace period is 0 for the first attempt (CO:1574) and cluster.election.duration for the later ones (ESF:218); the transcription takes it as a parameter (the setting duration occurs only in Valid), and attemptDelay_bounds holds for every grace period.

What is proved

The handlers (handlePreVoteRequest_spec, votes_mem, round_entries, round_start_quorum, round_starts_once). A node answers exactly when it is healthy and knows no leader or knows the requester as its leader, and then with its own response. A round counts exactly its cluster-manager-eligible senders; it records only delivered responses that are no fresher than its accepted state, one per sender; it calls startElection only while open, only when its votes, once the new response is recorded, form an election quorum, and at most once.
A quorum that refuses the requester blocks every pre-voting round (no_disruption). Let a quorum L of the last committed or of the last accepted configuration of a node c's accepted state consist of nodes that are unhealthy or follow a leader other than c, every node's health and collector state staying as they are while the round runs. Then no pre-voting round of c over that state starts an election, whatever answers to c's request it receives (each node's answer computed from those fixed states), in whatever order and number, and whatever the election strategy: the nodes of L do not answer, every recorded sender answered, and a set of voters disjoint from a quorum of a configuration is not a quorum of it. A node cut off from a cluster whose majority follows a leader cannot depose that leader by starting elections when it comes back.

The theorem is about the round, not about every effect of the request. Handling a pre-vote request raises the receiver's maxTermSeen to at least the requester's current term, and a leader whose current term is below it moves to that term and runs a new election itself, at once or when its publication in progress ends (CO:560-581, CO:1784). Pre-voting stops a returning node from starting elections; it does not stop this term bump when the returning node's term is higher than the leader's.
A successful pre-vote predicts a successful election (preVote_then_election). If a round of node c over its accepted state has started an election, the election startElection begins succeeds, provided nothing changes under it: every node whose answer the round recorded accepts c's StartJoinRequest for T = max(currentTerm, maxTermSeen) + 1, since its current term is at most maxTermSeen, below T; and when the joins those nodes send back reach c, c accepts every one of them, so its join votes contain the round's votes, a quorum of both configurations, and it wins: its CoordinationState has electionWon = true (the Coordinator's move to leader is outside the model). The hypotheses make "nothing changes" precise:
- the senders have not changed since answering: a response from n is preVoteResponseOf (node n), where node n, whose local node is n, is the coordination state in which n handles the StartJoinRequest, so its current term and its last accepted term and version are those it reported (the round's delivery predicate);
- c has not changed: the round is over c's current accepted state, and after its own start-join c handles only joins — no other start-join, publication or restart;
- no join of a higher term arrives: every join c handles has a term at most T, because Coordinator.handleJoin would first move c to the higher term and discard its votes (CO:1269); joins of term at most T from other nodes may be interleaved in any order, accepted or rejected;
- the election strategy is the default one, and maxTermSeen is at least the current term of every recorded answer (as updateMaxTermSeen ensures, PVC:231).
The freshness check that handleJoin makes at c is the one the round already made on the same values; the term check passes because every join is for T, c's new term; the remaining checks pass because c has just handled its own start-join and its configurations, having quorums, are nonempty.
The election scheduler (attemptDelay_bounds, maxDelay_schedule, nonNegative_two_to_one). For valid settings, attempt k waits between g + 1 and g + maxDelay s k milliseconds, g its grace period, and the bound is at least 1, so the Java assertion 0 < upperBound (ESF:170) always holds. The bound starts at initial_timeout, never decreases, and while below max_timeout grows by back_off_time per attempt or reaches max_timeout, where it stays (at the latest from attempt number max_timeout on). nonNegative maps the Java longs exactly two-to-one onto [0, 2^63), the counting fact behind the uniformity of the random delay (exact for nonNegative of a uniform long; the remainder modulo the bound adds a negligible bias; no probability is formalized).

What this rests on and what it does not say

The Java source at the pinned revision — PreVoteCollector.java, Coordinator.java (getPreVoteResponse, startElection, updateMaxTermSeen, handleJoin, startElectionScheduler), ElectionSchedulerFactory.java — and the per-node mission's transcription of CoordinationState. Only that mission's definitions are imported.

The Coordinator's side effects are outside the transcribed functions: the term bump above, the sending of messages, and the transitions between candidate, leader and follower. nodeMayWinElection, which startElection checks, is transcribed but not used.
Nodes are compared by id and role. Java compares ephemeral ids, which change when a node restarts, so the two differ only between two incarnations of one node with the same role: a follower of a node's previous incarnation with the same role refuses its pre-vote request in Java and answers it here.
The election strategy sees voter ids, as in the per-node mission; no_disruption holds for every strategy, preVote_then_election for the default one, the only one in OpenSearch itself.
The theorems are about one round with fixed answers. They say nothing about liveness: whether some election eventually succeeds when several nodes compete, how long messages take, or how the random delays separate competing candidates. The scheduler theorems hold for every drawn number; the distribution of Java's Random.nextLong() is not modelled.
Pre-voting is not needed for safety. The cluster-level properties — at most one leader per term, committed states never fork, the assertions of invariant() at every node — are the subject of the next mission, whose model lets any cluster-manager-eligible node send a start-join request of any term.

11 thms1 active userReviewed

Completed

Formal Verification Theoretical Computer Science·Captain: pitimespi

OpenSearch cluster coordination: the per-node consensus state machine (CoordinationState)Textbook

The claim

OpenSearch (and Elasticsearch since 7.0) keeps the metadata of a cluster — which indices exist, their mappings and settings, which node holds which shard — in a single cluster state that one elected node, the cluster-manager (formerly "master"), publishes to all others. The algorithm that elects the cluster-manager and makes every published state durable is a Paxos/Raft-like consensus protocol, introduced in Elasticsearch 7.0 as "Zen2". Its core is one class, CoordinationState, which every node runs: a state machine with a persisted part (the current term and the last accepted cluster state) and a transient part (election votes, publication votes), driven by seven handlers — setInitialState, handleStartJoin, handleJoin, handleClientValue, handlePublishRequest, handlePublishResponse, handleCommit. The class cites Elastic's TLA+ specification ZenWithTerms as its formal model; that specification is model-checked with TLC on a small instance (three nodes, terms up to 2, versions up to 3). Elastic's repository of formal models also contains an Isabelle/HOL proof of consistency for an alternative model of the algorithm. Neither is a statement about the Java code.

This mission transcribes CoordinationState at OpenSearch revision b2a54ba5c0defba3d1d20423e911d4bf920bab19 and proves its per-node properties. The cluster-level safety properties are the subject of the OpenSearchSafety mission, which builds on this transcription (it imports this mission's definitions, not its theorems) and proves them for a cluster model in which every node runs it, assuming compatible bootstrap configurations and the default election strategy: one cluster-manager per term (one_master_per_term), one state per term and version (one_state_per_version), committed states never fork (committed_linear), and the assertions of invariant() never fail at a cluster-manager-eligible node (javaInvariant_reachable).

The transcription

A node is identified by its id and carries its cluster-manager-eligible role. A voting configuration is a set of node ids; a set of votes is a quorum of it when it contains more than half of its members (VotingConfiguration.hasQuorum). Votes are counted only from cluster-manager-eligible nodes (VoteCollection.addVote). A cluster state is reduced to the fields CoordinationState reads or writes: term, version, metadata version (used instead of the version for term-0 states, getVersionOrMetadataVersion), last committed and last accepted configurations, the cluster-manager node (read only by the Zen1 compatibility branch), the cluster-UUID flags, and an opaque payload.

The handlers are transcribed check by check, in the Java order, each returning either a rejection or the new state with its output:

handleStartJoin moves to a strictly higher term and votes (a Join) for the requesting node, carrying the node's last accepted term and version (the metadata version, for a term-0 state);
handleJoin counts a vote for the current term, once the node has handled a start-join since its last restart and has been bootstrapped, from a voter whose accepted state is no fresher than the node's own; it recomputes electionWon as "the votes are a quorum of both the last committed and the last accepted configuration" (plus a pluggable election-strategy constraint);
handleClientValue lets an elected node that has accepted its own last publication publish a new state of its term with a higher version, reconfiguring only when no reconfiguration is pending and only to a configuration in which its votes are a quorum;
handlePublishRequest accepts a state of the current term unless it has the last accepted term and a version no higher than the last accepted one (at a node whose accepted term is at most its current term, this means a state newer than the last accepted one), and, in the compatibility branch for clusters upgrading from Zen1, even such a state when its term is 0, it names a cluster-manager, and the last accepted state names none or a different one;
handlePublishResponse counts publication votes and emits an ApplyCommitRequest once they are a quorum of both the last committed configuration and the configuration being published;
handleCommit marks the last accepted state committed (its accepted configuration becomes the committed one).

Java asserts are disabled in production and are caller contracts; the transcription does not check them. The asserted preconditions of setInitialState and handleClientValue are kept as separate predicates (initialStateContract, clientValueContract), which no theorem of this mission uses; the cluster model of the OpenSearchSafety mission imposes them at the steps that call these methods, and delivers a join only to its target. The assertion of markLastAcceptedStateAsCommitted about unknown cluster UUIDs and the assertions of the Join and PublishResponse constructors that their versions are non-negative are not represented. The remote cluster-state store (the REMOTE persisted state) is omitted: the handlers read it only to decide whether to write it, every value they compute comes from the LOCAL persisted state, and a failed remote write only makes the Java method throw after its local effects; the transcription returns the output instead, so the Java run is the transcription's run with that output lost, which a cluster model whose messages may be lost includes.

What is proved

Quorums: two quorums of the same configuration intersect; a superset of a quorum is a quorum; the empty configuration has no quorum; no votes are no quorum; only eligible votes count.
Handler specifications: what each handler other than setInitialState requires and changes (handleStartJoin_spec, which characterizes the handler in both directions; handleJoin_spec; handleClientValue_spec; handlePublishRequest_spec, which assumes that the accepted term is at most the current term; handlePublishResponse_spec; handleCommit_spec); apart from handleStartJoin_spec, they state what a successful call implies, not when a call succeeds.
Monotonicity: at a node whose last accepted term is at most its current term, every successful handler call (of setInitialState, with a state of term 0, as Java asserts) preserves that inequality, handleStartJoin strictly raises the current term, and every other handler leaves it unchanged; at such a node, a publication is accepted only if it is strictly newer than the last accepted state in the (term, version) order or has term 0 (the Zen1 compatibility branch, whose condition on the cluster-manager the statement does not record).
Elections: a node only counts votes from voters whose accepted state is no fresher than its own; for a monotone election strategy (the default is), a won election stays won at a node whose electionWon agrees with its votes — the assertion at CoordinationState.java:323-324.
The assertions of invariant(): they hold for a freshly started node whose persisted accepted term is at most its persisted current term; handleStartJoin re-establishes them at any node whose accepted term is at most its current term; for a monotone election strategy (the theorem assumes it for all three handlers), handleJoin, handleClientValue and handlePublishResponse preserve them. handlePublishRequest does not preserve them in isolation: for the default strategy, an explicit node satisfies invariant(), accepts a publication, and violates it. (handleCommit and setInitialState, which like handlePublishRequest change the configurations, are not covered by any theorem either.) That invariant() holds at every cluster-manager-eligible node of every execution is therefore a property of the whole cluster, which the OpenSearchSafety mission proves for its cluster model, assuming compatible bootstrap configurations and the default election strategy (javaInvariant_reachable).

Vectors

OpenSearch's own unit tests are replayed against the transcription (tests/OpenSearchCoordinationVectors.lean): 40 tests of CoordinationStateTests.java and testVotingConfiguration of CoordinationMetadataTests.java, 179 checks, each proved by decide. Every Java assertion holds, with two exceptions. Four copy-equality assertions about VoteCollection.equals in testVoteCollection fail: Java compares the maps of voters (and the recorded joins, none there), the transcription's = also compares the order in which the votes were added (no handler compares vote collections); they hold with set equality of the voters, which is checked instead. And the two tests that expect a Java AssertionError (testJoinWithWrongTarget, testHandleClientValueWithIllegalCommittedConfigurationChange) are recorded with a supplementary check, since the transcription does not check asserts. The randomized cluster test testSafety and the tests of the remote cluster-state store are not replayed; the properties testSafety checks (one cluster-manager per term, one state per term and version, and invariant() at every node, all of them cluster-manager-eligible there) are proved for the cluster model of the OpenSearchSafety mission (one_master_per_term, one_state_per_version, javaInvariant_reachable), under that mission's assumptions.

What this rests on

The Java source at the pinned revision: CoordinationState.java, CoordinationMetadata.java (VotingConfiguration), ElectionStrategy.java, ClusterState.java (getVersionOrMetadataVersion), and the message classes. Terms are natural numbers (Java longs that are never negative: a fresh node's term is 0 and among the handlers only handleStartJoin changes it, upwards; the constructor takes the persisted term as a parameter); versions are integers (Java long; overflow is not modelled, nor the assertions of the Join and PublishResponse constructors that their versions are non-negative). The file imports nothing beyond Lean's core. (CoordinationState.java)

19 thms1 active userReviewed

Quantum Information·Captain: Gohan

Simplicial principal bundles in parametrized spacesResearch Paper

Motivation

In this paper we study the classifying theory of principal bundles in the parametrized setting, motivated by recent interest in higher gauge theory. Using simplicial techniques, we construct a product-preserving classifying space functor for groups in the category of spaces over a fixed space B. Additionally, we prove that the fiberwise geometric realization functor sends a large class of simplicial parametrized principal bundles to ordinary parametrized principal bundles. As an application we show that the fiberwise geometric realization of the universal simplicial principal bundle for a simplicial group G in the category of spaces over B gives rise to a parametrized principal bundle with structure group |G|.

This mission is the statement-level formalization of Simplicial principal bundles in parametrized spaces (arXiv:1203.2460v4). 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 10: equivariant fiberwise NDR criterion (Lemma 10, 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

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

Theorem 1: classification of parametrized principal bundles (original paper seed): Actual bar-model classification map and its domain/codomain quotients (hard)
Theorem 2: realization of simplicial parametrized principal bundles: Coend realization with induced principal action and numerability (hard)
Proposition 3: well-sectioned simplicial groups: Simplicial internal groups, Wbar, realization, and canonical latching maps (hard)
Proposition 4: realized universal bundle and contractible total group: Realized universal W-bundle with contraction and canonical closed subgroup (hard)
Lemma 8: realization sends group objects to group objects: Actual fiberwise realization and induced internal group law (hard)
Lemma 9: topological bicompleteness of equivariant parametrized spaces: K-enrichment, tensors, cotensors and all induced equivariant (co)limits (hard)
Corollary 15: concordance and isomorphism classes: Principal-bundle isomorphism and fiberwise concordance quotients (hard)
Proposition 16: pullback of a strong cofibration along a principal bundle: Numerable principal bundle and its actual equivariant restriction (hard)
Lemma 19: canonical universal principal twisted cartesian product: Universal twisted product and its total-group construction in arbitrary finite-limit C (hard)
Lemma 21: realization of a Cech nerve: Cech nerve realization and its canonical augmentation (hard)
Lemma 22: pulled-back skeletal attachment is a pushout: Canonical skeletal attaching pushout pulled back along the given simplicial bundle (hard)
Lemma 23: equivariant cofibrations in the pulled-back skeletal filtration: Realized attaching map and pulled-back skeletal filtration with induced |G|-actions (hard)
Proposition 26: good implies proper under Lillig and extensivity hypotheses: General topological bicompleteness, strong hbar-cofibrations, Lillig and latching interfaces (hard)
Lemma 28: partial latching pullback squares: Canonical partial latching functor and properly extensive degeneracy square (hard)
Proposition 29: good simplicial parametrized spaces are proper: Canonical k-space latching colimits and good/proper predicates (hard)
Unnumbered main result: the classifying-space functor preserves products: Actual Wbar and B functors and their canonical product comparison (hard)
Unnumbered consequence: realization of principal twisted cartesian products: Pseudo-cross sections, principal twisted products and their induced realization (hard)
Unnumbered supporting result: the two total-decalage maps are simplicially homotopic: Diagonal total decalage, its two augmentations, and canonical simplicial cylinder homotopy (hard)

Selected references

Simplicial principal bundles in parametrized spaces, arXiv:1203.2460v4, https://arxiv.org/abs/1203.2460v4

4 thms1 active userReviewed

Quantum Information·Captain: Gohan

Topological Entanglement Entropy and HolographyResearch Paper

Motivation

We study the entanglement entropy in confining theories with gravity duals using the holographic prescription of Ryu and Takayanagi. The entanglement entropy between a region and its complement is proportional to the minimal area of a bulk hypersurface ending on their border. We consider a disk in 2+1 dimensions and a ball in 3+1 dimensions and find in both cases two types of bulk hypersurfaces with different topology, similar to the case of the slab geometry considered by Klebanov, Kutasov and Murugan. Depending on the value of the radius, one or the other type of hypersurfaces dominates the calculation of entanglement entropy. In 2+1 dimensions a useful measure of topological order of the ground state is the topological entanglement entropy, which is defined to be the constant term in the entanglement entropy of a disk in the limit of large radius. We compute this quantity and find that it vanishes for confining gauge theory, in accord with our expectations. In 3+1 dimensions the analogous quantity is shown to be generically nonzero and cutoff-dependent.

This mission is the statement-level formalization of Topological Entanglement Entropy and Holography (arXiv:0805.1891v2). 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 Conformal boundary profile and its finite-order logarithmic expansion ((3.8)–(3.11), (3.14), 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.

Deferred results

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

§3.2, (3.24)–(3.25): Constructed rotational D3 RT admissibility, attained renormalized minimum, eventual cylinder selection, and the entropy constant term (hard)
§3.1: numerical conformal coefficient, Fig.2: §3.1: numerical conformal coefficient, Fig.2 (source-ambiguity)
§3.2, Figs.3–6: Constructed competing D3 area branches, their singular joining geometry, and actual first-order entropy minimum (hard)
§3.2: strength of the finite-entropy remainder in (3.25): §3.2: strength of the finite-entropy remainder in (3.25) (source-ambiguity)
§4.1–§4.2, Figs.7–10: Constructed competing D4 area branches, critical joining, and first-order minimization switch (hard)
(4.16) and following sentence; compare rendered (4.9), PDF p.15: A consistent first logarithmic order for the physical D4 boundary expansion, and an independently reviewed source correction (source-ambiguity)
§4.3: printed bulk gamma evaluation, (4.25): §4.3: printed bulk gamma evaluation, (4.25) (source-ambiguity)
§4.3: gauge-theory expressions, (4.28): §4.3: gauge-theory expressions, (4.28) (source-ambiguity)
§4: supergravity/cutoff validity, (4.4), (4.29): §4: supergravity/cutoff validity, (4.4), (4.29) (source-ambiguity)
Appendix A: numerical Rc=0.7034: Appendix A: numerical Rc=0.7034 (source-ambiguity)
Reduction from induced geometry to profile-action prefactors, (3.6), (3.17), (3.19), (4.8): Reduction from induced geometry to profile-action prefactors, (3.6), (3.17), (3.19), (4.8) (source-ambiguity)
§5, regularized entropy scales as Nc² at both sides of the critical point: Nc-independent attained entropy minimization over the source D3/D4 rotational hypersurfaces, rather than one fixed stationary profile (hard)

Selected references

Topological Entanglement Entropy and Holography, arXiv:0805.1891v2, https://arxiv.org/abs/0805.1891v2

11 thms1 active userReviewed

Quantum Information·Captain: Gohan

Local structure of algebraic monoidsResearch Paper

Motivation

We describe the local structure of an irreducible algebraic monoid $M$ at an idempotent element $e$ . When $e$ is minimal, we show that $M$ is an induced variety over the kernel $MeM$ (a homogeneous space) with fibre the two-sided stabilizer $M_e$ (a connected affine monoid having a zero element and a dense unit group). This yields the irreducibility of stabilizers and centralizers of idempotents when $M$ is normal, and criteria for normality and smoothness of an arbitrary $M$ . Also, we show that $M$ is an induced variety over an abelian variety, with fiber a connected affine monoid having a dense unit group.

This mission is the statement-level formalization of Local structure of algebraic monoids (arXiv:0709.1255v2). 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 Minimal idempotents: global product descriptions (Lemma 2.3.1, PDF p. 14). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Lemma 1.1.1: Multiplicative one-parameter subgroup, its extension to A1, and neutral component of the computed unit stabilizer (hard)
Example 1.2.1: Invariant-theoretic tensor-image quotient, its normal scheme image, and corrected nonzero centralizer identity (source-ambiguity)
Lemma 1.2.2: Corner monoid eMe, centralizer retraction, represented kernel exactness, and algebraic normalizer (hard)
Lemma 1.2.3: Represented homogeneous space G/C_G(e), with its structure sheaf and conjugacy orbit morphism (hard)
Lemma 1.3.1: Regular corner retraction rho, exact sequence of algebraic groups, and algebraic normalizer of G_e^ell (hard)
Lemma 1.3.2: Two represented homogeneous quotients and their canonical variety isomorphism (hard)
Lemma 1.3.3: Two-sided pair stabilizer, corner fibre-product maps and the two exact group sequences (hard)
Remark 1.3.4: Reductivity, opposite parabolics, common Levi group, unipotent radicals and internal semidirect products (hard)
Lemma 2.1.1: Homogeneous quotient and contracted product with canonical multiplication maps (hard)
Proposition 2.1.2: Contracted-product scheme, equivariance, and scheme-theoretic intersection with Me (hard)
Remarks 2.1.3: Actual multiplication fibre, induced-variety open immersion and non-affine End(V) counterexample (hard)
Theorem 2.2.1: Iterated contracted product, canonical equivariant product map, and scheme intersection with the actual ideal MeM (hard)
Remarks 2.2.2: Local quotient slice and equivariant non-retraction for End(V) (hard)
Corollary 2.2.3: Two canonical contracted-product isomorphisms and irreducibility at e (hard)
Corollary 2.2.4: Right-centralizer contracted quotient and pair-stabilizer quotient by G_e x G_e (hard)
Corollary 2.2.5: Seven computed varieties with distinguished points, local normality and pair-group connectedness (hard)
Remark 2.2.6: Reductive unipotent radicals, middle contracted product, and orbit-idempotent property (hard)
Corollary 2.3.2: Five global canonical contracted-product isomorphisms at a minimal idempotent (hard)
Corollary 2.3.3: All seven stabilizer/centralizer schemes and local/global normality equivalence (hard)
Lemma 3.1.1: Canonical Chevalley subgroup G_aff and reduced closure M_aff inside M (hard)
Remark 3.1.6: Reductive smooth-monoid classification by matrix products and unordered sums of squares (hard)
Theorem 3.2.1: Normalized Albanese morphism, its actual fibre N and units H, finite-index Chevalley subgroup, and geometric induction (hard)
Remark 3.2.2: Canonical N,H and a descended monoid law on the geometric induced variety (hard)
Corollary 3.3.2: Categories of genuine algebraic monoids and triples, with morphisms and natural inverse functors (hard)
Corollary 3.3.3: Equivariant group embedding, normalized Albanese, and compatible monoid structures with uniqueness (hard)
Corollary 3.3.4: Canonical product pi from the Chevalley contracted product and associated normalized Albanese triple (hard)
§3.1, unnumbered extension of local structure: Chevalley and central-component constructions plus the entire non-affine quotient-chart and normality packages (hard)
§3.1, unnumbered extension at minimal idempotents: Minimal idempotents in M_aff, unique closed orbit/kernel, non-affine global quotient packages and existential smoothness criterion (hard)

Selected references

Local structure of algebraic monoids, arXiv:0709.1255v2, https://arxiv.org/abs/0709.1255v2

6 thms1 active userReviewed

Quantum Information·Captain: Gohan

Stochastic processes induced by singular operatorsResearch Paper

Motivation

In this paper we study a general family of multivariable Gaussian stochastic processes. Each process is prescribed by a fixed Borel measure $σ$ on $\mathbb R^n$ . The case when $σ$ is assumed absolutely continuous with respect to Lebesgue measure was studied earlier in the literature, when $n=1$ . Our focus here is on showing how different equivalence classes (defined from relative absolute continuity for pairs of measures) translate into concrete spectral decompositions of the corresponding stochastic processes under study. The measures $σ$ we consider are typically purely singular. Our proofs rely on the theory of (singular) unbounded operators in Hilbert space, and their spectral theory.

This mission is the statement-level formalization of Stochastic processes induced by singular operators (arXiv:1109.5273v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

15 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Gaussian measure on the continuous real tempered dual (§1(d), unnumbered: distribution Gaussian characteristic law, PDF p. 3). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Theorem 5.2: Complex Hilbert factor versus REAL isonormal lift (source-ambiguity)
Theorem 7.1: Real evaluation covariance versus unsymmetrized complex spectrum (source-ambiguity)
Theorem 7.2: Incorrect Lebesgue-L2 norm for evaluation process (source-ambiguity)
Lemma 8.1: Stationary distances do not define a linear unitary orbit (source-ambiguity)
Lemma 8.2: Continuity on an uncontrolled orthogonal complement (source-ambiguity)
Theorem 9.1: Unspecified joint white-noise coupling (source-ambiguity)
Theorem 10.2: Incompatible real normal field, probability space and time-Fourier conventions (source-ambiguity)

Selected references

Stochastic processes induced by singular operators, arXiv:1109.5273v1, https://arxiv.org/abs/1109.5273v1

16 thms1 active userReviewed

Quantum Information·Captain: Gohan

Framed bicategories and monoidal fibrationsResearch Paper

Motivation

In some bicategories, the 1-cells are morphisms' between the 0-cells, such as functors between categories, but in others they are objects' over the 0-cells, such as bimodules, spans, distributors, or parametrized spectra. Many bicategorical notions do not work well in these cases, because the morphisms between 0-cells', such as ring homomorphisms, are missing. We can include them by using a pseudo double category, but usually these morphisms also induce base change functors acting on the 1-cells. We avoid complicated coherence problems by describing base change nonalgebraically', using categorical fibrations. The resulting framed bicategories' assemble into 2-categories, with attendant notions of equivalence, adjunction, and so on which are more appropriate for our examples than are the usual bicategorical ones. We then describe two ways to construct framed bicategories. One is an analogue of rings and bimodules which starts from one framed bicategory and builds another. The other starts from a monoidal fibration', meaning a parametrized family of monoidal categories, and produces an analogue of the framed bicategory of spans. Combining the two, we obtain a construction which includes both enriched and internal categories as special cases.

This mission is the statement-level formalization of Framed bicategories and monoidal fibrations (arXiv:0706.1286v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Framing: three equivalent characterizations (Theorem 4.1: Three equivalent characterizations of framing, PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.

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

Deferred results

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

Proposition 3.4: Cartesian-arrow calculus: Cited-background fibration result with exact whole-result provenance/reuse (hard)
Proposition 3.8: Grothendieck equivalence of 2-categories: Cited-background fibration result with exact whole-result provenance/reuse (hard)
Proposition 3.9: Bifibrations characterized by adjoints: Cited-background fibration result with exact whole-result provenance/reuse (hard)
Corollary 4.13: Restriction and extension commute with horizontal composition: Chosen restrictions/extensions as functors on horizontal hom-categories, globular natural isomorphisms, and coherent companion/conjoint pseudofunctors (hard)
Proposition 4.16: Pseudofunctoriality of base change objects: Chosen restrictions/extensions as functors on horizontal hom-categories, globular natural isomorphisms, and coherent companion/conjoint pseudofunctors (hard)
Proposition 5.4: Dual pairs preserved by base change: Chosen restriction/extension functors and their action on specified duality units/counits (hard)
Proposition 5.5: Framed calculus of mates: Reversed variance in the printed mate bijection (source-ambiguity)
Proposition 5.11: Closed descriptions of restrictions: Two-variable horizontal right adjoints with natural hom-bijections, evaluation maps, and their canonical comparison transformations (hard)
Proposition 6.8: Automatic preservation of cartesian cells: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Proposition 6.17: Strict 2-categories of framed bicategories: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Proposition 7.2: Equivalence functors are strong: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Proposition 7.5: Full and faithful framed functors detected locally: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Proposition 7.7: Essential surjectivity detected locally: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Theorem 7.8: Double equivalence criterion: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Corollary 7.9: Framed equivalence criterion: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Proposition 8.2: Left adjoints are strong: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Corollary 8.5: Both equivalence functors are strong: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Proposition 8.6: Universal-arrow criterion for framed adjunction: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Proposition 9.4: External tensor preserves dual pairs: External strong framed tensor, monoidal/braided constraints and interchange compatibility (hard)
Proposition 10.3: Involution exchanges horizontal homs: Two-variable horizontal right adjoints with natural hom-bijections, evaluation maps, and their canonical comparison transformations (hard)
Theorem 11.5: Omnibus module construction: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Proposition 11.10: Module framed bicategory and local coequalizers: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Proposition 11.12: Module construction is 2-functorial: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Proposition 11.15: Module construction preserves external monoidal structure: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Proposition 11.16: Module construction preserves closedness: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Proposition 11.17: Module construction preserves involutions: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Theorem 12.8: Monoidal Grothendieck equivalence: Strict monoidal total/base functor, full cartesian lifts, indexed strong monoidal fibers, fixed-base morphisms, and the monoidal Grothendieck 2-equivalence (hard)
Proposition 13.13: Existence of internal and external homs: Internal and external fiber tensor right adjoints, canonical base-change/projection mates, and weak/strong Beck–Chevalley predicates (hard)
Proposition 13.25: Beck–Chevalley closedness comparison: Internal and external fiber tensor right adjoints, canonical base-change/projection mates, and weak/strong Beck–Chevalley predicates (hard)
Proposition 13.30: External closedness detects monoidal opfibration: Internal and external fiber tensor right adjoints, canonical base-change/projection mates, and weak/strong Beck–Chevalley predicates (hard)
Corollary 13.33: Strong BC and closed fibers force both closedness notions: Internal and external fiber tensor right adjoints, canonical base-change/projection mates, and weak/strong Beck–Chevalley predicates (hard)
Theorem 14.4: Seed: frameable bifibration construction with involution: Missing tensor reversal in the unconditional involution (source-ambiguity)
Theorem 14.9: Cocartesian construction with involution: Missing tensor reversal in the unconditional involution (source-ambiguity)
Theorem 14.11: Fr construction is a 2-functor: Definition 12.5 morphisms of frameable bifibrations and the actual induced strict Fr 2-functor, including product-comparison pushforward and transformations (hard)
Proposition 14.14: Adjunctions of frameable bifibrations: Definition 12.5 morphisms of frameable bifibrations and the actual induced strict Fr 2-functor, including product-comparison pushforward and transformations (hard)
Proposition 15.2: Local coequalizers and closedness for Mod of Fr: Both actual Fr and Mod constructions with fiberwise (co)equalizers, base-change preservation and external tensor preservation (hard)
Proposition 15.10: Canonical free construction from self-indexing: Definition 12.5 morphisms of frameable bifibrations and the actual induced strict Fr 2-functor, including product-comparison pushforward and transformations (hard)
Lemma 16.1: BC as cartesian–opcartesian lifting: Internal and external fiber tensor right adjoints, canonical base-change/projection mates, and weak/strong Beck–Chevalley predicates (hard)
Corollary 16.4: Tensor interchange squares satisfy BC: Internal and external fiber tensor right adjoints, canonical base-change/projection mates, and weak/strong Beck–Chevalley predicates (hard)
Corollary 16.6: Cartesian vertical tensor forces weak BC: Internal and external fiber tensor right adjoints, canonical base-change/projection mates, and weak/strong Beck–Chevalley predicates (hard)
Lemma 16.9: Diagonal lifting from internal closedness: Internal and external fiber tensor right adjoints, canonical base-change/projection mates, and weak/strong Beck–Chevalley predicates (hard)
Proposition 17.1: Strong BC cartesian construction: The Fr pullback arrow category with composition pi_! Delta^* and unit Delta_! pi^* I, coherent chosen lifts, and symmetric reshuffled external tensor; the cocartesian dual as applicable (hard)
Corollary 17.9: Strong co-BC cocartesian construction: The Fr pullback arrow category with composition pi_! Delta^* and unit Delta_! pi^* I, coherent chosen lifts, and symmetric reshuffled external tensor; the cocartesian dual as applicable (hard)
Proposition 17.10: Weak BC internally closed construction: The Fr pullback arrow category with composition pi_! Delta^* and unit Delta_! pi^* I, coherent chosen lifts, and symmetric reshuffled external tensor; the cocartesian dual as applicable (hard)
Proposition 17.13: Claimed canonical involution: Missing tensor reversal in the unconditional involution (source-ambiguity)
Proposition 17.14: Horizontal closedness of cartesian construction: The Fr pullback arrow category with composition pi_! Delta^* and unit Delta_! pi^* I, coherent chosen lifts, and symmetric reshuffled external tensor; the cocartesian dual as applicable (hard)
Proposition 17.15: Horizontal closedness of cocartesian construction: BC versus co-BC mismatch for the cocartesian Fr construction (source-ambiguity)
Proposition 17.16: Proof-stage Fr 2-functoriality: Definition 12.5 morphisms of frameable bifibrations and the actual induced strict Fr 2-functor, including product-comparison pushforward and transformations (hard)
Proposition B.3: Framed equivalence induces horizontal biequivalence: The actual horizontal bicategory and induced horizontal pseudofunctors, oplax transformations, modifications, local adjunctions, and full monoidal bicategory coherence where required (hard)
Theorem B.4: Horizontal monoidal bicategory: The actual horizontal bicategory and induced horizontal pseudofunctors, oplax transformations, modifications, local adjunctions, and full monoidal bicategory coherence where required (hard)
Proposition C.2: Equipment from framed bicategory: An independent proarrow equipment pseudofunctor, its strict vertical 2-category, locally fully faithful hom action, and explicit square construction/round trips (hard)
Proposition C.3: Framed bicategory from equipment: An independent proarrow equipment pseudofunctor, its strict vertical 2-category, locally fully faithful hom action, and explicit square construction/round trips (hard)
Example2.3: Mod(C) construction: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Example2.4: double category of spans: Actual spans and commuting span squares, pullback horizontal composition, graph/cograph adjunction data, and induced oplax functors/transformations (hard)
Example2.8 and AppendixD: Adj(K): Internal bicategorical adjunctions, mate-pairs with explicit unit/counit formula and composition laws, and the double or doubly weak Adj construction (hard)
Equations4.9–4.12: representability of restriction and extension: Chosen restrictions/extensions as functors on horizontal hom-categories, globular natural isomorphisms, and coherent companion/conjoint pseudofunctors (hard)
Example5.6(ii): all span dual pairs are base change pairs: Actual spans and commuting span squares, pullback horizontal composition, graph/cograph adjunction data, and induced oplax functors/transformations (hard)
Equation5.12: closed framing has coextensions: Two-variable horizontal right adjoints with natural hom-bijections, evaluation maps, and their canonical comparison transformations (hard)
Remark6.18: full embedding of monoidal categories: Lax, oplax, and strong double functors; double transformations and their strict 2-category compositions (hard)
Example6.19: strict Mod 2-functor: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Example6.20: strict Span 2-functor: Actual spans and commuting span squares, pullback horizontal composition, graph/cograph adjunction data, and induced oplax functors/transformations (hard)
Example8.7: induced Mod adjunction: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Example8.8: induced Span adjunction: Actual spans and commuting span squares, pullback horizontal composition, graph/cograph adjunction data, and induced oplax functors/transformations (hard)
Example9.3: braided structure on D(I,I): External strong framed tensor, monoidal/braided constraints and interchange compatibility (hard)
Example9.6: symmetric structure on D(I,I): External strong framed tensor, monoidal/braided constraints and interchange compatibility (hard)
Examples9.8: monoidal lifts of Mod and Span: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Example11.2: monoids in Span are internal categories: Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Example11.8: Mod(Mat(V)) is Dist(V): Actual monoids, non-globular monoid maps, bimodule actions and equivariant maps; relative tensor as the action coequalizer and its functorial constraints (hard)
Remark12.12: cartesian fibers and cartesian total category: Strict monoidal total/base functor, full cartesian lifts, indexed strong monoidal fibers, fixed-base morphisms, and the monoidal Grothendieck 2-equivalence (hard)
Example12.13: retraction bifibration: Strict monoidal total/base functor, full cartesian lifts, indexed strong monoidal fibers, fixed-base morphisms, and the monoidal Grothendieck 2-equivalence (hard)
Equations13.26–13.27: projection formula criterion: Internal and external fiber tensor right adjoints, canonical base-change/projection mates, and weak/strong Beck–Chevalley predicates (hard)
Example14.12: Span factors through Fr: Definition 12.5 morphisms of frameable bifibrations and the actual induced strict Fr 2-functor, including product-comparison pushforward and transformations (hard)
Example14.13: Ex is 2-functorial: Definition 12.5 morphisms of frameable bifibrations and the actual induced strict Fr 2-functor, including product-comparison pushforward and transformations (hard)
Example14.16: disjoint-section framed adjunction: Definition 12.5 morphisms of frameable bifibrations and the actual induced strict Fr 2-functor, including product-comparison pushforward and transformations (hard)
Example15.4: family fibration and enriched construction: Strict monoidal total/base functor, full cartesian lifts, indexed strong monoidal fibers, fixed-base morphisms, and the monoidal Grothendieck 2-equivalence (hard)
Example15.5: pointed internal categories: Missing closure hypotheses for the general pointed-internal-category claim (source-ambiguity)
AppendixA: uniqueness and coherence of companions/conjoints: Chosen restrictions/extensions as functors on horizontal hom-categories, globular natural isomorphisms, and coherent companion/conjoint pseudofunctors (hard)
EquationB.1: vertical-discrete embedding adjunction: The actual horizontal bicategory and induced horizontal pseudofunctors, oplax transformations, modifications, local adjunctions, and full monoidal bicategory coherence where required (hard)
EquationB.2: lift framed transformations to oplax ones: The actual horizontal bicategory and induced horizontal pseudofunctors, oplax transformations, modifications, local adjunctions, and full monoidal bicategory coherence where required (hard)
EquationB.5: framed adjunction induces local adjunction: The actual horizontal bicategory and induced horizontal pseudofunctors, oplax transformations, modifications, local adjunctions, and full monoidal bicategory coherence where required (hard)
AppendixC: equipment/framing round trips: An independent proarrow equipment pseudofunctor, its strict vertical 2-category, locally fully faithful hom action, and explicit square construction/round trips (hard)
AppendixD: canonical equipment of adjunctions: Internal bicategorical adjunctions, mate-pairs with explicit unit/counit formula and composition laws, and the double or doubly weak Adj construction (hard)

Selected references

Framed bicategories and monoidal fibrations, arXiv:0706.1286v2, https://arxiv.org/abs/0706.1286v2

5 thms1 active userReviewed

Quantum Information·Captain: Gohan

Mapping stacks of topological stacksResearch Paper

Motivation

We prove that the mapping stack Map(Y,X) of topological stacks X and Y is again a topological stack if Y admits a compact groupoid presentation. If Y admits a locally compact groupoid presentation, we show that Map(Y,X) is a paratopological stack. In particular, it has a classifying space (hence, a natural weak homotopy type). We prove an invariance theorem which shows that the weak homotopy type of the mapping stack Map(Y,X) does not change if we replace X by its classifying space, provided that Y is paracompact topological space. As an example, we describe the loop stack of the classifying stack BG of a topological group G in terms of twisted loop groups of G.

This mission is the statement-level formalization of Mapping stacks of topological stacks (arXiv:0809.2373v2). 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 Right principal bundles over a paracompact cylinder are pulled back (Lemma 7.1, PDF p. 12). 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.

Deferred results

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

Theorem 1.1: Groupoid-valued CGTop stacks, quotient presentations, compact mapping stacks, and paratopological atlases (hard)
Theorem 1.2: Weakly parashrinkable classifying maps, induced mapping-stack morphisms, and universal weak equivalence (source-ambiguity)
Theorem 1.3: Milnor spaces, classifying stacks, twisted-loop classifying spaces, inertia and conjugation Borel comparison maps (hard)
Unnumbered after Theorem 1.1: classifying space and atlas: Representable stack pullbacks, parashrinkable classifying-space maps, epimorphic atlases and their groupoid presentations (hard)
Unnumbered §2.1: canonical weak homotopy type: Localization at weak equivalences and a comparison functor for homotopical CGTop stacks (hard)
Lemma 2.4: Representable morphisms, groupoid-valued evaluation and the topological approximation of a paratopological stack (hard)
Unnumbered after Lemma 2.4: other test-space classes: Class-relative stack atlas and comparison inducing equivalences on every test-space groupoid (hard)
Proposition 2.6: Paratopological stacks and parashrinkable maps from spaces, including the epimorphic strengthening (hard)
Proposition 2.7: Constructed Haefliger and Milnor classifying spaces with their canonical maps to quotient stacks (hard)
Proposition 2.9: Bicategory of CGTop stacks with genuine finite and arbitrary bilimits, plus stack-class predicates (hard)
Unnumbered §3: stackhood, points and space case: Groupoid-valued mapping pseudofunctor with descent, coarse points, and representability by a CG mapping space (hard)
Lemma 3.1: Mapping-stack pseudofunctors acting on 1-morphisms and invertible 2-morphisms with coherence (hard)
Lemma 3.2: Stack products, internal mapping stacks and a natural exponential equivalence of groupoid-valued stacks (hard)
Lemma 4.1: Representable stack diagonal, mapping stack, and representability of every space map into it (hard)
Theorem 4.2: Topological quotient stacks, groupoid presentations and the mapping-stack atlas over finite covers (hard)
Theorem 4.4: Paratopological target, locally compact presentation, mapping-stack descent and classifying-space comparison (hard)
Corollary 4.5: Lie-groupoid differentiable stacks and their underlying CGTop stacks, mapping stacks and classifying spaces (hard)
Proposition 5.1: Hurewicz topological stacks, Hausdorff finite-proper gluing and its canonical mapping-stack 2-pullback comparison (hard)
Unnumbered §5.2: path and free-loop closure: Path and free-loop stacks with constant paths, all evaluations, invertible comparison cells and naturality (hard)
Unnumbered §5.2: explicit loop-model comparisons: The two displayed free-loop models and their based 2-fibers, with natural Hurewicz-stack comparisons (hard)
Proposition 5.2: Source-pinned Hurewicz fibration for possibly nonrepresentable stack maps (source-ambiguity)
Unnumbered §5.3: replacement and homotopy-fiber closure: Constructed mapping-path replacement and homotopy-fiber 2-pullback in the stack bicategory (hard)
Lemma 6.2: Representable stack maps and nonempty weakly contractible topological spaces of lifts for every paracompact test (hard)
Theorem 6.4: Representable weakly parashrinkable stack morphisms, induced mapping morphism and universal weak equivalence (hard)
Corollary 6.5: Weakly parashrinkable space-to-stack maps and canonical mapping-space classifying maps (hard)
Corollary 6.6: Space and stack free-loop constructions and their induced weakly parashrinkable comparison map (hard)
Corollary 6.7: Composable representable stack maps and the lift-space definition of weak parashrinkability (hard)
Remark 6.8: source noninvariance: Milnor BG, classifying stack BG, induced source comparison, weak equivalence and a noninvariance witness (hard)
Lemma 7.2: Clutched quotient T_f with its CG topology, constructed projection and right action, and equivariant bundle isomorphisms (hard)
Unnumbered §7: twisted-loop special cases: Clutched torsor T_alpha, its automorphism topological group and twisted-loop isomorphisms for identity-component and discrete twists (hard)
Lemma 7.3: Constructed torsor-defined point p_alpha of the loop classifying stack, its 2-fibers and their topological-group structures (hard)
Lemma 7.4: Loop-stack morphism from the coproduct of torsor points and local lifts on every locally contractible paracompact test (hard)
Corollary 7.5: Quotient-stack comparison Pbar, evaluation equivalences on locally contractible paracompact tests and universal weak equivalence (hard)
Theorem 7.6: Canonical free-loop comparison maps among Milnor spaces, classifying stacks, twisted-loop classifying spaces and the discrete inertia/Borel models (hard)
Unnumbered §7: claimed based-loop fiber and square: Correct evaluation-action quotient fiber in place of the printed kernel-only classifying stack (source-ambiguity)
Theorem 7.7: Correct based-loop component theorem in place of the printed conjugacy-class formula (source-ambiguity)

Selected references

Mapping stacks of topological stacks, arXiv:0809.2373v2, https://arxiv.org/abs/0809.2373v2

3 thms1 active userReviewed

Quantum Information·Captain: Gohan

Linear programs for entanglement and key distribution in the quantum internetResearch Paper

Motivation

Quantum networks will allow to implement communication tasks beyond the reach of their classical counterparts. A pressing and necessary issue for the design of quantum network protocols is the quantification of the rates at which these tasks can be performed. Here, we propose a simple recipe that yields efficiently computable lower and upper bounds on the maximum achievable rates. For this we make use of the max-flow min-cut theorem and its generalization to multi-commodity flows to obtain linear programs. We exemplify our recipe deriving the linear programs for bipartite settings, settings where multiple pairs of users obtain entanglement in parallel as well as multipartite settings, covering almost all known situations. We also make use of a generalization of the concept of paths between user pairs in a network to Steiner trees spanning a group of users wishing to establish Greenberger-Horne-Zeilinger states.

This mission is the statement-level formalization of Linear programs for entanglement and key distribution in the quantum internet (arXiv:1809.03120v3). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

5 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Lemma 1, Eq.(57): path rounding (Lemma 1, Eq.(57): path rounding, 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.

Deferred results

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

Theorem 1, Eq.(1): bipartite LP sandwich: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Theorem 2, Eq.(2): total multipair sandwich: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Theorem 3, Eq.(3): worst-case multipair sandwich: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Theorem 4, Eq.(4): multipartite sandwich: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Proposition 1, Eq.(48): fixed-frequency generic converse: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Corollary 1, Eq.(50): optimized generic converse: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Proposition 2, Eq.(52): fixed-frequency routing lower bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Corollary 2, Eq.(53): fixed-frequency distillable equality: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Corollary 3, Eq.(72): optimized routing lower bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Unnumbered Eq.(73) and p.6: optimized distillable tightness: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Proposition 3, Eq.(87): fixed-frequency worst-case upper bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Proposition 4, Eq.(94): fixed-frequency total upper bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Corollary 4, Eqs.(98)–(99): optimized multipair upper bounds: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Proposition 5, Eq.(104): weighted upper polytope: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Proposition 6, Eqs.(105)–(106): multipair routing lower bounds: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Corollary 5, Eqs.(134)–(135): optimized multipair lower bounds: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Proposition 7, Eq.(138): weighted lower bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Proposition 8, Eq.(151): fixed-frequency multipartite upper bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Corollary 6, Eq.(152): optimized multipartite upper bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Proposition 9, Eq.(153): fixed-frequency GHZ lower bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Lemma 4, Eq.(154): connectivity rounding and parity: A true parity claim for the exact printed rounded multigraph (source-ambiguity)
Corollary 7, Eq.(171): optimized GHZ lower bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Unnumbered IV.D: polynomial-time computation claim: A finite coefficient/input and solution-accuracy model for the claimed real-data solver complexity (source-ambiguity)
Unnumbered V.B: universal single-path attainment claim: A justified scope or reduction ensuring arbitrary operational capacities have a single-path optimizer (source-ambiguity)
Unnumbered V.C.2: achievable convex hull, Eq.(137): An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Unnumbered V.C: concave objectives and relaxed upper polytopes: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)
Unnumbered V.C.1, Eq.(82): generalized cut rate bound: An ownership-aware adaptive network execution on arbitrary completed local quantum registers, including bosonic channels, computing the history law, normalized branch outputs, branch-dependent target dimensions and integer per-edge channel-use counters from one separably initialized local-instrument schedule; operational capacities from these outputs with expected budgets and the source limit order. (hard)

Selected references

Linear programs for entanglement and key distribution in the quantum internet, arXiv:1809.03120v3, https://arxiv.org/abs/1809.03120v3

6 thms1 active userReviewed

Quantum Information·Captain: Gohan

Compactly Generated Stacks: A Cartesian Closed Theory of Topological StacksResearch Paper

Motivation

A convenient bicategory of topological stacks is constructed which is both complete and Cartesian closed. This bicategory, called the bicategory of compactly generated stacks, is the analogue of classical topological stacks, but for a different Grothendieck topology. In fact, there is an equivalence of bicategories between compactly generated stacks and those classical topological stacks which admit locally compact Hausdorff atlases. Compactly generated stacks are also equivalent to a bicategory of topological groupoids and principal bundles, just as in the classical case. If a classical topological stack and a compactly generated stack have a presentation by the same topological groupoid, then they restrict to the same stack over locally compact Hausdorff spaces and are homotopy equivalent.

This mission is the statement-level formalization of Compactly Generated Stacks: A Cartesian Closed Theory of Topological Stacks (arXiv:0907.3925v3). 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 Paracompact Hausdorff spaces admit shrinkings (Proposition 2.2, PDF p. 12). 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.

Deferred results

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

Abstract: complete and Cartesian closed bicategory of compactly generated stacks: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; bicategoricalEquivalence; associatedStack; presentableStack; topologicalStack; compactlyGeneratedStack; mappingStack (hard)
Theorem 1.1: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack (hard)
Theorem 1.2: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; mappingStack (hard)
Theorem 1.3: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; weakHomotopyTypeFunctor; stackWeakHomotopyEquivalence (hard)
Theorem 1.4: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; paratopologicalStack; mappingStack; weakHomotopyTypeFunctor; stackWeakHomotopyEquivalence (hard)
Theorem 1.5: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; twoAdjunction; pullbackGroupoid; cechGroupoid; bundlization; associatedStack; topologicalStack; compactlyGeneratedStack; stackWeakHomotopyEquivalence; stackCoreflector; bicategoricalEssentialImage (hard)
Lemma 2.1: openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; actionGroupoid; translationGroupoid; localSections; principalBundle; bundleMapGroupoid; JMoritaEquivalence; associatedStack; groupoidNerve; fatRealization; universalBundle (hard)
Lemma 2.2: openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; actionGroupoid; translationGroupoid; localSections; principalBundle; unitBundle; gaugeGroupoid; JMoritaEquivalence; associatedStack; groupoidNerve; fatRealization; universalBundle; fibrantGroupoid; fibrantReplacement (hard)
Lemma 2.3: openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; actionGroupoid; translationGroupoid; localSections; principalBundle; unitBundle; gaugeGroupoid; JMoritaEquivalence; associatedStack; groupoidNerve; fatRealization; universalBundle; fibrantReplacement (hard)
Theorem 2.4: openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; translationGroupoid; localSections; principalBundle; unitBundle; bundleMapGroupoid; pullbackBundle; gaugeGroupoid; JMoritaEquivalence; extendedYoneda; associatedStack; universalBundle; fibrantGroupoid; fibrantReplacement; topologicalStack (hard)
Proposition 2.1: openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; representableStackMorphism; paratopologicalStack; topologicalStack (hard)
Theorem 2.5: CGHaus; openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; associatedStack; topologicalStack; mappingStack (hard)
Theorem 2.6: CGHaus; openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; associatedStack; topologicalStack; paratopologicalStack; mappingStack (hard)
Lemma 2.7: CGHaus; openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; representableStackMorphism; mappingStack (hard)
Theorem 2.8: CGHaus; openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; pullbackGroupoid; cechGroupoid; generalizedHomomorphism; associatedStack; topologicalStack; representableStackMorphism; JAtlas; mappingStack; internalGroupoidExponential (hard)
Theorem 2.9: CGHaus; openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; associatedStack; topologicalStack; JAtlas; paratopologicalStack; mappingStack; internalGroupoidExponential; fibrantReplacement (hard)
Proposition 3.1: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps (hard)
Lemma 3.1: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps (hard)
Theorem 3.2: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps; geometricEmbeddingFactorization (hard)
Corollary 3.2: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps (hard)
Lemma 3.3: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps (hard)
Corollary 3.3: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps (hard)
Proposition 3.4: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps (hard)
Corollary 3.4: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; descentGroupoid; plusConstruction; stackification; weakStackRestriction; weakRightExtension; bicategoricalUniversalProperties; bicategoricalEquivalence; twoAdjunction (hard)
Lemma 3.4: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; weakStackRestriction; bicategoricalUniversalProperties (hard)
Corollary 3.5: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; plusConstruction; stackification; weakStackRestriction; weakRightExtension; bicategoricalUniversalProperties (hard)
Proposition 3.5: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; presheafRestriction; presheafRightExtension; sheafReflectionMaps; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; weakStackRestriction; weakRightExtension; bicategoricalUniversalProperties (hard)
Theorem 4.1: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; weakStackRestriction; weakRightExtension; bicategoricalUniversalProperties; bicategoricalEquivalence; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; JMoritaEquivalence; extendedYoneda; associatedStack; presentableStack; topologicalStack; compactlyGeneratedStack; bicategoricalEssentialImage (hard)
Theorem 4.2: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; bicategoricalEquivalence; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; JMoritaEquivalence; generalizedHomomorphism; bicategoryOfFractions; extendedYoneda; associatedStack; topologicalStack; compactlyGeneratedStack (hard)
Theorem 4.3: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; bicategoricalEquivalence; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; principalBibundle; bundlization; bibundleTensor; JMoritaEquivalence; extendedYoneda; associatedStack; topologicalStack; compactlyGeneratedStack (hard)
Proposition 4.1: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; pullbackBundle; JMoritaEquivalence; associatedStack; topologicalStack; compactlyGeneratedStack (hard)
Corollary 4.1: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; bundleMapGroupoid; pullbackBundle; principalBibundle; JMoritaEquivalence; associatedStack; topologicalStack; compactlyGeneratedStack (hard)
Corollary 4.2: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; bicategoricalEquivalence; associatedStack; topologicalStack; compactlyGeneratedStack (hard)
Theorem 4.4: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; bicategoricalEquivalence; associatedStack; presentableStack; topologicalStack; JAtlas; compactlyGeneratedStack; bicategoricalEssentialImage (hard)
Theorem 4.5: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; fibrantReplacement (hard)
Corollary 4.3: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack (hard)
Lemma 4.6: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; associatedStack; topologicalStack; compactlyGeneratedStack; mappingStack (hard)
Corollary 4.4: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; mappingStack (hard)
Lemma 4.7: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; mappingStack (hard)
Theorem 4.8: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; mappingStack; truncatedCechNerve (hard)
Theorem 4.9: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; gaugeGroupoid; JMoritaEquivalence; associatedStack; topologicalStack; compactlyGeneratedStack; mappingStack; internalGroupoidExponential; universalBundle; fibrantReplacement (hard)
Corollary 4.5: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; JMoritaEquivalence; associatedStack; topologicalStack; compactlyGeneratedStack; groupoidNerve; fatRealization; spaceWeakHomotopyEquivalence (hard)
Lemma 4.11: spaceWeakHomotopyEquivalence; universalWeakEquivalence; diskTestSpaces (hard)
Corollary 4.6: spaceWeakHomotopyEquivalence; universalWeakEquivalence (hard)
Lemma 4.12: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; JCoveringMorphism; representableStackMorphism; compactlyGeneratedStack; stackMapPropertyLift (hard)
Theorem 4.13: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; actionGroupoid; translationGroupoid; localSections; principalBundle; JMoritaEquivalence; associatedStack; topologicalStack; JCoveringMorphism; representableStackMorphism; JAtlas; compactlyGeneratedStack; groupoidNerve; fatRealization; universalBundle; canonicalClassifyingAtlas; stackMapPropertyLift (hard)
Corollary 4.7: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; actionGroupoid; translationGroupoid; localSections; principalBundle; JMoritaEquivalence; associatedStack; topologicalStack; representableStackMorphism; compactlyGeneratedStack; groupoidNerve; fatRealization; universalBundle; canonicalClassifyingAtlas; universalWeakEquivalence; stackMapPropertyLift (hard)
Corollary 4.8: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; JMoritaEquivalence; associatedStack; topologicalStack; compactlyGeneratedStack; groupoidNerve; fatRealization; canonicalClassifyingAtlas; spaceWeakHomotopyEquivalence (hard)
Lemma 4.14: bicategoricalUniversalProperties; twoAdjunction; tauOne; representableMorphismClass (hard)
Theorem 4.15: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; JCoveringMorphism; JAtlas; compactlyGeneratedStack; groupoidNerve; fatRealization; canonicalClassifyingAtlas; spaceWeakHomotopyEquivalence; universalWeakEquivalence; stackMapPropertyLift; tauOne; representableMorphismClass; homotopyCategorySpaces; weakHomotopyTypeFunctor (hard)
Proposition 4.2: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; relativePairGroupoid; localSections; associatedStack; topologicalStack; JCoveringMorphism; representableStackMorphism; JAtlas; compactlyGeneratedStack; quasiTopologicalStack (hard)
Proposition 4.3: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; paratopologicalStack; quasiTopologicalStack (hard)
Lemma 4.16: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; representableStackMorphism; compactlyGeneratedStack; quasiTopologicalStack; stackMapPropertyLift (hard)
Corollary 4.9: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; representableStackMorphism; compactlyGeneratedStack; quasiTopologicalStack; fatRealization; canonicalClassifyingAtlas; universalWeakEquivalence; stackMapPropertyLift (hard)
Theorem 4.17: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; representableStackMorphism; compactlyGeneratedStack; quasiTopologicalStack; canonicalClassifyingAtlas; spaceWeakHomotopyEquivalence; universalWeakEquivalence; stackMapPropertyLift; tauOne; representableMorphismClass; homotopyCategorySpaces; weakHomotopyTypeFunctor (hard)
Theorem 4.18: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; quasiTopologicalStack; tauOne; representableMorphismClass; homotopyCategorySpaces; weakHomotopyTypeFunctor; stackWeakHomotopyEquivalence (hard)
Corollary 4.10: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; paratopologicalStack; quasiTopologicalStack; homotopyCategorySpaces; weakHomotopyTypeFunctor; stackWeakHomotopyEquivalence (hard)
Theorem 4.19: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; compactlyGeneratedStack; paratopologicalStack; quasiTopologicalStack; mappingStack; homotopyCategorySpaces; weakHomotopyTypeFunctor; stackWeakHomotopyEquivalence (hard)
Theorem 4.20: CGHaus; openCoverTopology; CGTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; twoAdjunction; pullbackGroupoid; cechGroupoid; unitBundle; principalBibundle; bundlization; bibundleTensor; associatedStack; topologicalStack; JCoveringMorphism; JAtlas; compactlyGeneratedStack; weakHomotopyTypeFunctor; stackWeakHomotopyEquivalence; stackCoreflector; bicategoricalEssentialImage (hard)
Lemma A.1: WeakGroupoidPresheaf; groupoidPresheafBicategory (hard)
Proposition A.1: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; truncatedCechNerve (hard)
Theorem B.1: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; bicategoricalEquivalence; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; unitBundle; principalBibundle; bundlization; bibundleTensor; JMoritaEquivalence; generalizedHomomorphism; bicategoryOfFractions; associatedStack (hard)
Theorem B.2: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; bicategoricalEquivalence; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; unitBundle; principalBibundle; bibundleTensor; JMoritaEquivalence; generalizedHomomorphism; bicategoryOfFractions; extendedYoneda; associatedStack; presentableStack (hard)
Corollary B.1: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; bundleMapGroupoid; pullbackBundle; JMoritaEquivalence; associatedStack (hard)
Proposition B.1: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; pairGroupoid; relativePairGroupoid; principalBundle; associatedStack; presentableStack; JCoveringMorphism; representableStackMorphism; JAtlas (hard)
Lemma B.3: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; JMoritaEquivalence; associatedStack; presentableStack; groupoidNerve; truncatedCechNerve (hard)
Unnumbered §1.1: Kelley coreflection, completeness and Cartesian closure of CGH: CGHaus; KelleyFunctor (hard)
Unnumbered Introduction: free loop stack is topological: CGHaus; openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; mappingStack (hard)
Claim §3.1: the sheaf-reflection unit on representables is an isomorphism: CGHaus; compactHausdorffInclusion; presheafRestriction; presheafRightExtension; sheafReflectionMaps (hard)
Unnumbered §3.1: adjoints for restriction to compact Hausdorff spaces: CGHaus; compactHausdorffInclusion; presheafRestriction; presheafRightExtension; presheafLeftExtension (hard)
Remark §3.1: sheafification commutes with restriction to CH: CGHaus; compactHausdorffInclusion; openCoverTopology; compactNeighborhoodTopology; presheafRestriction; sheafReflectionMaps (hard)
Unnumbered §3.2: weak adjoints to restriction: CGHaus; compactHausdorffInclusion; WeakGroupoidPresheaf; groupoidPresheafBicategory; weakStackRestriction; weakRightExtension; weakLeftExtension; twoAdjunction (hard)
Remark §4.2: embedding CGH in topological stacks with LCH atlases: CGHaus; openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; identityGroupoid; pairGroupoid; pullbackGroupoid; cechGroupoid; associatedStack; topologicalStack; bicategoricalEssentialImage; compactCechEmbedding (hard)
Unnumbered §4.4: same presentation gives same weak type and LCH restriction: CGHaus; openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; associatedStack; topologicalStack; quasiTopologicalStack; canonicalClassifyingAtlas; homotopyCategorySpaces; weakHomotopyTypeFunctor; stackWeakHomotopyEquivalence (hard)
Example 1: compact-subset Cech groupoid realizes the weak type of a space: CGHaus; openCoverTopology; WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; TopologicalGroupoid; identityGroupoid; pairGroupoid; relativePairGroupoid; pullbackGroupoid; cechGroupoid; groupoidAction; localSections; principalBundle; JMoritaEquivalence; associatedStack; topologicalStack; groupoidNerve; fatRealization; spaceWeakHomotopyEquivalence (hard)
Remark Appendix A: weak presheaves are complete and cocomplete: WeakGroupoidPresheaf; groupoidPresheafBicategory; bicategoricalUniversalProperties (hard)
Unnumbered Appendix A: descent criterion using a basis: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; descentGroupoid; truncatedCechNerve (hard)
Unnumbered Appendix A: triple-plus stackification and reflection: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; descentGroupoid; plusConstruction; stackification; bicategoricalUniversalProperties; twoAdjunction (hard)
Remark Appendix A: stacks are complete and cocomplete: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties (hard)
Unnumbered Appendix A: Cartesian closure of stacks: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; bicategoricalUniversalProperties; mappingStack (hard)
Remark Appendix B.1: completeness of TOPGpd: TopologicalGroupoid; bicategoricalUniversalProperties (hard)
Unnumbered Definition B.11: principal bundle maps are isomorphisms: TopologicalGroupoid; groupoidAction; localSections; principalBundle; bundleMapGroupoid (hard)
Remark Appendix B.3: Morita equivalence and global sections: TopologicalGroupoid; localSections; JMoritaEquivalence (hard)
Unnumbered Appendix B.3: right calculus of Morita fractions: TopologicalGroupoid; identityGroupoid; pullbackGroupoid; cechGroupoid; groupoidAction; localSections; principalBundle; JMoritaEquivalence; generalizedHomomorphism; bicategoryOfFractions; associatedStack (hard)
Unnumbered Appendix B.3: equivalences are biprincipal bibundles: TopologicalGroupoid; identityGroupoid; groupoidAction; localSections; principalBundle; principalBibundle; bibundleTensor; JMoritaEquivalence; associatedStack (hard)
Remark Appendix B.4: extended Yoneda and stackified presentations preserve limits: WeakGroupoidPresheaf; groupoidPresheafBicategory; JStack; stackification; bicategoricalUniversalProperties; cechGroupoid; generalizedHomomorphism; extendedYoneda; associatedStack (hard)
Remark §2.1: fibrant replacement preserves CGH: CGHaus; TopologicalGroupoid; translationGroupoid; gaugeGroupoid; fatRealization; fibrantReplacement (hard)
Remark Appendix B.3: cover Cech augmentation is J-Morita: TopologicalGroupoid; cechGroupoid; localSections; JMoritaEquivalence (hard)

Selected references

Compactly Generated Stacks: A Cartesian Closed Theory of Topological Stacks, arXiv:0907.3925v3, https://arxiv.org/abs/0907.3925v3

7 thms1 active userReviewed

Quantum Information·Captain: Gohan

Entanglement Entropy in the O(N) modelResearch Paper

Motivation

It is generally believed that in spatial dimension d > 1 the leading contribution to the entanglement entropy S = - tr rho_A log rho_A scales as the area of the boundary of subsystem A. The coefficient of this "area law" is non-universal. However, in the neighbourhood of a quantum critical point S is believed to possess subleading universal corrections. In the present work, we study the entanglement entropy in the quantum O(N) model in 1 < d < 3. We use an expansion in epsilon = 3-d to evaluate i) the universal geometric correction to S for an infinite cylinder divided along a circular boundary; ii) the universal correction to S due to a finite correlation length. Both corrections are different at the Wilson-Fisher and Gaussian fixed points, and the epsilon -> 0 limit of the Wilson-Fisher fixed point is distinct from the Gaussian fixed point. In addition, we compute the correlation length correction to the Renyi entropy S_n = (log tr rho^n_A)/(1-n) in epsilon and large-N expansions. For N -> infinity, this correction generally scales as N^2 rather than the naively expected N. Moreover, the Renyi entropy has a phase transition as a function of n for d close to 3.

This mission is the statement-level formalization of Entanglement Entropy in the O(N) model (arXiv:0904.4477v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

4 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Square-torus inverse Laplacian: theta formula and Fourier normalization (§V A (5.13)–(5.14): zero-mean square-torus Green function, PDF p. 27). 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.

Deferred results

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

Abstract main result, pinned to (1.11)/(4.86): Wilson–Fisher correlation-length entropy coefficient: Renormalized O(N) replica partition functions and the mass-gap-normalized entropy coefficient (hard)
§III (3.4)–(3.11): scaling integral and parametric enhancement: Mass-gap-dependent one-point scaling function and replica free-energy differentiation (hard)
§IV A (4.5)–(4.8): Gaussian correlation-length coefficients: Gaussian cone determinant, coincident subtraction, and entropy residue (hard)
§IV B (4.19)–(4.21): induced boundary coupling and its beta function: Boundary insertion Feynman amplitudes and MS/cutoff beta-coefficient extraction (hard)
§IV B (4.22)–(4.25), Fig.5: perturbative fixed points and RG flow: Maximal infrared flow and nested joint asymptotics of the retained boundary beta polynomial (hard)
§I/§IV B: nonanalytic replica dependence and two universal branches: §I/§IV B: nonanalytic replica dependence and two universal branches (source-ambiguity)
§IV B (4.27)–(4.31): Wilson–Fisher Renyi coefficient and cancellation near n=1: Stable-branch renormalized tadpole and nested Renyi-coefficient extraction (hard)
§IV B (4.32)–(4.34): boundary OPE exponent: Boundary OPE exponent extracted from renormalized two-point correlations (hard)
§IV C1 (4.35)–(4.46): inhomogeneous RG equation and scaling solution: Renormalized Fourier transform Phi, additive counterterm, and inhomogeneous RG solution (hard)
§IV C3–4 (4.63)–(4.65): free conical tadpole to first order in n-1: Dimensionally continued free cone tadpole from an independent Green kernel (hard)
§IV C4 (4.75)–(4.81): metric variation of conical propagator: Distributional inverse of the metric-dependent kinetic operator and its variation (hard)
§IV C2–4 (4.47)–(4.85): MS two-loop boundary beta function and entropy amplitude: Two-loop boundary graph counterterms and entropy-amplitude matching (hard)
§V A (5.6)–(5.10): periodized propagator and finite-size subtraction: Twisted cone inverse kernel and regulated periodization/diagonal subtraction (hard)
§V A (5.11)–(5.12): Gaussian geometric coefficient in D=3: Three-dimensional free replica determinant and universal finite-size entropy (hard)
§V A (5.15)–(5.16), (1.9): Gaussian geometric coefficient in D=4: Four-dimensional free spatial entropy from the subtracted cone determinant (hard)
§V B (5.17)–(5.21): interacting geometric Renyi coefficient: Interacting finite-size replica functional with boundary insertion (hard)
§V C (5.30)–(5.31), (1.7): Wilson–Fisher geometric coefficient: Wilson-Fisher geometric entropy coefficient from renormalized finite-size free energy (hard)
§V C (5.34)–(5.35): quasi-zero-mode estimate of validity: Normalized quasi-zero-mode projection and its tree-level effective action (hard)
§I (1.8)/§V C (5.36): conjecture at periodic zero twist: §I (1.8)/§V C (5.36): conjecture at periodic zero twist (source-ambiguity)
§VI (6.1)–(6.7): large-N saddle reduction and correlation-length normalization: Nonlinear sigma-model saddle, common point splitting, and massive gap normalization (hard)
§VI (6.8)–(6.21): spectral propagator, boundary branch, and infrared obstruction: Signed Bessel-branch resolvent with self-adjoint domain and dimensional continuation (hard)
§VI (6.21)–(6.25): explicit gap equation and existence: Continued spectral gap functional including its negative-alpha residue (hard)
§VI (6.26)–(6.31): near-one saddle and vanishing N-squared entropy term: Saddle branch connected to n=1 and the enhanced entropy coefficient (hard)
§VI (6.36)–(6.37): additional near-threshold saddle: Near-endpoint saddle branch of the full spectral gap functional (hard)
§VI (6.38): D=3 large-N Renyi coefficient: Physical D=3 saddle free energy and its leading large-N Renyi amplitude (hard)
§VI numerical findings, Table I, and root-count qualification: §VI numerical findings, Table I, and root-count qualification (source-ambiguity)

Selected references

Entanglement Entropy in the O(N) model, arXiv:0904.4477v1, https://arxiv.org/abs/0904.4477v1

5 thms1 active userReviewed

Quantum Information·Captain: Gohan

On the existence of bibundlesResearch Paper

Motivation

We consider the existence of bibundles, in other words locally trivial principal $G$ spaces with commuting left and right $G$ actions. We show that their existence is closely related to the structure of the group $\Out(G)$ of outer automorphisms of $G$ . We also develop a classifying theory for bibundles. The theory is developed in full generality for $(H, G)$ bibundles for a crossed-module $(H, G)$ and we show with examples the close links with loop group bundles.

This mission is the statement-level formalization of On the existence of bibundles (arXiv:1102.4388v2). 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 Existence and reduction: exactness of (3.3) (§1 / §3, unnumbered main existence result: exactness of (3.3), PDF p. 12). 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.

Deferred results

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

Proposition 2.8: Isomorphism-class group of all topological (H,G) bispaces and its actual Type homomorphism (hard)
Lemma 3.2: Geometric internal tensor and dual bibundles and their induced isomorphism-class group (hard)
§3, obstruction exact sequence (3.4): The specified cohomology model H2(M,G1) and multiplicative compatibility of the lifting obstruction (source-ambiguity)
§3, unnumbered extension to 3-groups: Higher exactness and coherent lifting-gerbe morphism into the 3-group of G1 gerbes (source-ambiguity)
Proposition 3.9: Canonical Aut(G) crossed module for simply connected semisimple Lie G (hard)
§3.2, sections classify bibundle structures on fixed P: Diagonal associated quotient P times_G H, its continuous sections, and the natural pullback comparison (hard)
Theorem 3.11: Type-constant slice-homotopy classes and the canonical pullback map to bibundle isomorphism classes (hard)
Note 3.3, concordance classification: Concordance relation of actual bibundles and its quotient, distinct from isomorphism (hard)
Theorem 3.12: Chosen universal principal G-bundle EG to BG and its diagonal bibundle quotient (hard)
§3.6, universal bibundle comparison (3.13): Chosen equivariant universal total group EG and the normal subgroup quotient of EG semidirect H (hard)
Lemma 3.13: External balanced product of the actual group-model bibundle over B times B (hard)
Proposition 3.14: Actual group-model pullbacks, tensor and dual with their comparison maps (hard)
Theorem 3.15: Group structures on all-types slice-homotopy and bibundle isomorphism quotients, with actual pullback (hard)
§3.7, bibundle-structure lifting criterion: Actual universal principal classifying maps and the projection B(H,G) to BG (hard)
Example 3.11, explicit path-loop classifying group: Smooth based path and endpoint-loop topological groups with actual path-fibration model (hard)
Example 3.12, ordinary homotopy does not classify isomorphism: Pullbacks of the actual smooth path-loop universal bibundle for a compact connected nontrivial Lie K (hard)
§3.8, general exact sequence of classifying groups: Normal quotient group B(H,G), EG/G1 and their actual kernel inclusion and type homomorphism (hard)
§4, unnumbered change of bibundle gerbe by R: Smooth bibundle gerbes, balanced products over submersion fibre powers, and the canonical contraction product (hard)
§4, type/band bundle of a bibundle gerbe (4.2): Gerbe product type cocycle and actual quotient descent to the principal band bundle (hard)

Selected references

On the existence of bibundles, arXiv:1102.4388v2, https://arxiv.org/abs/1102.4388v2

18 thms1 active userReviewed

Quantum Information·Captain: Gohan

Reflection positive one-parameter groups and dilationsResearch Paper

Motivation

The concept of reflection positivity has its origins in the work of Osterwalder--Schrader on constructive quantum field theory. It is a fundamental tool to construct a relativistic quantum field theory as a unitary representation of the Poincare group from a non-relativistic field theory as a representation of the euclidean motion group. This is the second article in a series on the mathematical foundations of reflection positivity. We develop the theory of reflection positive one-parameter groups and the dual theory of dilations of contractive hermitian semigroups. In particular, we connect reflection positivity with the outgoing realization of unitary one-parameter groups by Lax and Phillips. We further show that our results provide effective tools to construct reflection positive representations of general symmetric Lie groups, including the ax+b-group, the Heisenberg group, the euclidean motion group and the euclidean conformal group.

This mission is the statement-level formalization of Reflection positive one-parameter groups and dilations (arXiv:1312.6161v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

13 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is OS descent and adjoint compatibility for densely defined operators (Lemma 2.2, 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.

Deferred results

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

Lemma 3.11: Smooth-orbit Frechet space, continuous antilinear distribution dual, and integrated action (hard)
Proposition 3.14: Translation representation on vector-valued L2 and equivalence preserving the outgoing subspace (hard)
Lemma 3.19: Hardy reflection multiplier on L2(R), its positive subspace, and the Laplace quotient (hard)
Proposition 4.1: Canonical operator-valued RKHS dilation and equivalence of minimal euclidean realizations (hard)
Proposition 4.2: Operator-density L2 dilation and cutoff distributional Fourier-support subspaces (hard)
Proposition 4.4: Unbounded positive generator calculus and the explicit outgoing isometry (hard)
Lemma 5.4: Lemma 5.4: a source-pinned full-domain correction (source-ambiguity)
Lemma 5.5: Equivariant GNS/Poisson dilation and the symmetric Lie representation domain (hard)
Proposition 5.8: Positive affine-group representation and its genuine euclidean realization (hard)
Theorem 5.16: Generalized free-field Poisson measure, generated distribution RKHS, and H-equivariant quotient (hard)
Lemma 5.17: Lemma 5.17: a source-pinned full-domain correction (source-ambiguity)
Lemma 5.18: Normalized power-law measure family and its measure-normalized Fourier distribution (hard)
Theorem 5.19: Concrete euclidean conformal group, complementary series, and a covering of SO(2,d)_0 (hard)
Lemma 5.20: The Poisson Heisenberg model, algebraic Schwartz tensor core, and its projection (hard)
Proposition 5.21: Heisenberg symmetric Lie group and euclidean realization via a derived-invariant core (hard)
Proposition A.4: Antilinear Fourier distributions with full convolution and halfspace reflection positivity (hard)
Lemma A.5: Restriction and symmetric extension of antilinear distributions across zero (hard)
Theorem A.6: Full distribution classification with the canonical Poisson mixture and local-integrability bridge (hard)
Proposition A.8: Reflection-positive distribution extension of a tempered-measure Laplace transform (hard)
Theorem B.1: Theorem B.1: a source-pinned full-domain correction (source-ambiguity)
Lemma C.3: Completed operator-valued kernel space, its inclusion iota, and the generally unbounded GNS action (hard)
Lemma D.1: Bounded star-character cone and the antilinear Fourier-Laplace functional (hard)
Lemma D.6: Halfspace Fourier-Laplace functional and smooth-dual weighted multiplier vectors (hard)
Lemma D.7: Smooth-vector graph Frechet topology, weighted-L2 antilinear dual, and canonical constant-vector interpretation (hard)
Corollary D.8: Concrete vector-group multiplier smooth dual, constant vector, and Fourier-test action (hard)
1.8.fock: Completed coherent-kernel Fock space, vacuum, and canonical OS intertwiner (hard)
3.15.multiplier: Vector-valued L2 Fourier multiplier/reflection and its inverse-Fourier distribution (hard)
3.18.process-cyclicity: 3.18.process-cyclicity: a source-pinned full-domain correction (source-ambiguity)
4.L2-model: Canonical operator-density L2 model, constant embedding and its actual adjoint (hard)
4.2.multiplication: Canonical scalar-product-measure dilation with a.e. L2 actions and OS equivalence (hard)
5.12.free-field: Mass-shell measure, its dilation product and the onto projection pullback (hard)
5.17.power-law: Normalized mass-shell mixture and its projected measure (hard)
5.22.outgoing-heisenberg: Concrete outgoing Weyl pair and a.e. theta multiplier compatibility (hard)
A.7.nonuniqueness: Polynomial differential operator on delta0 and the reflection-positive distribution cone (hard)
B.1.mixture-temperedness: Measurable mass-shell kernel, canonical measure mixture, and spatial pushforward (hard)

Selected references

Reflection positive one-parameter groups and dilations, arXiv:1312.6161v2, https://arxiv.org/abs/1312.6161v2

14 thms1 active userReviewed

Quantum Information·Captain: Gohan

Bipartite Units of Non-LocalityResearch Paper

Motivation

Imagine a task in which a group of separated players aim to simulate a statistic that violates a Bell inequality. Given measurement choices the players shall announce an output based solely on the results of local operations -- which they can discuss before the separation -- on shared random data and shared copies of a so-called unit correlation. In the first part of this article we show that in such a setting the simulation of any bipartite correlation, not containing the possibility of signaling, can be made arbitrarily accurate by increasing the number of shared Popescu-Rohrlich (PR) boxes. This establishes the PR box as a simple asymptotic unit of bipartite nonlocality. In the second part we study whether this property extends to the multipartite case. More generally, we ask if it is possible for separated players to asymptotically reproduce any nonsignaling statistic by local operations on bipartite unit correlations. We find that non-adaptive strategies are limited by a constant accuracy and that arbitrary strategies on n resource correlations make a mistake with a probability greater or equal to c/n, for some constant c.

This mission is the statement-level formalization of Bipartite Units of Non-Locality (arXiv:0808.0651v4). 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 The corrected smaller resource is a permutation system (Lemma 1: the reduced resource is a permutation system (corrected construction), 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.

Deferred results

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

Theorem 1: PR boxes are an asymptotic unit of bipartite nonlocality (seed): A finite asynchronous local-port wiring evaluator with resource identities and at-most-once use, arbitrary local next-resource choices, input-independent shared probability law, independent resource copies, and the computed joint output law. It must allow one port to answer before the opposite port is queried and permit different local resource orders. (hard)
Lemma 4: binary permutation resources approximate every permutation system: A finite asynchronous local-port wiring evaluator with resource identities and at-most-once use, arbitrary local next-resource choices, input-independent shared probability law, independent resource copies, and the computed joint output law. It must allow one port to answer before the opposite port is queried and permit different local resource orders. A resource-family restriction identifying each copy as a binary uniform graph/XOR law. (hard)
Unnumbered performance estimate (17): cost in R resources: The general finite wiring evaluator plus a count equal to actual R resource instances and a recursive alphabet-reduction substitution tree. (hard)
Theorem 2: explicit PR-box resource bound: The general finite wiring evaluator, actual PR-copy count, rational-replacement interface and compositional approximation estimate. (hard)
Lemma 6: partner-specific output dependence forces simulation error: A finite asynchronous local-port wiring evaluator with resource identities and at-most-once use, arbitrary local next-resource choices, input-independent shared probability law, independent resource copies, and the computed joint output law. It must allow one port to answer before the opposite port is queried and permit different local resource orders. A five-party wiring restriction separating input dependence by partner and a measure-valued partial-history minority integral. (hard)
Theorem 3: restricted R-protocols admit a local approximation with constant-factor loss: A finite asynchronous local-port wiring evaluator with resource identities and at-most-once use, arbitrary local next-resource choices, input-independent shared probability law, independent resource copies, and the computed joint output law. It must allow one port to answer before the opposite port is queried and permit different local resource orders. The partner input-dependence restriction and an actual five-party shared-randomness local-mixture law. (hard)
Corollary 1: non-adaptive bipartite resources are not a multipartite unit: A finite asynchronous local-port wiring evaluator with resource identities and at-most-once use, arbitrary local next-resource choices, input-independent shared probability law, independent resource copies, and the computed joint output law. It must allow one port to answer before the opposite port is queried and permit different local resource orders. An outer non-adaptive protocol class over arbitrary finite bipartite no-signaling resources. (hard)
Lemma 7: minority-potential decrement after replacing one local output by a fair bit: A physically modified local fair-bit wiring experiment, reachable prefix minority potential, and an independent justification of the printed decrement inequality. (source-ambiguity)
Lemma 8: printed factor-two adaptive minority bound (deferred): A valid source correction to the printed coefficient 2/n. (source-ambiguity)
Theorem 4: reciprocal-error lower bound for adaptive R simulations: A finite asynchronous local-port wiring evaluator with resource identities and at-most-once use, arbitrary local next-resource choices, input-independent shared probability law, independent resource copies, and the computed joint output law. It must allow one port to answer before the opposite port is queried and permit different local resource orders. Actual per-player incident-resource count and independent resolution of the adaptive minority argument. (hard)
Unnumbered specialization: the reciprocal lower bound also holds for PR resources: A finite asynchronous local-port wiring evaluator with resource identities and at-most-once use, arbitrary local next-resource choices, input-independent shared probability law, independent resource copies, and the computed joint output law. It must allow one port to answer before the opposite port is queried and permit different local resource orders. A PR-resource specialization of the general adaptive R-network interface with per-player count. (hard)
Unnumbered main conclusion: every correlated nonlocal box is an asymptotic bipartite unit: A finite asynchronous local-port wiring evaluator with resource identities and at-most-once use, arbitrary local next-resource choices, input-independent shared probability law, independent resource copies, and the computed joint output law. It must allow one port to answer before the opposite port is queried and permit different local resource orders. Resource substitution for approximate PR distillation from the correlated-box family. (hard)

Selected references

Bipartite Units of Non-Locality, arXiv:0808.0651v4, https://arxiv.org/abs/0808.0651v4

7 thms1 active userReviewed

Quantum Information·Captain: Gohan

Routing entanglement in the quantum internetResearch Paper

Motivation

Remote quantum entanglement can enable numerous applications including distributed quantum computation, secure communication, and precision sensing. In this paper, we consider how a quantum network-nodes equipped with limited quantum processing capabilities connected via lossy optical links-can distribute high-rate entanglement simultaneously between multiple pairs of users (multiple flows). We develop protocols for such quantum "repeater" nodes, which enable a pair of users to achieve large gains in entanglement rates over using a linear chain of quantum repeaters, by exploiting the diversity of multiple paths in the network. Additionally, we develop repeater protocols that enable multiple user pairs to generate entanglement simultaneously at rates that can far exceed what is possible with repeaters time sharing among assisting individual entanglement flows. Our results suggest that the early-stage development of quantum memories with short coherence times and implementations of probabilistic Bell-state measurements can have a much more profound impact on quantum networks than may be apparent from analyzing linear repeater chains. This framework should spur the development of a general quantum network theory, bringing together quantum memory physics, quantum information theory, and computer network theory.

This mission is the statement-level formalization of Routing entanglement in the quantum internet (arXiv:1708.07142v2). 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 Parallel attempts: probability of one usable external link (§II.A: parallel optical attempts give the effective link probability, 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.

Deferred results

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

Abstract single-flow capstone, pinned to Appendix B.2, Eq.(B5): Computed L2 local port-pairing policy, its tie randomness, countable-lattice success-flag experiment, and actual delivered-ebit count/rate (hard)
§II.B.1 / Fig.4(a,b): percolation and global rate-distance scaling: Infinite-square-lattice greedy execution and measurable connection/delivered-count interface for the Bernoulli bond measure (hard)
Fig.4 and §II.B.2: numerical global/local/linear comparison and directional enhancement: Numerical tolerances, raw Monte Carlo data and complete finite-grid boundary specification (source-ambiguity)
Appendix B.2 final paragraph and §II.B.2: local advantage away from horizontal separation: Computed L2 local port-pairing policy, its tie randomness, countable-lattice success-flag experiment, and actual delivered-ebit count/rate (hard)
§II.C: synchronized single-flow time sharing gives the baseline rate segment: Computed single-flow L2 local policies and the shared-schedule execution on all nodes (hard)
§II.C / Fig.6: leftover entanglement and improved multi-flow time sharing: Complete terminal-excluding two-flow stochastic policy and rate attribution (source-ambiguity)
§II.C / Fig.6: spatial division versus time sharing, crossing and noncrossing: Exact spatial-boundary assignment, terminal operations, and quantitative performance margins (source-ambiguity)
Appendix A / Fig.8: recursive rate-distance metrics and L2 comparison: Quantified metric comparison or convergence/optimality claim and zero-rate reciprocal convention (source-ambiguity)
Appendix A: deterministic perfect-link setting does not make the proposed local rule optimal: Actual p=q=1 L2 local delivery distribution under the fair routing ties (hard)
Appendix B.1 / Fig.9: empirical exponential fit and p,q improvement trend: Mathematically defined fitted functions f,g and fit-error/parameter-trend specification (source-ambiguity)
Appendix B.2, Eq.(B1): two-hop black-path improvement: Fig.10 labeled black-path event with the actual incident-link local decisions (hard)
Appendix B.2, Eqs.(B2)–(B4): positive dependence across shared link 9: Joint Fig.10 black-path events, conditioning on shared link 9, and local connection at v (hard)

Selected references

Routing entanglement in the quantum internet, arXiv:1708.07142v2, https://arxiv.org/abs/1708.07142v2

6 thms1 active userReviewed

Quantum Information·Captain: Gohan

Proof of the Holographic Formula for Entanglement EntropyResearch Paper

Motivation

Entanglement entropy for a spatial partition of a quantum system is studied in theories which admit a dual description in terms of the anti-de Sitter (AdS) gravity one dimension higher. A general proof of the holographic formula which relates the entropy to the area of a codimension 2 minimal hypersurface embedded in the bulk AdS space is given. The entanglement entropy is determined by a partition function which is defined as a path integral over Riemannian AdS geometries with non-trivial boundary conditions. The topology of the Riemannian spaces puts restrictions on the choice of the minimal hypersurface for a given boundary conditions. The entanglement entropy is also considered in Randall-Sundrum braneworld models where its asymptotic expansion is derived when the curvature radius of the brane is much larger than the AdS radius. Special attention is payed to the geometrical structure of anomalous terms in the entropy in four dimensions. Modification of the holographic formula by the higher curvature terms in the bulk is briefly discussed.

This mission is the statement-level formalization of Proof of the Holographic Formula for Entanglement Entropy (arXiv:hep-th/0606184v2). 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 A finite exterior BTZ geodesic turns before the horizon (Section 2, following (2.13), PDF p. 9). 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.

Deferred results

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

Abstract main result, pinned to (2.12) and conditions 1–4: The gravitational integration measure/domain, an operation extracting semiclassical leading entropy, and a rule selecting the noninteger replica continuation are not specified. Integer beta values do not determine its derivative. Defining entropy by area, assuming its desired derivative, or inventing a continuation deletes the physical content. This is source ambiguity, not missing Lean geometry. (source-ambiguity)
(1.1): cited planar entropy-density conjecture: Deferred background conjecture, not a theorem proved here. Neither fundamental microscopic theory nor infinite-plane density limit is defined in this source. (source-ambiguity)
(1.2): conditional Kaluza-Klein product-area conversion: Product Riemannian geometry and its induced finite volume (hard)
(1.3): prior static RT proposal and applications: Deferred cited proposal/applications: exact underlying CFT and application models are not given here and no accepted holographic interface was found. Do not claim a general previously proved RT theorem. (source-ambiguity)
(2.1),(2.6): assumed extended Euclidean AdS/CFT: Deferred assumed duality: no integration measure/domain or construction of the dual CFT is supplied, and it is introduced as a conjecture. Arbitrary scalar partition functions cannot stand in for the stated theories. (source-ambiguity)
(2.4)–(2.5): cited replica identity and continuation: The field path-integral measure and selection of its noninteger continuation are not supplied. Smooth continuations can agree at all integers but differ in derivative at 2*pi. Defer the cited physical identity rather than selecting an arbitrary interpolation. (source-ambiguity)
Section 2, p.6: stationary rotating-frame extension: The source specifies quotient identifications but no analytic domain/branch or conditions justifying Omega->i*Omega. It also inherits the unspecified replica continuation and path integral. (source-ambiguity)
(2.7): conical Einstein action contribution: Curvature measure and regulated Einstein action of an actual cyclic cone (hard)
Section 2, p.7: no extra conical boundary terms: Allowed invariant functions f and regulator class are not fully pinned. The dimensional inconsistency also needs interpretation. A universal no-boundary-term theorem requires extra unprovided restrictions. (source-ambiguity)
(2.9)–(2.11): Einstein and stationary-surface variation: Independent metric and embedding variations of the constructed conical action (hard)
Section 2, p.9, Figures 2–3: complementary-cut obstruction: Embedded solid-torus cuts, their oriented boundaries and nonzero longitude homology (hard)
(3.2)–(3.5): cited RS effective-action expansion: Deferred cited expansion: no scheme/construction of Gamma_RS, higher Ik or remainder order/topology is given. Explicit first two local functionals can still be constructed for the new coefficient results below. (source-ambiguity)
(3.6): U(N) CFT/supergravity dictionary: Deferred physical dictionary: no construction of the U(N) theory or coupling/rank map is given here. Declaring this scalar equality as a structure field assumes its content. (source-ambiguity)
(3.9): two-sided RS junction and bulk-surface equations: Two-sided RS action, variational matter stress tensor, and branch variations (hard)
(3.7)–(3.10): RS semiclassical doubled-area entropy: The gravitational measure, replica continuation and leading-order entropy operation remain unselected as in Section 2. Defining S_RS by doubled area would replace rather than state the result. (source-ambiguity)
(3.11)–(3.12): entropy expansion and complementary vacuum terms: Thermal functional is inconsistently specified and no full correction sequence/remainder is given. This prevents a uniquely determined all-order entropy expansion and universal claim about its thermal/vacuum split. (source-ambiguity)
Section 3, p.11: cited high-temperature extensivity: Deferred cited asymptotic: coefficient, phase/limit assumptions and precise remainder/dominance are absent here; S_TH is also inconsistent in (3.12). (source-ambiguity)
(4.1), p.12: induced Einstein entropy coefficient: Actual induced Einstein local action and its regularized replica differential coefficient (hard)
(4.2): quadratic-curvature entropy coefficient: Ambient curvature contractions, induced I2 functional and its smoothed replica variation (hard)
Section 4, p.12: cited smoothing independence: Deferred cited all-order claim: admissible smoothing class, general Ik and convergence conditions are not specified. This does not prevent constructing a concrete smoothing and evaluating the explicitly given local functionals. (source-ambiguity)
(4.3): d=4 logarithmic geometric entropy: Separate four-dimensional logarithmic counterterm and its geometric replica coefficient (hard)
(4.4): printed Weyl law for normal curvature contractions: For constant nonzero omega the derivative terms vanish, yet the scalar curvature contraction scales by exp(2*omega). Literal (4.4) lacks this factor; choosing a density interpretation or corrected scalar law requires an explicit source correction. (source-ambiguity)
(4.5): candidate general anomaly with undetermined lambda: The physical coefficient of the conformal invariant is not determined in this source; arbitrary lambda values cannot all be actual entropy of one fixed theory. The candidate family is recorded exactly, but no completed physical entropy value is invented; (4.4) adds a source ambiguity. (source-ambiguity)
(5.2)–(5.3): Gauss-Bonnet conical action: Smoothed Einstein-Gauss-Bonnet action and intrinsic branch curvature (hard)
(5.4): semiclassical GB entropy correction: Physical entropy identification inherits unspecified gravitational measure, replica continuation and leading-order operation. Omitted GB boundary terms also exclude a universal exact law. Geometric conical coefficient is separately stateable. (source-ambiguity)
(5.5)–(5.6): GB surface Euler-Lagrange embedding equation: Induced-metric curvature functional and its embedding first variation (hard)
(6.1): flat-brane planar ground-state entropy density: No infinite-plane regulator/density limit is selected; this uses the unpinned full entropy expansion and inconsistent S_TH definition. Computing a local geometric area density alone would not establish the microscopic entropy claim. (source-ambiguity)
Section 6, pp.14–15: string/brane parameter relations: Deferred background string dictionary: underlying string/CFT theories and the physical coupling map are not constructed. Arbitrary scalar assumptions only restate, rather than establish, that dictionary. (source-ambiguity)
Section 6, p.15: spin-chain/effective-QFT comparison: Deferred cited comparison: details needed to select a definite model, limit and entropy expression are explicitly referred to [1], outside the supplied source. (source-ambiguity)

Selected references

Proof of the Holographic Formula for Entanglement Entropy, arXiv:hep-th/0606184v2, https://arxiv.org/abs/hep-th/0606184v2

4 thms1 active userReviewed

Quantum Information·Captain: Gohan

On Cohomology theory for topological groupsResearch Paper

Motivation

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

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

What is formalized

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

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

Deferred results

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

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

Selected references

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

15 thms1 active userReviewed

Completed

Quantum Information·Captain: Gohan

Cohomology of Local CochainsResearch Paper

Motivation

We prove that for generalised partitions of unity ${φ_i \mid i \in I}$ and coverings $\mathfrak{U}:={φ_i^{-1} (R \setminus {0}) \mid i \in I}$ of a topological space $X$ the cohomology of abstract $\mathfrak{U}$ -local cochains coincides with the cohomology of continuous $\mathfrak{U}$ -local cochains, provided the coefficients are loop contractible. Furthermore we show that for each locally contractible group $G$ and loop contractible coefficient group $V$ the complex of germs of continuous functions on left-invariant diagonal neighbourhoods computes the Alexander-Spanier and singular cohomology; similar results are obtained for $k$ -groups and for germs of smooth functions on Lie groups $G$ .

This mission is the statement-level formalization of Cohomology of Local Cochains (arXiv:1110.2661v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

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

Deferred results

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

Lemma 1.1: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Proposition 1.2: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 1.3: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 1.4: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 1.5: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 1.6: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, smallSingularCochainComplex, coverRefinementSystem, alexanderSpanierComplex, globalCechCohomology, Actual induced cohomology map, not a freely chosen isomorphism (hard)
Lemma 1.7: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 1.8: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 1.9: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Example 1.10: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Proposition 1.11: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 1.12: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 1.13: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Lemma 1.14: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels (hard)
Example 1.15: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Example 1.16: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Theorem 1.17: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, smallSingularCochainComplex, vertexPullback, leftTranslateCover, identityNeighborhoodColimit, Actual induced cohomology map, not a freely chosen isomorphism (hard)
Corollary 1.18: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, smallSingularCochainComplex, vertexPullback, leftTranslateCover, identityNeighborhoodColimit, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Lemma 2.1: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Remark 2.3: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, generalizedRingPartition, ringPartitionOfUnity, ringNumerableCover, cozeroCover (source-ambiguity)
Proposition 2.4: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 2.6: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Theorem 2.7: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 2.8: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, generalizedRingPartition, ringPartitionOfUnity, ringNumerableCover, cozeroCover, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Corollary 2.9: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 2.10: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Proposition 2.11: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 2.12: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringPartitionOfUnity, ringNumerableCover, uniformEntourageCover, sourceRiemannianGeometry, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Corollary 2.13: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 2.14: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Proposition 2.15: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 2.16: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 2.17: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Lemma 2.18: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels (hard)
Example 2.19: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Example 2.20: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Theorem 2.21: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels (hard)
Corollary 2.22: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels (hard)
Lemma 3.1: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Proposition 3.2: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 3.3: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Theorem 3.4: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 3.5: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, generalizedRingPartition, ringPartitionOfUnity, ringNumerableCover, kCoreflector, kAlgebraicStructures, kContinuousLocalCochainComplex, cozeroCover, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Corollary 3.6: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 3.7: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringPartitionOfUnity, ringNumerableCover, kCoreflector, kAlgebraicStructures, kContinuousLocalCochainComplex, kOmegaSpace, kacMoodyGroupTopology, Actual induced cohomology map, not a freely chosen isomorphism; precise Kac-Moody group/root-data and topology scope relative to the GGH06 Section 6 convention (hard)
Corollary 3.8: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 3.9: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Proposition 3.10: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 3.11: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringPartitionOfUnity, ringNumerableCover, uniformEntourageCover, kCoreflector, kAlgebraicStructures, kContinuousLocalCochainComplex, sourceRiemannianGeometry, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Corollary 3.12: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 3.13: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 3.14: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringPartitionOfUnity, ringNumerableCover, leftTranslateCover, kCoreflector, kAlgebraicStructures, kContinuousLocalCochainComplex, kOmegaSpace, hilbertLieGroup, kacMoodyGroupTopology, Actual induced cohomology map, not a freely chosen isomorphism; precise Kac-Moody group/root-data and topology scope relative to the GGH06 Section 6 convention (hard)
Proposition 3.15: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 3.16: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 3.17: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Lemma 3.18: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels; kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps (hard)
Example 3.19: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Example 3.20: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Theorem 3.21: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels; kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps (hard)
Corollary 3.22: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels; kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps (hard)
Lemma 4.1: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Proposition 4.2: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 4.3: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Theorem 4.4: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 4.5: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 4.6: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, generalizedRingPartition, ringPartitionOfUnity, ringNumerableCover, BGNSmoothCalculus, smoothLocalCochainComplex, cozeroCover, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Corollary 4.7: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 4.8: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Example 4.9: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 4.10: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Proposition 4.11: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 4.12: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Example 4.13: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Lemma 4.14: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Example 4.15: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Example 4.16: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Lemma 4.17: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Lemma 4.18: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Proposition 4.19: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 4.20: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Theorem 4.21: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Example 5.5: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringNumerableCover, loopContraction, realizationStepFunctionModel, semiTopologicalGroup (hard)
Proposition 5.6: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringNumerableCover, loopContraction, continuousSimplexInterpolation (hard)
Lemma 5.7: Recursive simplex interpolation from Eq. (5.1), face-compatible maps and variable-finite-support barycentric row homotopies (hard)
Lemma 5.8: Recursive simplex interpolation from Eq. (5.1), face-compatible maps and variable-finite-support barycentric row homotopies (hard)
Lemma 5.9: Recursive simplex interpolation from Eq. (5.1), face-compatible maps and variable-finite-support barycentric row homotopies (hard)
Proposition 5.10: Recursive simplex interpolation from Eq. (5.1), face-compatible maps and variable-finite-support barycentric row homotopies (hard)
Corollary 5.11: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Theorem 5.12: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 5.13; page-1 abstract main result: cozero-cover comparison: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, generalizedRingPartition, ringNumerableCover, loopContraction, cozeroCover, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Corollary 5.14: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 5.15: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 5.16: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, alexanderSpanierComplex, globalCechCohomology, ringNumerableCover, loopContraction, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Proposition 5.17: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 5.18: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringNumerableCover, uniformEntourageCover, loopContraction, sourceRiemannianGeometry, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Corollary 5.19: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 5.20: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Proposition 5.21: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 5.22: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 5.23: Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Lemma 5.24: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels (hard)
Example 5.25: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Example 5.26: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Theorem 5.27: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels (hard)
Corollary 5.28: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels (hard)
Example 6.2: Based path k-group and evaluation extension for arbitrary group objects in kTop, including kified compact-open maps (hard)
Remark 6.3: Based path k-group and evaluation extension for arbitrary group objects in kTop, including kified compact-open maps (hard)
Example 6.4: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringNumerableCover, kCoreflector, kAlgebraicStructures, kContinuousLocalCochainComplex, loopContraction, realizationStepFunctionModel, semiTopologicalGroup (hard)
Proposition 6.5: Recursive simplex interpolation from Eq. (5.1), face-compatible maps and variable-finite-support barycentric row homotopies; kified products and mapping spaces (hard)
Lemma 6.6: Recursive simplex interpolation from Eq. (5.1), face-compatible maps and variable-finite-support barycentric row homotopies; kified products and mapping spaces (hard)
Lemma 6.7: Recursive simplex interpolation from Eq. (5.1), face-compatible maps and variable-finite-support barycentric row homotopies; kified products and mapping spaces (hard)
Lemma 6.8: Recursive simplex interpolation from Eq. (5.1), face-compatible maps and variable-finite-support barycentric row homotopies; kified products and mapping spaces (hard)
Proposition 6.9: Recursive simplex interpolation from Eq. (5.1), face-compatible maps and variable-finite-support barycentric row homotopies; kified products and mapping spaces (hard)
Corollary 6.10: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Theorem 6.11: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 6.12: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, generalizedRingPartition, ringNumerableCover, kCoreflector, kAlgebraicStructures, kContinuousLocalCochainComplex, loopContraction, cozeroCover, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Corollary 6.13: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 6.14: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, alexanderSpanierComplex, ringNumerableCover, kCoreflector, kAlgebraicStructures, kContinuousLocalCochainComplex, loopContraction, kOmegaSpace, kacMoodyGroupTopology, Actual induced cohomology map, not a freely chosen isomorphism; precise Kac-Moody group/root-data and topology scope relative to the GGH06 Section 6 convention (hard)
Corollary 6.15: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 6.16: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, alexanderSpanierComplex, globalCechCohomology, ringNumerableCover, kCoreflector, kAlgebraicStructures, kContinuousLocalCochainComplex, loopContraction, kOmegaSpace, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Proposition 6.17: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 6.18: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, abstractLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringNumerableCover, uniformEntourageCover, kCoreflector, kAlgebraicStructures, kContinuousLocalCochainComplex, loopContraction, sourceRiemannianGeometry, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Corollary 6.19: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 6.20: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Proposition 6.21: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Corollary 6.22: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Example 6.23: kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps; Alternating fixed-cover Cech/local double complexes, their total complexes, explicit augmentations and induced quotient-cohomology maps (hard)
Lemma 6.24: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels; kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps (hard)
Example 6.25: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Example 6.26: Source-compatible infinite-dimensional Riemannian/Hilbert Lie geometry, geodetic convexity and its local-cohomology comparison maps (hard)
Theorem 6.27: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels; kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps (hard)
Corollary 6.28: Cover-refinement and identity-neighborhood systems, actual induced maps and their colimits, including co-Mittag-Leffler kernels; kTop group/module operations and k-continuous local-cochain complexes with coherent k-product restriction and comparison maps (hard)
Example 7.2: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Example 7.3: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringNumerableCover, BGNSmoothCalculus, smoothLocalCochainComplex, loopContraction, basedPathAndLoopGroup, smoothLoopContraction (hard)
Remark 7.4: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringNumerableCover, BGNSmoothCalculus, smoothLocalCochainComplex, loopContraction, basedPathAndLoopGroup, smoothLoopContraction (hard)
Proposition 7.5: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, ringNumerableCover, BGNSmoothCalculus, smoothLocalCochainComplex, loopContraction, smoothSimplexInterpolation, smoothLoopContraction (source-ambiguity)
Lemma 7.6: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Lemma 7.7: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Proposition 7.8: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 7.9: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Theorem 7.10: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 7.11: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 7.12: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Example 7.13: Full source statement and its source-pinned background/interface: coverDiagonalNeighborhood, abstractLocalCochainComplex, continuousLocalCochainComplex, abstractLocalCohomology, continuousLocalCohomology, alternatingCechComplex, fixedCoverCechCohomology, cechLocalDoubleComplex, cechLocalTotalComplex, rowAugmentation, columnAugmentation, singularCochainComplex, alexanderSpanierComplex, globalCechCohomology, ringNumerableCover, BGNSmoothCalculus, smoothLocalCochainComplex, loopContraction, smoothLoopContraction, Actual induced cohomology map, not a freely chosen isomorphism (source-ambiguity)
Proposition 7.14: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Corollary 7.15: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Theorem 7.16: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Lemma A.3: Full source statement and its source-pinned background/interface: generalizedRingPartition, cozeroCover (source-ambiguity)
Lemma A.4: Full source statement and its source-pinned background/interface: generalizedRingPartition (source-ambiguity)
Lemma A.5: Full source statement and its source-pinned background/interface: generalizedRingPartition, ringNumerableCover, BGNSmoothCalculus, sigmaLocallyFiniteSmoothRefinement, cozeroCover (source-ambiguity)
Proposition A.6: BGN general-ring/infinite-dimensional smooth manifolds and smooth local-cochain complexes with their concrete comparison maps (hard)
Theorem A.7: Full source statement and its source-pinned background/interface: generalizedRingPartition, ringNumerableCover, BGNSmoothCalculus, sigmaLocallyFiniteSmoothRefinement, cozeroCover (source-ambiguity)
Lemma B.11: Full source statement and its source-pinned background/interface: kCoreflector (hard)
Lemma C.7: Full source statement and its source-pinned background/interface: kOmegaSpace, locallyKOmegaSpace (hard)
C.compact-exhaustion: Full source statement and its source-pinned background/interface: kOmegaSpace, locallyKOmegaSpace (source-ambiguity)
background.pseudometric-entourage: Full source statement and its source-pinned background/interface: uniformEntourageCover (source-ambiguity)
background.pseudometric-partition: Full source statement and its source-pinned background/interface: uniformEntourageCover (hard)
intro.classical-comparisons: Full source statement and its source-pinned background/interface: alexanderSpanierComplex, Actual induced cohomology map, not a freely chosen isomorphism (hard)
intro.vanEst: Full source statement and its source-pinned background/interface: alexanderSpanierComplex, leftTranslateCover, Actual induced cohomology map, not a freely chosen isomorphism (hard)

Selected references

Cohomology of Local Cochains, arXiv:1110.2661v2, https://arxiv.org/abs/1110.2661v2

20 thms1 active userReviewed

Quantum Information·Captain: marwahaha

Quantum Max-Cut: $0.595$ energy estimationResearch Paper

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

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

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

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

15 thms1 active userReviewed

Quantum Information·Captain: marwahaha

Quantum Max-Cut: $0.603$ energy estimationResearch Paper

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

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

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

12 thms1 active userReviewed

Campaigns

All missions

Campaigns

All missions

Campaigns

All missions

The Jacobian ConjectureOpen Problem

Beal's ConjectureOpen Problem

OpenSearch cluster coordination: randomized election timersTextbook

The claim

What is proved

What this rests on and what it does not say

OpenSearch cluster coordination: progress under a stable periodTextbook

The claim

The stable periods

What is proved

What this rests on and what it does not say

OpenSearch cluster coordination: safety of the Zen2 consensus protocolTextbook

The claim

The model

What is proved

Findings

What this rests on

OpenSearch cluster coordination: pre-voting and election schedulingTextbook

The claim

The transcription

What is proved

What this rests on and what it does not say

OpenSearch cluster coordination: the per-node consensus state machine (CoordinationState)Textbook

The claim

The transcription

What is proved

Vectors

What this rests on

Simplicial principal bundles in parametrized spacesResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Topological Entanglement Entropy and HolographyResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Local structure of algebraic monoidsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Stochastic processes induced by singular operatorsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Framed bicategories and monoidal fibrationsResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Mapping stacks of topological stacksResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Linear programs for entanglement and key distribution in the quantum internetResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Compactly Generated Stacks: A Cartesian Closed Theory of Topological StacksResearch Paper

Motivation

What is formalized

Deferred results

Selected references

Entanglement Entropy in the O(N) modelResearch Paper

Motivation

What is formalized

Deferred results

Selected references

On the existence of bibundlesResearch Paper

Quantum Max-Cut: $0.595$ energy estimationResearch Paper

Quantum Max-Cut: $0.603$ energy estimationResearch Paper