Logical Phase Transitions for Graph-Minor Principles

Definitions and mathematical statement

Fix the source's size, logarithm and parameter conventions, and set $f_r(i)=r\sqrt{\log i}$ for $i\geq1$. The finite graph-minor principle intended by "every sufficiently long sequence" has the quantifier pattern \[ \forall K\in{\mathbb{N}}\ \exists N\in{\mathbb{N}}\ \forall(G_1,\ldots,G_N):\quad \left[\forall i\in\{1,\ldots,N\},\ |G_i|<K+f_r(i)\right] \Longrightarrow \left[\exists i<j\leq N:\ G_i\preccurlyeq_{\mathrm{minor}}G_j\right]. \] The graphs are finite simple graphs. Minor containment permits vertex/edge deletion and edge contraction, with the simple-graph convention after contraction; it is not induced-subgraph containment. The length $N$ may depend on $K,r$ but must work for every controlled sequence. The usual interpretation of $|G|$ is number of vertices, but the source does not explicitly define its graph norm, and that choice matters for an exact threshold.

Writing this arithmetical assertion as $\mathrm{GM}_{f_r}$, the proposed phase transition is \[ r\leq2:\quad I\Delta_0+\exp\ \vdash\ \mathrm{GM}_{f_r}, \qquad r>2:\quad \mathrm{PA}\ \nvdash\ \mathrm{GM}_{f_r}. \] Here $I\Delta_0+\exp$ denotes bounded-induction arithmetic with total exponentiation, and PA is first-order Peano arithmetic. The endpoint $r=2$ is included on the provable side. Unprovability is a proof-theoretic assertion about the chosen formal sentence, not a claim that the finite combinatorial principle is false.

The coefficient domain/coding is omitted: the relevant usual regime is a fixed nonnegative effectively specified parameter, often rational, but the source does not state that restriction. An arbitrary real $r$ need not name a first-order arithmetical function. The base of $\log$, graph-size norm, rounding/strict-inequality implementation and sequence encoding must also be fixed before the number $2$ has the claimed exact meaning. Changing logarithm base rescales this coefficient threshold; none of these choices is silently normalized or corrected.

The literature triage checked 21 August 2026 reports no authoritative complete resolution of the extracted phase claim. It supplies no precise arithmetization or threshold theorem reference beyond the report; its dated open assessment is not independently verified here.

Short English statement

The source predicts a sharp proof-theoretic threshold at $r=2$ for finite graph-minor sequences controlled by $K+r\sqrt{\log i}$. The sequence bound is uniform over graphs for each $K$. Exact logarithm, graph-size and parameter-encoding conventions are essential to that numerical threshold.

Sources

• Local UnsolvedMath registry, permanent ID 30000615, exact source code catalogue entry; Logical Phase Transitions for Graph-Minor Principles. Proposed year 2006, status open; corrected_verified extraction retains both logical theories and the two parameter ranges.
• Supplied report citation: Mini-workshop: Logic, Combinatorics and Independence Results (2007), Oberwolfach Reports, DOI 10.4171/owr/2006/52, pp. 3087--3130, https://doi.org/10.4171/owr/2006/52. Title year differs from DOI/proposed year.
• Supplied literature triage checked 2026-08-21 cites the same report, https://doi.org/10.4171/owr/2006/52, and reports no authoritative complete resolution found. The dated OWR-derived curation requests independent verification of time-sensitive status and cited claims; no separate threshold-theorem reference is supplied.