Final Flyspeck LP family and exact certificates

Let $\mathcal C$ be the fixed catalogue of records $000,\ldots,538$, concatenating the six displayed lists of lengths $81,230,109,127,5,28$. It has $580$ occurrences with repetitions and covers all $539$ numbered records: $488$ have arity $6$, $46$ arity $5$, two arity $1$, one arity $9$, and two arity $10$. Each fixed record $j$ specifies an arity $n_j$, a domain $D_j$ and a conclusion $Q_j$. In this catalogue each domain is the conjunction of its written closed-interval tests, with a bound triple $(a,t,b)$ meaning $a\leq t\leq b$. The proposition $C$ means exactly $\forall j\in\mathcal C\,\forall x\in\mathbb R^{n_j},\ D_j(x)\Rightarrow Q_j(x)$, retaining the fixed formula's strict or weak comparisons, disjunctions and implications. All endpoints and singleton intervals are included; an empty domain makes its implication vacuous. No geometric realizability, triangle inequality, nondegeneracy, sign or nonzero-denominator premise is added to the written domain. Repeated entries impose the same requirement again. Scalar expressions use total real arithmetic, so $a/0=0$, and natural powers, trigonometric functions and their total inverse functions. The custom square root is $\sigma(t)=\sqrt t$ if $t\geq0$ and $-\sqrt{-t}$ otherwise. The custom logarithm chooses a real $z$ satisfying $e^z=t$ when one exists and has no specified logarithm property for $t\leq0$. The custom two-argument angle is $\alpha(x,y)=\arctan(y/x)$ if $|y|<x$, otherwise $\pi/2-\arctan(x/y)$ if $y>0$, otherwise $-\pi/2-\arctan(x/y)$ if $y<0$, and otherwise $\pi$, including $\alpha(0,0)=\pi$. Inverse sine is clamped to $\pm\pi/2$ outside $[-1,1]$, and inverse cosine to $0$ or $\pi$. The constant $h_-$ chooses a real $h$ with $6/5\leq h<13/10$ and $M(h)=L(h)$ if any exists, where $h_0=63/50$, $h_+=6627/5000$, $M(h)=(\sqrt2-h)(h-h_+)(9h^2-17h+3)/(5(\sqrt2-1)(h_+-1))$, and $L(h)=(h_0-h)/(h_0-1)$ for $h\leq h_0$ and $0$ otherwise. Existence and uniqueness of that choice are not fields of the definition. The remaining named scalar helpers are the fixed displayed arithmetic and analytic functions; their names add no geometric assumptions. The ambient space is $\mathbb R^3$ with its Euclidean norm and distance. A set $V$ is a packing exactly when distinct members have distance at least $2$, with no nonemptiness or saturation requirement. Write $B(a,r)=\{x:\|x-a\|<r\}$ and $N_V(a,r)=\#(V\cap B(a,r))$, where this natural-number cardinality is defined as $0$ if the intersection is infinite. Put $w(t)=(63/25-t)/(63/25-2)=(63-25t)/13$, $A=\{x:2\leq\|x\|\leq63/25\}$ and $S(s)=\sum_{v\in s}w(\|v\|)$ for finite sets $s$. Saturation means $\forall x\in\mathbb R^3\,\exists v\in V,\ \|x-v\|<2$; it alone does not require separation. The finite-container condition on $V$ is $\exists c\in\mathbb R\,\forall r\geq1,\ N_V(0,r)\leq\pi r^3/\sqrt{18}+cr^2$. The constant may depend on $V$ and has no sign restriction. A finite hypermap $H$ consists of a natural number $d$, darts $\{0,\ldots,d-1\}$ and permutations $e,n,f$ with $e(n(f(a)))=a$ for every dart. Let $E_a,N_a,F_a$ be its edge, node and face permutation-cycle orbits, including $a$, and let $\mathcal E,\mathcal N,\mathcal F$ be the finite sets of distinct such orbits. Let $\mathcal K$ be the finite set of distinct components reachable by zero or more applications of $e,n,f$. Incident faces at $a$ are the distinct sets $\mathcal I_a=\{F_b:b\in N_a\}$. Write $\mathcal T_a,\mathcal Q_a,\mathcal X_a$ for those incident faces of size $3$, size $4$, and size at least $5$, respectively, and $(p_a,q_a,x_a)=(|\mathcal T_a|,|\mathcal Q_a|,|\mathcal X_a|)$. A face list $L$ is a finite ordered list of finite lists of natural labels. A face $[v_0,\ldots,v_{k-1}]$ supplies the cyclic directed pairs $(v_i,v_{i+1\bmod k})$; an empty face supplies none, and a singleton supplies a loop. The dart list concatenates these lists with multiplicities. Good means no repeated directed pair, every face nonempty, and each occurring $(u,v)$ accompanied by $(v,u)$; it imposes no further length, label-range, connectedness or planarity condition, and the empty list is Good. The list represents $H$ if $e^2=\mathrm{id}$ and there exists a labeling $\ell$ of darts by natural numbers such that $\ell(a)=\ell(b)\Leftrightarrow b\in N_a$, the map $a\mapsto(\ell(a),\ell(f(a)))$ is injective, $(\ell(e(a)),\ell(f(e(a))))=(\ell(f(a)),\ell(a))$, every face of $L$ is a cyclic rotation of $[\ell(a),\ell(f(a)),\ldots,\ell(f^{|F_a|-1}(a))]$ for some dart $a$, and every dart has such a face in $L$. Representation alone permits repeating a face. The opposite hypermap has the same darts and permutations $f\circ n,n^{-1},f^{-1}$. The fixed archive has $19{,}715$ strings; decoding splits at periods into nonempty faces and maps A through O to labels $0$ through $14$. Empty strings, empty faces and other characters fail. Membership means equality to the decoded face list at some in-range index. Archive well-formedness requires successful decoding and Good at every index. For $a,u,v\in\mathbb R^3$ put $P_a(u)=u-\langle u,a\rangle a/\|a\|^2$, using total division, and let $\theta$ be the unoriented Euclidean angle between $P_a(u)$ and $P_a(v)$. Define $Z(a,u,v)=0$ if $a=0$ or either projection is zero; otherwise it is $2\pi-\theta$ when $\det(a,u,v)<0$ and $\theta$ otherwise, including zero determinant with nonzero projections. For a finite set $s$, standard neighbors of a member $v$ are $\{u\in s:u\neq v,\ \|u-v\|\leq63/25\}$, and contact neighbors are $\{u\in s:u\neq v,\ \|u-v\|=2\}$; a point outside $s$ has no neighbors. For either relation, the successor of $w$ around $v$ is $w$ if the neighbor set is exactly $\{w\}$; otherwise it is a chosen neighbor $u\neq w$ minimizing $Z(v,w,u)$ among neighbors other than $w$. If no such neighbor exists the choice has no specified property; minimizers need not be unique. The dart angle is $Z(v,w,\operatorname{successor}(v,w))$ when $v$ has more than one neighbor and $2\pi$ otherwise. Being surrounded means that membership in $s$ implies a nonempty neighbor set and a dart angle strictly less than $\pi$ at every neighbor. Outside $s$ this implication is vacuous. A contravening configuration is a finite set $s$ of pairwise separated points in the closed annulus $2\leq\|v\|\leq63/25$, with score $S(s)=\sum_{v\in s}(63-25\|v\|)/13>12$, and with score at least that of every finite packing in that annulus, without restricting competitors' cardinality. It must also have $13$, $14$ or $15$ members; every member must be surrounded for standard neighbors; and every member must either be surrounded for contact neighbors or have norm exactly $2$. A placement of $H$ is any map $p$ from darts into $\mathbb R^3$, with center set $s_p=\{p(a):a\text{ a dart}\}$, counting distinct images once. It realizes the standard fan when $p(a)=p(b)\Leftrightarrow b\in N_a$, each $p(e(a))$ is a standard neighbor of $p(a)$, every ordered standard-neighbor pair $(v,w)$ in $s_p$ comes from exactly one dart $a$ with $p(a)=v,p(e(a))=w$, $p(e(e(a)))=p(a)$, and $p(e(n(a)))$ equals the chosen standard successor of $p(e(a))$ around $p(a)$. A contravening realization is a standard-fan realization whose center set is a contravening configuration; it does not additionally assume tameness or an involutive edge permutation on darts. For $L,H,p$, the position map $q:\mathbb N\to\mathbb R^3$ is chosen as follows. If $L$ represents $H$, choose a witnessing labeling and return $p(a)$ for the first dart, in the order $0,\ldots,d-1$, with label $v$, or $0$ if the label is missing. If this representation fails but $L$ represents the opposite, choose a labeling for the opposite and negate the first Cartesian coordinate of the same first-dart lookup in $p$. If neither representation holds return $0$ for every label. The direct representation takes priority if both hold. These are fixed choices, not universal quantification over all representing labelings. For a face list $L'$ and pair $a=(u,v)$, take the pair-list of the first face containing $a$, defaulting to the empty list. Let $a^+,a^-$ be its next and previous pairs at the first occurrence of $a$, defaulting to $a$ if lookup fails, and let $a^{--}=(a^-)^-$. Put $z_a=Z(q(u),q(v),q((a^-)_1))$, $s_0=3\arccos(1/3)-\pi$, $\lambda(t)=(63-25t)/13$ for $t\leq63/25$ and $0$ otherwise, and $R_v=1+(s_0/\pi)(1-\lambda(\|q(v)\|))$. Node variables yn, ln, rho evaluate to $\|q(v)\|,\lambda(\|q(v)\|),|R_v|$. Dart variables azim, azim2, azim3 evaluate to $z_a,z_{a^+},z_{a^-}$; rhazim, rhazim2, rhazim3 evaluate to $|R_{a_1}|z_a,|R_{(a^+)_1}|z_{a^+},|R_{(a^-)_1}|z_{a^-}$. Dart variables ye and y6 both give $\|q(u)-q(v)\|$; y1,y2,y3 give $\|q(u)\|,\|q(v)\|,\|q((a^-)_1)\|$; y4 and y9 both give the length of $a^+$; y5 gives the length of $a^-$; y7 gives $\|q((a^{--})_1)\|$; y8 gives the length of $a^{--}$; and y4prime gives $\|q(v)-q((a^-)_1)\|$. For a pair-list $F$, its face sol variable is $|\sum_{a\in F}(z_a-\pi)+2\pi|$, and its tau variable is $|\sum_{a\in F}z_aR_{a_1}+(\pi+s_0)(2-|F|)|$, counting list multiplicities. A node address is valid if its label occurs in $L'$. For dart kinds ye,y1,y2,y6, both endpoint labels must occur but the pair need not; all other dart kinds require the pair itself in the dart list. A face address must equal an occurring face's pair-list exactly, not just up to rotation. A finite case tree is a leaf or a branch with an indexed child family. Its branch guards use $r_v=\|q(v)\|$ and $l_{uv}=\|q(u)-q(v)\|$. Rule 218 has children guarded by $109/50\leq r_v$ and $r_v\leq109/50$; rule 236 by $r_v\leq59/25$ and $59/25\leq r_v$; an edge rule by $9/4\leq l_{uv}$ and $l_{uv}\leq9/4$; a triangle rule by its perimeter being at least or at most $25/4$. For a quadrilateral set $a=l_{v_0v_2},b=l_{v_1v_3},t=\sqrt8$; its five guards are $a\leq b\land a\leq t$, $b\leq a\land b\leq t$, $a\leq b\land t\leq a\leq3$, $b\leq a\land t\leq b\leq3$, and $3\leq a\land3\leq b$. For a pentagon set $(a,b,c,d,e)=(l_{v_0v_2},l_{v_1v_3},l_{v_2v_4},l_{v_3v_0},l_{v_4v_1})$; its eleven guards are: all five at least $t$; $a\leq t\leq c,d$; $b\leq t\leq d,e$; $c\leq t\leq e,a$; $d\leq t\leq a,b$; $e\leq t\leq b,c$; $a,c\leq t$; $b,d\leq t$; $c,e\leq t$; $d,a\leq t$; and $e,b\leq t$. For a hexagon the six lengths are $l_{v_0v_2},l_{v_1v_3},l_{v_2v_4},l_{v_3v_5},l_{v_4v_0},l_{v_5v_1}$; its seven guards are all six at least $t$, followed by each individual length at most $t$. Rules high, mid and add_big each have one child with guard true. Reaching a leaf means a root-to-leaf path satisfying every guard; syntactic leaf membership ignores guards. Weak inequalities allow overlap at boundaries. The LP data are fixed tables of $19{,}715$ graph records, $43{,}078$ graph-indexed leaf records, $216$ selectable row names, and $1{,}525$ integer row templates at precisions $3$ through $7$. Graph identifier strings are not consulted. Tree decoding consumes space-separated tags l, 218, 236, edge, tri, quad, pent, hex, high, mid and add_big, their exact numbers of natural labels, and their prescribed numbers of children; malformed tokens, exhausted token-count fuel and leftovers fail. A tree starts with state $(L,\mathrm{true})$. Splitting a face at a pair finds the first containing face, rotates it so that the predecessor of the pair's initial label is first, then replaces a face longer than $3$ by its first three labels and by its first label followed by its labels from position $2$ onward. A shorter face is only rotated; no containing face leaves the list unchanged. Refinement marks the state false even if unchanged. Quad children $0,2$ refine at $(v_1,v_2)$, children $1,3$ at $(v_0,v_1)$, and child $4$ keeps the state. For pentagon and hexagon rules rotate their cyclic dart list once. Pentagon child $0$ keeps the state; children $1,\ldots,5$ refine at entries $0,\ldots,4$; children $6,\ldots,10$ split successively at those entries and the entries two positions later cyclically. Hexagon child $0$ keeps the state and children $1,\ldots,6$ refine at entries $0,\ldots,5$. Other rules leave the state unchanged. Leaves carry a natural ordinal and the accumulated state. A leaf code begins with a precision digit 3–7 and mode I or B, followed by vertical-bar-separated selections. Each selection starts with character code $256+k$ for an in-range name index, followed by i and indices encoded by characters # through p excluding backslash, giving $0,\ldots,76$, or by b and a base-64 bit mask in alphabet A–Z,a–z,0–9,-,_, with its first digit least significant. Only masks below $2^{77}$ pass; their set bits give indices. The stored graph index must equal the requested index. Template lookup selects the first matching name and precision, preferring a true standard-only flag in a true state and falling back to false; a false state only permits false. Index pools are distinct labels, all darts, all faces' dart lists, outgoing-dart lists for each distinct label, or darts of faces of a specified size. Distinct labels retain the order of last occurrences by right-to-left duplicate removal. Addresses select bound objects, all labels, next/previous/reversed darts, initial nodes, first darts or containing faces; feature constructors produce one coordinate or sum coordinates on a node/dart list. Type mismatches, empty required lookups and out-of-range pool indices fail. Each integer coefficient is copied to its instantiated terms, with no additional precision scaling. Selected row groups are concatenated. Mode I uses only them; mode B appends the false-flag main template at pool index $0$. Columns are the distinct syntactic variable addresses; a matrix entry sums every coefficient for that column in its row, and the right-hand side is the rational row constant. Compilation itself checks neither geometric validity nor nonempty rows, guards, feasibility or certificates. The archive obligation is a conjunction of three claims. First, the graph-table size is $19{,}715$, the leaf-table size $43{,}078$, and the graph-table size equals the decoded-archive size; for every archive index $i$ there are a successfully decoded list $L$ and successfully decoded state-labeled tree built from graph index $i$ and $L$, and every syntactic leaf location has a successfully compiled program with strictly positive row count and every column address valid in that location's face list. Second, for every index $i$, every list $L$ and tree satisfying those decoding equalities, every hypermap $H$ and placement $p$ with $L$ representing $H$ or its opposite and $(H,p)$ a contravening realization, and every location and successfully compiled program there, reaching that location under the radii and distances of the chosen map $q$ implies every row inequality $\sum_j A_{kj}x_j\leq b_k$ at the program's geometric column values, evaluated on that location's face list. Third, for every index, decoded list, decoded tree, syntactic leaf location and successfully compiled program there, a rational vector $y$ indexed by its rows exists such that $y_k\geq0$, $\sum_k y_kA_{kj}=0$ for each column, and $\sum_k y_kb_k<0$. The third claim includes geometrically unreachable leaves. It provides existential certificates rather than a displayed list of certificate vectors. The geometric implication can be vacuous in the absence of a contravening realization or guarded path, while successful compilation and certificates remain required at every syntactic leaf. The theorem asserts that $C$ implies this full three-part archive obligation. It assumes neither archive classification nor tameness as a separate premise for its geometric soundness quantifiers. It does not display certificate vectors or assert that the Boolean checker has been run; rational certificate existence at every syntactic leaf is part of the mathematical conclusion.