The upper oriented general position number: first values and extremal graphs

The bridge: G[S] is a comparability graph iff some ordering of S passes the triple loop

Headline: mu(n), the least ugp over all graphs of order n, equals 4, 4, 5, 5 at n = 4, 5, 6, 7

43 exact values of ugp for named graphs, including ugp(Petersen) = 7; the complete/path/even-cycle ones restate the source, the rest are new

Negative controls: each clause of the definition is load-bearing, and the values are sharp in both directions

Validation: OEIS A123416 reproduced at n = 4..8, extending the scouting pass by one term

Frontier closed: mu(8) = 6, now a Lean theorem

Golumbic Gamma-forcing soundness kernel-clean; ugp(Kneser(6,2)) = 9 and ugp(co-Cₙ) = n-1 through n = 16 (past the factorial wall)

Acceptance lemma: a bipartite induced subgraph is a comparability graph

Acceptance lemmas: bipartite/blocks/rank routes to comparability (three lemmas)

mu(n) for n = 4..8 as one statement

Gallai's theorem: an implication class that does not meet its own reverse is a transitive relation

The gluing step: a consistent class together with *any* transitive orientation of what is left after deleting it is a transitive orientation of the whole graph

The TRO theorem: if the greedy Γ-decomposition runs to completion with every class consistent, the graph is a comparability graph

A polynomial, certified acceptance test for comparability

ugp(Petersen) = 7 and ugp(Kneser(6,2)) = 9 with both halves polynomial and no hand-supplied witness

Golumbic's (ii) ⟹ (iii) — that consistency survives deleting an implication class — is not proved, and is exhaustively true at orders 5 and 6

Negative controls, including that Γ is not itself transitive

ugp(Kneser(7,2)) = 12 — the family's named next step, both halves proved

The same value with no hand-supplied witness: compFind searches, troCert re-checks

Hereditary pruning, proved sound: a refuted subset kills every superset

The pruning measured: 30 026 nodes against 203 490 flat calls, mean order 8.00 not 13

The 21 row bitmasks really are Kneser(7,2)

Negative controls, including that the pruned search refuses to refute a comparability graph

ugp(Petersen) = 7 and ugp(Kneser(6,2)) = 9 re-proved through the pruned search

μ(9) = 6 — the least ugp over all graphs on 9 vertices

μ(10) = 6, refuting ⌊n/2⌋ + 2

ugp is monotone under induced subgraphs, and μ(n) ≤ μ(n+1) ≤ μ(n) + 1

μ(N) ≥ 6 at every order N ≥ 8 from the landed μ(8) chunks alone, and the source's own Corollary 4.7 at every order from one 64-graph sweep

Two of the four MinAll.lean sweeps are redundant: μ(4…9) needs sweeps at three orders, not five

Negative controls for the transfer lemma and the ninth value

μ(2) = 2, μ(3) = 3, and the whole table n = 2 … 10 as one statement

μ(11) = 7, and 10 is the largest order with μ(n) = 6 — the family's own extremal question, answered

No eleventh vertex can be added to either order-10 minimiser: all 2·2¹0 extensions have ugp ≥ 7

The triangular graph T(5) = L(K₅) = complement of the Petersen graph is one of exactly two extremal graphs at order 10

The prefix-pruned sweep: μ(n) ≥ m proved without enumerating the graphs of order n, with the pruning proved sound

μ(8) ≥ 6 from 415 564 partial matrices instead of 2²8 graphs: one native axiom against sixteen chunks, and no dylib

Negative controls for the sweep and its pruning test

The Lean route to the classification, priced in three variants

μ(11) = 7 — unconditional; the family's own extremal question max N: μ(N) = 6 = 10, answered by a Lean theorem

Exactly two graphs of order 10 have ugp ≤ 6: minAttaining10 and triangular5 = L(K₅) = complement of Petersen

The sound lex-max prune: isomorph rejection with an untrusted search, and no verified canonical form

The gate: the same route reproduces A000088 at orders 2–4 and the landed ladder 220, 226, 30, 2 at orders 7–10

μ(N) ≥ 7 for every N ≥ 11, and the next frontier μ(12) ∈ 7, 8

Negative controls for the prune, the allowed list and the value

μ(12) = 7 — the frontier ugp-frontier-12 left open, closed on the lower end of its 7,8 bracket

μ(N) = 7 for every 11 ≤ N ≤ 15, from one graph: T(6) = L(K₆)

The minimisers are line graphs: L(K₂,₃), L(K₂,₄), L(K₃,₃), L(K₅), L(K₃,₄), L(K₆) at orders 6, 8, 9, 10, 12, 15

The new frontier μ(16) ∈ 7,8, with its upper half attained by a connected 6-regular graph

Negative controls for the value, the search and the pattern

At least two isomorphism classes attain μ(12) = 7: K₃ □ K₄ and the circulant C₁₂(1,4,5,6)

No sixteenth vertex that avoids four named pairs extends T(6) = L(K₆) — 2 048 of the 32 768 order-16 extensions of the order-15 minimiser have ugp ≥ 8, with the transport in place for the other 30 720

Controls for the sweep: it returns false where an extension exists, false at a larger budget, and does not fire at its root

T(6) is an isolated order-15 minimiser — no ugp ≤ 7 graph within two edge flips — and no graph in the scanned transitive families (all order-15 Cayley graphs, all abelian order-16 Cayley graphs, named line/Kneser graphs and SRG deletions) matches it — external, not Lean

No sixteenth vertex extends T(6) = L(K₆) while keeping ugp ≤ 7 — all 32 768 extensions of the order-15 minimiser, unconditional, and μ(16) = 8 now follows from the order-15 classification alone

The order-backtracking search and its soundness: a comparability m-set is a linear order passing a prefix-closed triple loop, so a DFS with a re-checked rank certificate replaces subset enumeration at every order

Controls for the new route: it is calibrated against two landed values by a different algorithm, refuses a larger budget, refuses at the root, returns false where an extension exists — and hlow finally has its non-vacuity control and its graph-terms reading

The 2.9 CPU-hour price was a property of troSearchLast, not of the problem — but the speed-up is a function of the order, and the (8, 16) classification stays parked at ≥ 38 CPU-hours for level 10 alone