we-solve (beta)

Math-2882 · mathematics · Probability

One root-independent IID factor for all free uniform spanning forests

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
Is there a single Borel rule, equivariant under graph isomorphisms and independent of a distinguished root, which takes iid uniform vertex labels on every infinite connected locally finite simple unweighted graph to an edge set with that graph’s free uniform spanning forest law?

Short English statement

Is there a single Borel rule, equivariant under graph isomorphisms and independent of a distinguished root, which takes iid uniform vertex labels on every infinite connected locally finite simple unweighted graph to an edge set with that graph’s free uniform spanning forest law?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2882-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2882

The free spanning forest on every infinite locally finite simple graph is claimed obtainable by one root-free Borel rule from iid labels; invariant strongly Rayleigh processes have an analogous group-equivariant construction. The question retains these same parameters and conventions. Within these assumptions, this is a claimed affirmative answer to the stated question.

One root-independent IID factor for all free uniform spanning forests

OpenAI's claim

OpenAI presents a proof in the selected manuscript. The free spanning forest on every infinite locally finite simple graph is claimed obtainable by one root-free Borel rule from iid labels; invariant strongly Rayleigh processes have an analogous group-equivariant construction.

Mathematical statement of the claimed result

Result 1.
One Borel root-independent rule $\Phi(G,U,e)\in\{0,1\}$ is claimed to work for every infinite graph that is connected, has finite degrees, and is simple, undirected and unweighted. With independent uniform vertex labels, its selected edge set \[ \{e:\Phi(G,U,e)=1\} \] has the free uniform spanning-forest law and the rule commutes with graph isomorphisms. The second theorem takes any countable group $\Gamma$ and any translation-invariant strongly Rayleigh law $\nu$ on $\{0,1\}^\Gamma$. It supplies a Borel map $\Phi_\nu:[0,1]^\Gamma\to\{0,1\}^\Gamma$, equivariant at every input, whose iid-uniform input has output law $\nu$.

Outline of the argument

Finite determinant tilts define a canonical response drift for the free forest law. Brownian observations provide independent innovations, and a deterministic inverse reconstructs the sampler; vertex labels are converted to independent edge paths in a measurable rule that also applies to varying graphs.

Formal verification

For family 231, the Lean scope includes a root-free iid rule for free spanning forests and invariant strongly Rayleigh and determinantal sampling supplements without amenability assumptions. The listed Comparator files are FreeUniformSpanningForest.lean, StronglyRayleighDPP.lean. The inventory does not supply a named declaration for these Comparator entries. This site has not executed the Lean code. The scope descriptions do not certify the remaining manuscript arguments.

Status caveat

OpenAI attributes these manuscripts to work by an internal model. Its release cautions that arguments without formalization can contain mistakes. This catalogue has not independently checked the proofs; the labels report the mathematical claims attributed to OpenAI.

Sources

Go to contribution →