The Two-Pin Wall Reduction

Theorem R · proofs/two-pin-wall-reduction.md · a-tangency board, wall-local-obstruction-lemma.md §7 · ARGUED — natural-language proof, no Lean · firewalled adversarial cold review CONFIRMED (stands-with-errata), 2026-07-23

A circle arrangement crosses from one combinatorial type into a neighboring one at a contact point $V^*$ — a point where some pair of circles' relation value touches the boundary between two classes. proofs/wall-local-obstruction-lemma.md builds the local theory of a single such crossing, a single pin, into a short trichotomy for its excess function $\varepsilon$: escape at first order if $d\varepsilon(V^*) \neq 0$, escape at second order if the Hessian has a positive direction transverse to the contact locus, and obstruction — genuine non-realizability — if that Hessian is negative definite there. The obstruction case is a real certificate, and it works because the excess is forced to be critical along its own zero set: second-order data alone decides it.

Most of the measured n=5 hard residue does not sit at a single pin, though. At a two-pin contact point, two excesses $\varepsilon_1, \varepsilon_2$ touch zero together, and the measured population — all four of the hardest two-pin classes — sits at what proofs/wall-local-obstruction-lemma.md §7 calls a flat cone: every second-order joint quantity the single-pin toolkit can compute is zero to machine precision. Neither escape nor obstruction fires; the trichotomy has nothing to say. The diagnosis given there is that the individual gradients $d\varepsilon_i$ do not vanish along the joint contact locus $Z_{\mathrm{all}}$ — only a balanced combination does — so the single-pin proof's key move, criticality forced along the whole zero set, has no direct analogue.

Theorem R says the diagnosis was half right. A gradient that refuses to vanish is not a dead end — it is exactly the coordinate the reduction needs. At a balanced two-pin point with both reduced gradients nonzero and opposing (the generic case, and the one every measured two-pin n=5 point sits in), eliminate one pin by using its nonvanishing gradient to straighten a chart; what remains is a single scalar function on the resulting wall, and the two-pin problem becomes the already-solved single-pin problem, one order deeper. The reduction is an equivalence, not merely a sufficient direction, and it needs no extra smoothness hypothesis: the wall is automatically smooth because the eliminated gradient is nonzero.

Two pins, one balance point

Write $g_1, g_2$ for the reduced gradients of the two excesses at $V^*$ on the tangent space of the reduced manifold, and let $B$ be the balance polytope — the convex combinations that cancel. The two-pin case splits exhaustively into four:

• b0, no balance ($0 \notin \operatorname{conv}\{g_1, g_2\}$): first-order escape already fires; realizable, and not this essay's concern.
• b1, both critical ($g_1 = g_2 = 0$): the balance polytope is the whole simplex. Untouched below — see the fences.
• b2, one critical ($\text{exactly one } g_i = 0$): partially covered — see the fences.
• b3, both nonzero, balanced: forces the two gradients into exact opposition, $g_2 = -\lambda g_1,\ \lambda > 0$, with $B = \{\mu^*\}$ a single interior point. This is the generic balanced case, and measurement (the four hardest two-pin n=5 contact points, all independently re-verified for this essay) shows it is the only case that occurs there: every one has an interior balance point, e.g. $(0.065, 0.935)$, $(0.191, 0.809)$, $(0.063, 0.937)$, $(0.451, 0.549)$. Theorem R addresses exactly this case.

Theorem R: the gradient as fuel, not obstacle

Theorem R. Let $V^*$ be a clean two-pin contact point with $d\varepsilon_1(V^*) \neq 0$ and $d\varepsilon_2(V^*) = -\lambda\, d\varepsilon_1(V^*)$ for some $\lambda > 0$. Let $Z_1 = \varepsilon_1^{-1}(0)$ near $V^*$ and $\beta := \varepsilon_2|_{Z_1}$. Then $d\beta(V^*) = 0$, and

In particular, $\beta \le 0$ on a $Z_1$-neighborhood of $V^*$ is a certificate-grade open-neighborhood non-realizability exclusion, of exactly the same evidentiary shape as a single-pin obstruction.

The proof is elementary and needs nothing exotic. Since $d\varepsilon_1(V^*) \neq 0$, $\varepsilon_1$ is a submersion at $V^*$; straighten a chart $(t,y) \in \mathbb{R}\times\mathbb{R}^{m-1}$ with $\varepsilon_1 = t$. Hadamard's lemma then writes $\varepsilon_2(t,y) = \beta(y) + t\,g(t,y)$, and evaluating the hypothesis $g(0,0) = \partial_t\varepsilon_2(0,0)$ at the base point gives $g(0,0) = -\lambda < 0$ — strictly negative, hence of one fixed sign on a whole neighborhood by continuity. That one fact is the entire engine: it lets a curve $t \mapsto (t, y(t))$ trade $\varepsilon_1$ against $\varepsilon_2$ in either direction, giving both halves of the iff by the same short computation. Nothing about the joint locus $Z_{\mathrm{all}}$ (which is $\beta^{-1}(0)$ inside $Z_1$ and may itself be singular) had to be assumed smooth, and no definiteness or aggregate choice entered anywhere — the earlier diagnosis was right that the vector-valued map has no forced joint criticality, and wrong only in reading that as a dead end rather than as fuel for elimination.

Symmetry. The two pins can be swapped — eliminate $p_2$ and restrict $\varepsilon_1$ to $Z_2$ instead — and both reductions must agree. This is a free consistency check, exercised on two of the four measured classes below.

The normal form

Reparametrizing $t$ by a positive unit turns the chart into an exact orthant picture:

So the germ of $\beta$ on $Z_1$ — up to diffeomorphisms of $Z_1$ fixing $V^*$ and multiplication by positive units, both of which preserve the sign locus — carries all the local feasibility information Theorem R proves is decisive. This answers, for $r=2$ in case b3, the normal-form demand docs/research/tangency-chambers-walls-strata.md §8 makes for the orthant map and proofs/wall-local-obstruction-lemma.md §7 names as missing — but only there: whether $\beta$ is a complete invariant of the pair, one step stronger than what Theorem R needs, is plausible but unproved and explicitly out of scope.

The ladder: third and fourth order

Everything past this point is the single-pin toolkit applied to the scalar $\beta$ on $Z_1$, plus one splitting lemma. $d\beta(V^*)=0$, so its intrinsic Hessian $H_\beta$ on $T_{V^*}Z_1$ is well defined.

Second order (recovering what existed, and unlocking what didn't). If $H_\beta(w,w) > 0$ for some direction, the class is realizable — this recovers the multi-pin joint-escape theorem of the proofs document exactly, one level down. The obstruction direction is genuinely new: if $H_\beta$ is negative definite transverse to $Z' := \beta^{-1}(0)\cap Z_1$, the class is obstructed. That instrument was unavailable before the reduction: the un-restricted proofs document needs a single aggregate excess transversally definite on the whole reduced tangent space, and the measured points show that aggregate is indefinite everywhere on it (a positive direction always survives on the full space). Restricting to the wall first is precisely what discards that positive direction.

Lemma FM (the fiberwise-max cascade). When $H_\beta \preceq 0$ with negative block $E$ and kernel $N$, each fiber of $N$ is strictly concave in the $E$-directions, so the implicit function theorem gives a smooth fiber-critical section $\varphi(n)$; the reduced function $\tilde\beta(n) := \beta(\varphi(n), n)$ inherits $\beta \le \tilde\beta\circ\pi$ with equality on the graph of $\varphi$, so $\{\beta>0\}$ accumulates at $V^*$ exactly when $\{\tilde\beta>0\}$ does — and $\tilde\beta$ has a zero second-order jet on $N$, ready for the next rung. (The idea rhymes with the Gromoll–Meyer splitting lemma; that name is context only, not a citation this essay leans on.)

Third order, new. If $j^2\tilde\beta = 0$ and the cubic form $C = j^3\tilde\beta$ is not identically zero on $N$, pick $w$ with $C(w) > 0$ (a cubic is odd, so a sign is always available): $\tilde\beta(sw) = C(w)s^3 + O(s^4) > 0$ for small $s>0$, hence realizable. No second-order instrument sees this.

Fourth order, new. If the cubic vanishes and the quartic form $Q_4 = j^4\tilde\beta$ is negative definite on $N$, then $\tilde\beta(n) \le -c|n|^4 + O(|n|^5) < 0$ near $0$, so the class is obstructed — a genuinely fourth-order two-pin obstruction certificate.

Two micro-examples, both invisible to any second-order test. On $\mathbb{R}^2$:

is flat-cone ($H_\beta = 0$, so the second-order tests are silent); $\beta = y^3$ takes positive values, hence realizable — directly, $t = y^3/2$ for $y>0$. And

is also flat-cone; $\beta = -y^4 \le 0$, hence obstructed — directly, $\varepsilon_2>0$ forces $t < -y^4 \le 0$. Both verdicts are immediate from the ladder and invisible one rung down.

The measured wall Hessian

Appendix A of proofs/two-pin-wall-reduction.md runs the reduction against all four hardest two-pin n=5 contact points (60-digit-polished, from the relay-20 Lane F campaign); this essay re-ran that script independently (scratch/relay21-lane4b/beta_probe.py, verbatim from the Appendix) and confirms every published number. At every point and both pin choices where checked: $\beta \text{ is critical}$ to a relative residual no worse than $3\times 10^{-22}$; the wall Hessian has exactly the single-pin obstruction shape — no positive direction, a kernel, and exactly one strictly negative direction; the fitted cubic on every checked kernel direction is zero at the resolution of an h²-halving check (a pure quintic-contamination signature); every fitted quartic coefficient on every checked kernel direction is strictly negative; and a direct numeric probe (dozens of directions, four radii, hundreds of accepted points per class) finds no positive $\beta$ anywhere near any of the four points.

Read plainly, this says: at measurement precision, the reduction's verdict for all four classes is non-realizable, decided (numerically, not certified) at fourth order. But two things keep this from being a decision of record. First, it is one contact point per class, found by a stochastic solver, with no claim that every point of the same class behaves identically. Second — the sharper honesty point — Corollary L4 as proved needs the quartic negative definite on the whole kernel $N$; what is measured is a kernel strictly larger than a transverse complement to $Z'$ (the moduli of $Z'$ itself sits inside it, mixed into the generic eigendirections), so L4's hypothesis does not literally hold. The ladder proved here does not decide these four classes. What would is the graded, parametrized obstruction theorem named next — and that theorem is open.

The honest fences

• Case b1 (both reduced gradients critical) is untouched. There is no coordinate to eliminate; the balance polytope is the whole simplex, and deciding whether $\{\varepsilon_1>0,\ \varepsilon_2>0\}$ accumulates at the contact point needs hypotheses on the pair of intrinsic Hessians (and higher jets) at a common critical point — a genuine question this document does not touch. No point of the measured n=5 population lands there today, but any future contact point that does inherits this open b1 wall as-is.
• Case b2 (one reduced gradient zero) survives only one way. The escape direction transfers by the same curve argument. The obstruction direction fails: in the straightened chart, $\varepsilon_2 = -|y|^2+t^2$ has $\beta=-|y|^2\le 0$ on the wall, yet $F=\{t>|y|\}\neq\varnothing$ — an escape invisible on the wall alone. (This is also the referee's proof that Theorem R's opposing-gradient hypothesis is load-bearing, not decorative: it is exactly what fails here.)
• r ≥ 3 pins survive only partially. A one-way escape criterion holds at any $r$ (all reduced excesses positive on the wall ⇒ realizable, at all orders), and the full iff transfers verbatim in the special case where every pin opposes the eliminated one. The general converse, with mixed helping and opposing pins, is open — the genuinely vectorial character of the problem survives exactly there, because balance in the two-pin case forces pure opposition and nothing forces it once $r\ge 3$.
• The graded, parametrized obstruction theorem is open. This is the single theorem standing between the reduction and an actual decision at the measured points: a quartic negative-definite transverse to a positive-dimensional $Z'$, uniformly along it — a “quartic tube lemma,” scalar and standard-shaped but genuinely new. Nothing in this document proves it.
• Exactification is untouched. Every number above is MEASURED-numeric (one contact point per class, tolerance calls on eigenvalue signs); turning any of it into a certificate needs an exact algebraic contact point and a local Positivstellensatz for $\beta\le 0$ on the wall, in the shape of the n=4 case-3 exactification the proofs document already has as a template. Not attempted here.
• The global assembly corollary is untouched. Deciding any class of record, even after a local exactification, still needs the unproved paving corollary of docs/research/tangency-chambers-walls-strata.md §8 — orthogonal to everything in this essay and unmoved by it.

Grade, stated plainly: ARGUED — a refereed natural-language proof, strictly sub-PROVED. No Lean, no kernel check. A solo first draft was lifted to ARGUED by an independent firewalled adversarial cold review that re-derived Theorem R, the normal form, Lemma FM, and Corollaries L1–L4 from their bare statements before reading the argument, and confirmed both directions of the iff, the exhaustiveness of the b0/b1/b2/b3 split, and the b2 counterexample; the verdict was stands-with-errata, the errata cosmetic prose fixes, applied. Everything here lives on the a-tangency board (docs/research/tangency-chambers-walls-strata.md's relation-labelings), never the a(6) board: it decides no class of record, the n=5 a-tangency UNKNOWN residue is unchanged at 355 iso-classes, and it moves no a(6) quantity and no bracket — the bracket of record is docs/a6-bracket.md, untouched here and unreferenced by any number above.