CLAIMS_LEDGER.md

Claims ledger

Claim	Status	Exact assumptions	Evidence	Independent verification	Source	Remaining gap
The displayed three-variable map has determinant -2.	VERIFIED_EXACT_COMPUTATION	Polynomial ring Q[x,y,z]; displayed coefficients exactly as announced.	results/sympy_verification.json	results/independent_verification.json uses a separate sparse implementation.	Public formula recorded by Zhang, 2026.	None for the identity; publication review is separate.
The three displayed rational points share image (-1/4,0,0).	VERIFIED_EXACT_COMPUTATION	Exact rational arithmetic.	Both verification JSON files.	Two implementations.	Public formula recorded by Zhang, 2026.	None for the evaluations.
The map is a counterexample in dimension three.	REPRODUCED_KNOWN_RESULT	Over C; constant nonzero determinant plus two distinct points with one image rules out injectivity.	Exact determinant and collision certificates.	Both implementations plus elementary implication.	Public announcement, 2026; no journal review asserted.	Provenance and literature priority remain external questions.
The plane case remains open as of 2026-07-23.	SOURCE_REQUIRED	Characteristic zero, dimension two.	Multiple current expository/preprint pages say so.	Not a mathematical computation.	Current source matrix.	A status claim cannot be exhaustively proved by search.
Below maximum degree 125, (72,108) and its symmetric pair are the only survivors claimed by the 2022 paper.	SOURCE_REQUIRED	Plane Jacobian counterexample; exact normalizations and base-field hypotheses must be extracted from the paper.	arXiv:2204.14178 abstract and HTML introduction.	None yet.	Guccione et al., preprint v1 (2022).	Read proof and dependency papers; check journal status.
No z=k slice plus coordinate projection yields a constant-Jacobian map.	VERIFIED_THEOREM	Any k in a characteristic-zero field; output pair among (A,B),(A,C),(B,C).	Nonconstant coefficients -89 y^3, -16 y, -42xy.	Direct symbolic expressions saved in descent JSON.	This repository.	Does not cover non-coordinate projections or conjugacy.
Solving C=0 cannot yield a plane Keller counterexample while preserving the displayed collision.	VERIFIED_THEOREM	Reduced affine varieties over C; use the two irreducible components of C=0.	Proof in notes/descent_attempts.md; exact restricted maps.	SymPy certificate plus coordinate-ring proof.	This repository.	Does not cover levels of other components or conjugacy.
The unique affine plane through the three collision points fails after every coordinate projection.	VERIFIED_EXACT_COMPUTATION	Plane 3x+2y=0; coordinate output pairs only.	Three exact nonconstant minors in descent JSON.	Collision reevaluated exactly.	This repository.	General two-output polynomial combinations untested.
A two-variable analogue of the same weighted quotient mechanism is impossible.	CONJECTURAL	Must first define the admissible family and support bounds.	Research hypothesis H1.	None.	This repository.	Formulate and run finite classification.
Every hyperbolically G_m-equivariant plane Keller map in characteristic zero is linear after diagonalizing the actions.	REPRODUCED_KNOWN_RESULT	Standard diagonal action with coprime weights (a,-b); arbitrary actions over C additionally use linearization.	Complete leading-coefficient proof in notes/equivariant_no_go_theorem.md.	SymPy symbolic families and independent sparse exact verifier.	Shaska, arXiv:2607.20210v1, Theorem 3.3.	None for the diagonal hyperbolic theorem; broader novelty is not claimed.
On an orbit-parameter cover, an equivariant map satisfies det(DG)=±mu^sum(w) det(DH).	VERIFIED_THEOREM	Integer weights; source/target weight multisets agree; matched nonzero orbit weight; rational orbit chart.	Chain-rule proof in notes/quotient_jacobian_weight_formula.md.	Generic exact coordinate-change checks plus the independent sparse announced-map certificate.	Derived after Shaska Remark 6.2; no exact prior source located.	Priority review and intrinsic stack formulation remain.
The exponent two in the announced map's quotient Jacobian equals minus the total source weight.	VERIFIED_EXACT_COMPUTATION	Weights (1,-1,-2), orbit multiplier L=C/x=2-3u-v, invariants (BC,AC^2).	Jac(BC,AC^2)=2L^2; total weight -2.	SymPy and independent sparse arithmetic.	Shaska Theorem 6.1 proves the example-specific relation; this repository supplies the weight explanation.	Coarse-quotient generalization for non-unit orbit weights.
On a regular polynomial quotient chart, the sign of total weight gives a three-way constraint on the orbit multiplier and quotient Jacobian.	VERIFIED_THEOREM	Algebraically closed characteristic-zero field; H and mu regular polynomial; ambient map Keller.	Immediate divisibility corollary of the quotient-weight formula.	Symbolic cases cover negative, zero, and positive total weight.	This repository; priority unassessed.	The conclusion is chamber-dependent and not yet globalized.
Weighted source/output conjugation satisfies J(P_tau,Q_tau)=tau^(a+b-c-d)J(P,Q)(tau^a x,tau^b y).	VERIFIED_THEOREM	Polynomial pair; integer weights; Laurent family allowed.	Chain-rule proof and weighted_conjugation.py.	Standalone verifier reconstructs the displayed families without primary-module imports.	Heitmann Lemma 1.1 gives the equivalent valuation inequality; formula derived here.	None.
A lowest positive-weight special pair of a normalized plane Keller map is either an automorphic Keller pair or algebraically dependent and non-dominant.	VERIFIED_THEOREM	Infinite characteristic-zero field; F(0)=0; strictly positive source weights; both lowest components nonzero.	Weight-layer proof in candidate_reduction_theorems.md; exact classifiers.	Independent verifier checks strict/equality cases; layer identities tested separately.	Heitmann 1990 supports the equality criterion; Shaska 2026 supports positive equivariant invertibility.	Higher layers are not retained.
If a highest positive-weight face has p+q=a+b, the full plane Keller map is triangular/affine; otherwise its leading pair is dependent and non-dominant.	VERIFIED_THEOREM	Infinite characteristic-zero field; target translated so F(0)=0; positive weights.	Complete proof in candidate_reduction_theorems.md; exact classifier.	Independent examples and bounded support scan; proof is unbounded and does not rely on the scan.	Heitmann 1990, Lemmas 1.1-1.2.	Priority of the exact triangular formulation is SOURCE_REQUIRED.
Ordinary positive-weight degeneration preserves a noninvertible dominant Keller obstruction.	DISPROVED_LEMMA	Naive one-weight lowest or highest Rees special fiber.	General dichotomy plus pole/dependence examples.	Primary and independent JSON certificates.	This repository; consistent with graded no-go theorems.	Flagged, multi-valuation, or parameter-dependent reductions remain open.
The two initial generators automatically define the full associated-graded Keller map.	DISPROVED_LEMMA	Arbitrary filtration/Rees flatness without a strict/SAGBI assumption.	P=x+y^2,Q=y: initials generate k[y], while the full graded ring is k[x,y]; P-Q^2=x.	Rees torsion/saturation certificate and independent bracket reconstruction.	Anderson 2013 requires compatible filtrations to induce Rees maps.	The full filtered object is not a two-coordinate plane special map.
A single dicritical divisor canonically produces a hyperbolic A^2 Keller model.	DISPROVED_LEMMA	Smooth surface and one divisorial valuation; canonical normal-cone construction.	Canonical-shift bracket and normal-bundle category obstruction.	Direct local wedge calculation; line-at-infinity normal bundle gives an explicit check.	Nguyen 1999 supplies an equality-layer Wronskian on a distinct separative series, not at the dicritical endpoint and not as an A^2 map.	A coupled dicritical/separative construction remains open.
In a fixed affine regular family with dominant generic and special plane maps, function-field degree satisfies d_0 <= d_eta.	VERIFIED_THEOREM	Infinite characteristic-zero field; P,Q in k[t,x,y]; both fibers dominant.	Primitive-element specialization proof in noninvertibility_preservation.md.	Exact strict examples 2 -> 1; finite-locally-free equality boundary checked independently.	Literature priority SOURCE_REQUIRED.	Not applicable to non-dominant special fibers, varying models, or inseparable characteristic.
Flat ambient source, target, and graph plus strict J=1 preserve noninjectivity in a Keller family.	DISPROVED_LEMMA	Polynomial family; no properness/finite-locally-free hypothesis on graph-to-target projection.	Normalized verified 3D map has noninjective generic fibers and a linear automorphic special fiber, determinant one throughout.	Primary modular and standalone exact computations.	This repository.	Dimension three; a plane-specific preservation theorem is not ruled out.
A divisorial valuation carries a shifted residue bracket v({f,g}) >= v(f)+v(g)-kappa_E.	VERIFIED_THEOREM	Smooth surface, prime divisor, rational functions, local normal/tangent parameters.	Direct expansion of df wedge dg in infinity_valuation_model.md.	Origin and line-at-infinity specializations reproduce both Rees exponents.	Lê-Weber 1994 and Nguyen 1999 give related infinity formulas.	Global finite generation and boundary preservation are separate.
Nguyen's nonzero Delta_phi=2 Wronskian occurs at a genuine dicritical endpoint.	DISPROVED_LEMMA	Nguyen's 1999 definitions and the 2004 associated sequence over C.	Dicritical endpoint has a_phi=b_phi=0; all positive ancestors have common roots, J_i=0, and strict Delta_i>2.	Direct symbolic equality/strict controls in both flagged verifiers.	Nguyen 1999, Def. 3.4, Thm. 3.6, Main Lemma 3.3; Nguyen 2004, Lemma 3 and proof of Thm. 1.	A new coupled dicritical plus separative filtration would be required.
A divisor-point flag defines a rank-two lexicographic valuation.	VERIFIED_THEOREM	Smooth surface, prime divisor E, closed smooth point p in E, rational functions; residue valuation on k(E).	Composite-valuation proof in rank_two_flag_valuations.md.	Exact monomial chart verifies multiplicativity and ultrametric inequality.	Standard composite valuation construction; project-specific formulation.	Choice of (E,p) is not canonical and does not encode a disjoint second branch.
The full Z^2_lex flag-Rees algebra is Noetherian whenever the flag associated graded is finitely generated.	DISPROVED_LEMMA	Increasing full-cone filtration with constants in every nonnegative piece.	Evaluation quotient onto C[Gamma_+]; (1,-N) proves the positive cone is not finitely generated.	Proof certificate and independent witness reconstruction.	This repository; literature priority SOURCE_REQUIRED.	An affine-submonoid replacement is a different degeneration requiring new proofs.
The natural independently labelled two-pole construction is a two-dimensional normal affine domain retaining both labels.	DISPROVED_LEMMA	Two points 0,infinity on P1; full two-budget multisection or corner associated graded.	Full ring C[A,B,C,D]/(AC-BD) has dimension 3; diagonal cone loses labels; corner C[W,L,R]/(LR) is reducible.	Hilbert-basis decompositions and presentations independently checked.	This repository.	Does not quantify over every noncanonical coupled construction.
Nguyen's equality Wronskian is an ordinary or global logarithmic Jacobian unit on a graded surface.	DISPROVED_LEMMA	Laurent boundary chart with P=t^-a p(xi)+..., Q=t^-b q(xi)+....	Exact wedge calculation and parameter law; log coefficient is J_phi/(pq).	Primary and independent symbolic verifiers.	Nguyen 1999 supplies the coefficient identity.	It is naturally a residue/twisted-canonical coefficient; extra trivialization would be new.
Relative Cartier plus finite-locally-free marked boundary data preserves the marked nonproper target curve in every fiber.	VERIFIED_THEOREM	Fiber-compatible relative graph closure; geometrically irreducible relative Cartier D; flat integral affine C; D->C finite locally free of rank d>0.	Base change preserves Cartier property and finite locally free positive rank; Jelonek identifies graph-boundary image with nonproper values.	The family (x^2y+t^2x,y) gives an exact rank-one chart control.	Jelonek 1993 Prop. 14; standard base-change facts recorded in source matrix.	These strong hypotheses are not derived from a Keller flag-Rees construction.
A dominant hyperbolically equivariant boundary-preserving surface map with log-Jacobian unit must be an automorphism.	DISPROVED_LEMMA	Even X=A2, coordinate boundary, characteristic zero.	(x^2y,y) has log determinant 2, generic degree 2, contracts y=0, and is nonautomorphic.	Ordinary and log determinants independently reconstructed.	Toric/log interpretation checked against Kato 1989.	Ordinary Jacobian unit, or exact characteristic map plus torsion-free cokernel, is substantially stronger.
The exact fixed-presentation two-pole Keller class is excluded.	INCOMPLETE_ARGUMENT	#Pol(F,P)=2 for a fixed ordered coordinate pair.	Nguyen's audited theorems do not give this exclusion; finite-support controls are narrower.	Referee checklist rejects promotion.	Nguyen 1999/2004.	No minimal infinity class is newly excluded in this cycle.
A full-rank map between pointed saturated rank-two affine cone monoids is exact exactly when the inverse target cone equals the source cone.	VERIFIED_THEOREM	Q=sigma_Q cap L_Q, P=sigma_P cap L_P; rational pointed full-dimensional cones; injective full-rank lattice map carrying source cone into target cone.	Rational-cone lattice-point proof in notes/breakthrough_program/characteristic_monoid_exactness.md.	Smooth enumeration plus a singular-cone reconstruction in both breakthrough certificates.	This repository.	Does not derive exactness for the characteristic map of every Keller compactification.
Exactness of the characteristic monoid map forces torsion-free group cokernel.	DISPROVED_LEMMA	Even saturated pointed rank-two monoids and both marked extremal rays.	diag(m,1) and the singular-cone index-two control are exact with nonzero torsion.	Smith invariants independently reconstructed.	This repository.	A Keller-derived primitive lattice condition would be additional data.
Equality of selected ordinary rational two-forms plus a boundary-dominant component forces characteristic lattice index one.	DISPROVED_LEMMA	Normal finite-type two-dimensional model; one marked divisor dominates a target curve.	x=AB,y=AB^2, (U,V)=(A^2B^2,B/2) has form equality and index two.	Standalone symbolic wedge and determinant reconstruction.	This repository.	Not an actual nonautomorphic polynomial Keller map; missing invariant is boundary primitivity of the affine volume form.
Ordinary and logarithmic ramification satisfy R_H=R_H^log+H^*B_Y-B_X.	VERIFIED_THEOREM	Dominant generically finite smooth surface germs with reduced normal-crossing boundaries; coefficientwise at normal generic boundary points.	Canonical divisor subtraction and monomial formula in ordinary_boundary_ramification.md.	Independent chart Jacobians.	Standard canonical/log divisor identities, specialized here.	Conductor corrections remain if one works away from normal generic points.
At a dicritical generic point over an affine target curve, transverse Kummer index equals canonical shift and ordinary ramification plus one.	REPRODUCED_KNOWN_RESULT	Actual Keller graph chart; source divisor maps dominantly and generically finitely to a smooth affine target curve; normal smooth generic points; characteristic zero.	Local parameters give H^*t=u^e unit, hence ord H^*(dt wedge ds)=e-1; compare with dx wedge dy.	Standalone controls reconstruct indices 1 through 6.	Borisov, J. Algebraic Combinatorics 39 (2014), plus this repository's local proof.	Does not determine the index without determinant-label information.
An affine-dominating dicritical divisor in a hypothetical nonproper Keller resolution has canonical/Kummer index at least two and positive ordinary ramification.	REPRODUCED_KNOWN_RESULT	Resolved complex plane Keller map; boundary curve maps to a curve in A^2; Borisov augmented-canonical and determinant labels.	Such curves have negative determinant label; label-one valuations have nonnegative determinant label; positive label equals ramification index.	Source proof and local identity cross-checked; no generator dependence.	Borisov, J. Algebraic Combinatorics 39 (2014), pp.691-710.	Does not bound indices above two or exclude a counterexample; shows zero ramification would already be globally contradictory.
J(P,Q)=1 forces zero ordinary ramification on every compactified boundary chart.	DISPROVED_LEMMA	Arbitrary compatible compactification, without a crepant/primitivity condition.	The polynomial automorphism (x,y+x^m) has chart (U,W)=(u,u^m/(v+1)) and ramification order m.	Standalone affine and chart Jacobian calculation.	This repository.	Does not refute a stronger theorem retaining a nonproper divisor under unavoidable relative hypotheses.
In an irreducible generic exactly-two-pole Keller fiber, finite-valued boundary ramification has total n+2g.	VERIFIED_THEOREM	Ordered pair (P,Q); smooth irreducible generic P-fiber; compact restriction degree n, genus g; exactly two distinct poles.	Hamiltonian vector field gives no affine ramification; Riemann-Hurwitz proof in exactly_two_pole_class.md.	Independent exact totals and z+1/z positive control.	This repository; classical Riemann-Hurwitz.	Does not exclude embedded plane realizations; generic-fiber irreducibility is explicit.
In the transverse nonvertical dicritical charts of an irreducible exactly-two-pole fiber, sum_p(kappa_D(p)-1)=n+2g.	VERIFIED_THEOREM	Same two-pole assumptions; generic vertical target line transverse to smooth nonproper-curve loci; smooth normal source generic points.	Combine the local dicritical Kummer-canonical identity with the two-pole Riemann-Hurwitz theorem.	Canonical-shift profiles independently reconstructed as ramification deficits plus one.	This repository.	Repeated punctures may lie on one dicritical class, so the equality does not prove independent marks.
The irreducible coordinate-fixed exactly-two-pole class has at least four distinct punctures.	VERIFIED_THEOREM	Same assumptions as the two-pole ramification theorem.	Two pole points plus at least two finite ramified punctures.	Exact partition enumeration.	This repository.	Presentation-dependent; does not prove the global independent-mark gate.
Every hypothetical nonautomorphic Keller map has at least three coordinate-independent coupled infinity marks.	INCOMPLETE_ARGUMENT	A coordinate-invariant equivalence relation on dicritical, separative, polar, and puncture data is required.	The one-separative/two-polar plus one-dicritical pattern survives current constraints.	Referee report rejects counting descendants twice.	Nguyen 1999/2004 plus this repository.	Must separate the forced finite ramification points into independent dicritical classes or minimize over target presentations.
The surviving sub-125 degree case is the (8,28), (3,2) family giving degree pair (72,108), while the (9,27) degree-108 family is excluded.	REPRODUCED_KNOWN_RESULT	Standard-pair and Laurent conventions inherited by the Guccione papers over characteristic zero.	Full PDFs; algorithms tables pp.27-28; 2022 Proposition 4.3 and Corollary 5.7 visually checked.	Repository table exactly reconstructs the ten cases and unique survivor.	Guccione et al., arXiv:1708.07936v1 and arXiv:2204.14178v1.	Full independent reconstruction of every inherited exclusion is not complete.
The vertex-only approximate-root skeleton inside the surviving (8,28) polygons is impossible.	VERIFIED_EXACT_COMPUTATION	Exact displayed four-parameter ansatz; transformed equation [P,Q]=x^2; omitted edge/interior coefficients fixed to zero.	Seventeen coefficient equations have Groebner basis (1).	Standalone verifier rebuilds the ideal.	This repository.	Not exhaustive for either full Newton polygon; no Breakthrough Gate follows.
The full surviving (8,28) Newton configuration is excluded.	INCOMPLETE_ARGUMENT	Every lattice coefficient in both Proposition 4.3 polygons and all allowed normalizations.	Only a vertex-only subansatz is excluded.	Adversarial review rejects exhaustiveness.	Guccione et al. 2022 and this repository.	Complete approximate-root recursion and finite elimination remain.
The coordinate-optimized generic-fiber branch mark count satisfies N_branch(F)>=3 for every nonautomorphic plane Keller map.	REPRODUCED_KNOWN_RESULT	N_branch minimizes the number of branches at infinity of a generic component fiber over all target polynomial automorphisms and both components; complex plane; source/target automorphism invariance.	Druzkowski's 1991 two-branch theorem applied to a minimizing presentation; source changes identify normalizations and target changes reindex the minimum.	Original p.99 theorem/proof visually checked.	Druzkowski, Ann. Polon. Math. 55 (1991), 95-101.	Does not imply three dicritical divisors, poles, or separative chains; known result, not an original gate.
Each complete (8,28) P-coefficient space contains a nonempty Zariski-open locus on which no allowed Q solves [P,Q]=x^2.	VERIFIED_THEOREM	All 61/125 lattice points in the polygon with vertical left edges and all 25/47 points without; arbitrary characteristic zero after the integral certificate.	Explicit maximal augmented minors specialize nonzero modulo 2147483629; ranks are 124/125 and 46/47.	Standalone reconstruction uses different coefficients and prime 2147483587.	This repository; priority overlaps Santibanez-Leal Zenodo v0.07 / CAOS_RESEARCH sampled-minor program.	All survivors lie on determinantal exceptional hypersurfaces; those closed loci are not excluded.
The live Santibanez-Leal (72,108) program has completely excluded both Proposition 4.3 polygons.	DISPROVED_LEMMA	Public Zenodo v0.07 and CAOS_RESEARCH main at audited commit.	Its own scope statements keep the floor raise gated on a simultaneous-all-coefficients certificate; degree three is open through triple supports.	Repository verdict audit includes the EXP-070 arithmetic-bug retraction and corrected EXP-071/072 record.	DOI 10.5281/zenodo.21503368 and commit b8237a8e980830173defacb9923016717f3f66f8.	A later repository version may change; re-audit before relying on current status.
The full smaller Proposition 4.3 system is equivalent to five univariate Belyi-lift equations.	VERIFIED_THEOREM	Complete 25/47 lattice supports; Laurent change z=xy^2,t=1/y; characteristic zero.	Direct chain rule and exact comparison of every t coefficient; no coefficient specialization.	Standalone verifier reconstructs both transformed polygons; tests re-expand the symbolic Jacobian.	This repository.	The reduction is lossless; the companion degree-35 lift certificate now proves the five-equation system inconsistent with the required G_12 vertex.
The bottom edge of the smaller polygon is impossible by passport or monodromy.	DISPROVED_LEMMA	Forced degrees A=z*a, D=z^2*d, deg(a,d)=(7,10), nonzero vertices.	R=D^2/A^3 has passport (2^10,1),(3^7),(17,1^4); an exact transitive genus-zero permutation triple exists.	Independent reconstruction gives product one, the three cycle types, transitivity, genus zero, and group order 21!/2.	Riemann-existence correspondence as stated in Manes-Melamed-Tobin, arXiv:1908.10459; finite witness from this repository.	Edge realizability does not imply that any realization lifts through the other four equations.
The degree-21 edge passport has exactly five dessin isomorphism classes.	VERIFIED_EXACT_COMPUTATION	Labeled branch values; cycle types (2^10,1),(3^7),(17,1^4); connected genus-zero covers.	Four face monogons reduce the dessin to one of two trees with degree sequence (3,3,2,1,1,1,1); all 2^7 ribbon orders per tree give orbit counts 4+1.	Standalone enumeration reverses the simultaneous-conjugacy canonical traversal and returns the same five classes.	This repository; Riemann-existence bridge from Manes-Melamed-Tobin, arXiv:1908.10459.	No matching published enumeration was found in exact-coordinate/passport searches.
The smaller Proposition 4.3 Newton pair admits no solution of [P,Q]=x^2.	MAJOR_BREAKTHROUGH	Algebraically closed characteristic-zero field; exact 25/47 Newton polygons conv{(0,0),(1,0),(8,14),(8,16)} and conv{(0,0),(2,1),(12,21),(12,24)}.	Exact edge recurrence gives seven tail equations; exact modular-reconstruction/FGLM yields one reduced degree-35 edge field. Layer ranks are 17/19, 18/20, and 12/12; third-layer compatibility has minor gcd 1, forcing B=E=0, then G'=0, contradicting G_12!=0.	Independent Sage verifier changes column order and both kernel bases and obtains Groebner basis (1) for the direct compatibility ideal in K[q,r,s]; deleting G_12 gives an exact positive control.	This repository; source configuration is Guccione et al., arXiv:2204.14178v1, Proposition 4.3(2).	This theorem is frozen separately; the larger configuration is now excluded by the logical branch theorem below.
The larger Proposition 4.3 Laurent system has exactly 61/125 slots, 302 nontrivial coefficient equations, and first normalized top/right obstruction at layer 5.	VERIFIED_THEOREM	Exact larger polygons; algebraically closed characteristic-zero base; normalized degree-35 top edge.	Unimodular Laurent support enumeration, independent full symbolic bracket expansion, and exact cokernel projection retaining all five early kernel parameters.	Tests independently compare sparse and symbolic rows; frozen lex hash and all rank tables are checked.	This repository.	This is a finite reduction milestone, not a polygon exclusion.
The coefficient-zero chart of the first larger-polygon layer-5 obstruction is empty.	VERIFIED_THEOREM	Chart c(x1)=0 of f=c(x1)x5+b; exact degree-35 field K; compatibility through top layers 5--7.	Five low-degree compatibility generators have an explicit 72,672,850-byte Bezout identity sum(q_i*f_i)=1 over K (SHA-256 481efe2c...f7fe8), not just a basis (1).	A primary parser rebinds every hash and expands the serialized identity; a second constructor descends through the mu_7 action to a degree-five subfield, runs liftstd, lifts back, and exactly reproduces the same multipliers. The existing reversed-variable lex verifier independently gives basis (1).	This repository.	None for this chart; the principal c!=0 chart and global chart cover remain separate gates.
The principal c(x1)!=0 chart is excluded by layer 7.	VERIFIED_THEOREM	Corrected six-generator row split on the principal chart over the reduced degree-five field.	The exact identity b2*p0-a2*r7=D*Y+E gives the exhaustive split D!=0 versus D=0,E=0. In D!=0, the a2=0 and degree-one strata have gcd one; on the degree-18 stratum a linear L divides D,E, L^2 divides Q0,P1, and a fixed residual (5,6) Sylvester determinant is nonzero. In D=E=0, Res_X(D,E) is squarefree with factors (1,18); the linear factor has no D,E root and the degree-18 factor has a nonzero fraction-free value of Res_Y(p0,p1).	A source-chain verifier rebuilds the degree-five descent, quotient matrix, right inverse, and all six row-split generators from the original degree-35 principal system. Independent residue-field paths reproduce the degree-18 Sylvester nonvanishing and both D=E=0 factor witnesses.	This repository.	No unknown multiplier degree or prime enumeration is used. The historical 2,900-column CRT reconstruction is not part of this proof.
The full larger Proposition 4.3 Newton configuration is excluded.	MAJOR_BREAKTHROUGH	Algebraically closed characteristic-zero field; exact 61/125 transformed supports; every forced Newton vertex nonzero, with arbitrary interior coefficients.	The top/right layer scheme is a necessary superset of the complete coefficient scheme. Its exhaustive charts V(c) and D(c) are empty respectively by an explicit characteristic-zero Bezout identity and the finite logical branch theorem above.	large_polygon_logical_coverage_audit.json binds the lossless support count, degree-35 edge field, layer ranks, both chart certificates, source chain, terminal nonvanishing witnesses, and omitted-equation logical direction.	This repository; source configuration is Guccione et al., arXiv:2204.14178v1, Proposition 4.3.	This excludes one Newton configuration, not all larger polygons and not the plane Jacobian conjecture.
Every hypothetical characteristic-zero plane Jacobian counterexample has maximum degree at least 125.	VERIFIED_THEOREM	The two exact Proposition 4.3 exclusions plus the pinned published finite-case reduction and exchange/base-change audits.	The 2022 Theorem 2.1 leaves only the (72,108) family below 125; Proposition 4.3 gives exactly the two now-excluded Newton configurations.	global_degree_bound_125_audit.json binds both frozen configuration certificates, source archive hashes, literature audit, symmetry, and ground-field reduction.	Guccione et al. 2013/2014/2017/2022 plus this repository.	Dependency-bearing corollary; it does not exclude degree 125 or larger and does not prove the Jacobian conjecture.