Jacobian discovery lab

A new, independently checkable result

Which precise unreported statement survives exact computation, Lean verification, and a prior-art audit?

Perfect-square sextics give an omitted surface for Gao F6

Does the square fiber polynomial force every candidate preimage to have zero escape multiplier?

Check the deleted-root condition, not just a discriminant

What exact identity relates the reconstructed gamma to the fiber polynomial and its derivative?

Classify the realizable simple-root counts of the sextic slice

Which multiplicity partitions occur in 2t^6-2t^5-t^3+a t^2+b t+c?

Compress a Keller counterexample while preserving the full Jacobian

Can a stable polynomial equivalence improve the published explicit cubic dimensions?

Six-variable arithmetic-circuit lift fails off the constraint graph

Does replacing repeated products by constrained variables preserve a constant ambient Jacobian?

Degree reduction in the original symmetry class is crowded

Is there an unclaimed degree-five or degree-six construction beyond the classified symmetry class?

Two-variable Gaussian moments remain a distinct target

Can a richer mixture of positive and negative weights produce all vanishing moments in two Gaussian variables?

Monomial data challenge middle-branch rigidity

Does a full-rank middle-branch sweep with a noncylindrical critical-value hypersurface answer Gao Problem 4.8 negatively?

Real-only coefficient searches miss the monomial witness

Can the displayed parameter equations be solved over the reals?

Higher monomials suggest non-suspended cones in every even degree

Do G2=v^n w and G4=A v^(2n+1)w give a uniform theorem for all n at least one?

Three additional substantive results

Which three distinct new results survive the same novelty and proof audit?

An eight-dimensional polynomial Hurwitz counterexample

Does the explicit eight-dimensional field have constant spectrum {-1} and three distinct zeros?

Gaussian quartic moduli and an exhaustive ansatz classification

Can every zero-moment polynomial Wh(Z)+v(Z)T²+b(Z)T+c(Z) be classified, giving a sharp degree-four lower bound in this family?

The full omitted set of Gao F6

Does the omitted surface exhaust every missing target, including the first-coordinate boundary?

coeff mul 0

Status: proved

See the linked Lean declaration for the exact statement.

coeff mul 1

Status: proved

See the linked Lean declaration for the exact statement.

coeff mul 2

Status: proved

See the linked Lean declaration for the exact statement.

coeff mul 3

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 2 0

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 2 1

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 2 2

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 2 3

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 3 0

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 3 1

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 3 2

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 3 3

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 4 0

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 4 1

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 4 2

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 4 3

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 5 0

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 5 1

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 5 2

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 5 3

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 6 0

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 6 1

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 6 2

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 6 3

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 7 0

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 7 1

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 7 2

Status: proved

See the linked Lean declaration for the exact statement.

coeff pow 7 3

Status: proved

See the linked Lean declaration for the exact statement.

Is this the full omitted locus on C ≠ 0?

Status: proved

The formerly open omitted-locus converse is now proved for every nonzero first coordinate.

g2

Status: proved

See the linked Lean declaration for the exact statement.

g3

Status: proved

See the linked Lean declaration for the exact statement.

g4

Status: proved

See the linked Lean declaration for the exact statement.

x1

Status: proved

See the linked Lean declaration for the exact statement.

sweep

Status: proved

See the linked Lean declaration for the exact statement.

fiber

Status: proved

See the linked Lean declaration for the exact statement.

fiberDerivative

Status: proved

See the linked Lean declaration for the exact statement.

squareCubic

Status: proved

See the linked Lean declaration for the exact statement.

omitted

Status: proved

See the linked Lean declaration for the exact statement.

The sextic becomes a square

Status: proved

At the omitted targets, R(t)=2(t³−t²/2−t/8−5/16)².

square derivative

Status: proved

See the linked Lean declaration for the exact statement.

The exact multiplier identity

Status: proved

After reconstructing the other parameters, gamma = R′ − 2R.

sweep reconstruction

Status: proved

See the linked Lean declaration for the exact statement.

omitted requires zero multiplier

Status: proved

See the linked Lean declaration for the exact statement.

Square fibers cannot survive the twist

Status: proved

The specified sweep target can only be attained with escape multiplier zero.

e1

Status: proved

See the linked Lean declaration for the exact statement.

e2

Status: proved

See the linked Lean declaration for the exact statement.

e3

Status: proved

See the linked Lean declaration for the exact statement.

e4

Status: proved

See the linked Lean declaration for the exact statement.

stageG

Status: proved

See the linked Lean declaration for the exact statement.

stageU

Status: proved

See the linked Lean declaration for the exact statement.

stageV

Status: proved

See the linked Lean declaration for the exact statement.

stageW

Status: proved

See the linked Lean declaration for the exact statement.

numerator

Status: proved

See the linked Lean declaration for the exact statement.

The denominators cancel polynomially

Status: proved

The i-th scaled sweep numerator is divisible by X^(i+1).

scaled sweep

Status: proved

See the linked Lean declaration for the exact statement.

map

Status: proved

See the linked Lean declaration for the exact statement.

quotient identity

Status: proved

See the linked Lean declaration for the exact statement.

eval numerator

Status: proved

See the linked Lean declaration for the exact statement.

map sweep link

Status: proved

See the linked Lean declaration for the exact statement.

omittedSurface

Status: proved

See the linked Lean declaration for the exact statement.

An explicit omitted surface

Status: proved

For C nonzero and arbitrary b, F6 never equals (C, -11/(32C), b/C², (b+25/128)/C³, (-b²+53b/32+1773/4096)/C⁴).

Gao F6 is not surjective

Status: proved

The explicit five-dimensional polynomial map F6 misses an explicit rational surface.

P

Status: proved

See the linked Lean declaration for the exact statement.

x

Status: proved

See the linked Lean declaration for the exact statement.

y

Status: proved

See the linked Lean declaration for the exact statement.

z

Status: proved

See the linked Lean declaration for the exact statement.

alpoge

Status: proved

See the linked Lean declaration for the exact statement.

jac

Status: proved

See the linked Lean declaration for the exact statement.

pderiv num

Status: proved

See the linked Lean declaration for the exact statement.

pderiv one'

Status: proved

See the linked Lean declaration for the exact statement.

d00

Status: proved

See the linked Lean declaration for the exact statement.

d01

Status: proved

See the linked Lean declaration for the exact statement.

d02

Status: proved

See the linked Lean declaration for the exact statement.

d10

Status: proved

See the linked Lean declaration for the exact statement.

d11

Status: proved

See the linked Lean declaration for the exact statement.

d12

Status: proved

See the linked Lean declaration for the exact statement.

d20

Status: proved

See the linked Lean declaration for the exact statement.

d21

Status: proved

See the linked Lean declaration for the exact statement.

d22

Status: proved

See the linked Lean declaration for the exact statement.

alpoge keller

Status: proved

See the linked Lean declaration for the exact statement.

evalAt

Status: proved

See the linked Lean declaration for the exact statement.

alpoge collision

Status: proved

See the linked Lean declaration for the exact statement.

Original counterexample: verification

Status: proved

Supporting declarations and definitions.

Sweep and fiber definitions

Status: proved

Supporting declarations and definitions.

Polynomial-map definitions

Status: proved

Supporting declarations and definitions.

Polynomial coefficient library

Status: proved

Supporting declarations and definitions.

A rational point outside the image

Status: proved

For every source p, F6(p) differs from (1, -11/32, 0, 25/128, 1773/4096).

surface

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

sweep

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

potentials

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

pencil

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

pencil determinant

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

surfaceMinor

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

minor determinant

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

parameter nonzero

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

quartic

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

imageConstant

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

image constant nonzero

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

surface on quartic

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

singular

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

singular locus

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

complexA

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

complexB

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

complex parameters

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

full rank witness

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

polynomialMap

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

polynomialJacobian

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

polynomial jacobian entries

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

polynomial jacobian determinant

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

P

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

equation

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

tangentExpression

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

tangent field fixes vertex

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

derivation equation

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

Every tangent derivation vanishes at the vertex

Status: proved

Coefficient extraction at four degree-three monomials forces the constant vector field to vanish.

No slice even modulo the equation

Status: proved

A derivation preserving the quartic ideal cannot differentiate any polynomial to 1 modulo that ideal.

chartInverse

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

chart reconstruction

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

Exact reconstruction on the dense chart

Status: proved

Every point of the quartic with a*d nonzero has an explicit preimage under the critical parametrization.

polynomialMap evaluation

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

critical value parametrization

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

surface minor is derivative

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

potentialPolynomial

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

directionPolynomial

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

pencil is derivative

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

no real parameter pair

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

relationIdeal

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

CoordinateRing

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

quotient

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

quotient equation

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

quotient surjective

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

derivation lift

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

quotient zero iff

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

No derivation of the quotient ring has a slice

Status: proved

All derivations vanish at the vertex, so no derivative can equal 1.

transportedDerivative

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

transported derivative slice

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

No polynomial-ring presentation over any algebra

Status: proved

An arbitrary polynomial-ring isomorphism would transport the derivative to a derivation with a slice.

The master equation is a perfect square

Status: proved

The pencil determinant equals (mu-B v²w)², so D2=1 and 4D0=D1².

Actual polynomial Jacobian equals g squared

Status: proved

The explicit complex-coefficient sweep belongs to the middle branch.

critical source

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

The critical image has a nonzero derivative minor

Status: proved

The verified first-three-coordinate derivative minor is nonzero at (0,1,1).

The critical-value quartic has no affine-line factor

Status: proved

For every complex algebra R, the coordinate ring of the exhibited quartic is not isomorphic to R[s].

mv pderiv numeral

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

mv coeff X mul

Status: proved

See the linked declaration for the exact hypotheses and conclusion.

MiddleBranch declarations

Status: proved

Definitions and auxiliary certificates.

ConeObstruction declarations

Status: proved

Definitions and auxiliary certificates.

ConeRing declarations

Status: proved

Definitions and auxiliary certificates.

MiddleResult declarations

Status: proved

Definitions and auxiliary certificates.

field

Status: proved

field. See the linked declaration for its exact quantified statement.

jacobian

Status: proved

jacobian. See the linked declaration for its exact quantified statement.

characteristicMatrix

Status: proved

characteristicMatrix. See the linked declaration for its exact quantified statement.

eval hasDerivAt

Status: library

eval hasDerivAt. See the linked declaration for its exact quantified statement.

polynomialMap

Status: proved

polynomialMap. See the linked declaration for its exact quantified statement.

polynomialJacobian

Status: proved

polynomialJacobian. See the linked declaration for its exact quantified statement.

polynomial jacobian entries

Status: proved

polynomial jacobian entries. See the linked declaration for its exact quantified statement.

polynomialMap evaluation

Status: proved

polynomialMap evaluation. See the linked declaration for its exact quantified statement.

polynomialJacobian evaluation

Status: proved

polynomialJacobian evaluation. See the linked declaration for its exact quantified statement.

analytic jacobian

Status: proved

analytic jacobian. See the linked declaration for its exact quantified statement.

characteristic determinant

Status: proved

characteristic determinant. See the linked declaration for its exact quantified statement.

vectorField

Status: proved

vectorField. See the linked declaration for its exact quantified statement.

zeroPoint

Status: proved

zeroPoint. See the linked declaration for its exact quantified statement.

positivePoint

Status: proved

positivePoint. See the linked declaration for its exact quantified statement.

negativePoint

Status: proved

negativePoint. See the linked declaration for its exact quantified statement.

three zeros

Status: proved

three zeros. See the linked declaration for its exact quantified statement.

three points distinct

Status: proved

three points distinct. See the linked declaration for its exact quantified statement.

not injective

Status: proved

not injective. See the linked declaration for its exact quantified statement.

characteristicMatrix eq

Status: proved

characteristicMatrix eq. See the linked declaration for its exact quantified statement.

characteristic root

Status: proved

characteristic root. See the linked declaration for its exact quantified statement.

analyticJacobian

Status: proved

analyticJacobian. See the linked declaration for its exact quantified statement.

IsHurwitz

Status: proved

IsHurwitz. See the linked declaration for its exact quantified statement.

actual jacobian

Status: proved

actual jacobian. See the linked declaration for its exact quantified statement.

complexified jacobian

Status: proved

complexified jacobian. See the linked declaration for its exact quantified statement.

vectorField hurwitz

Status: proved

vectorField hurwitz. See the linked declaration for its exact quantified statement.

vectorField smooth

Status: proved

vectorField smooth. See the linked declaration for its exact quantified statement.

Weak Markus–Yamabe fails in dimension eight

Status: proved

There exists a smooth map R^8 → R^8 whose analytic Jacobian has only characteristic roots with negative real part, but which is not injective.

eight 0

Status: library

eight 0. See the linked declaration for its exact quantified statement.

eight 1

Status: library

eight 1. See the linked declaration for its exact quantified statement.

eight 2

Status: library

eight 2. See the linked declaration for its exact quantified statement.

eight 3

Status: library

eight 3. See the linked declaration for its exact quantified statement.

eight 4

Status: library

eight 4. See the linked declaration for its exact quantified statement.

eight 5

Status: library

eight 5. See the linked declaration for its exact quantified statement.

eight 6

Status: library

eight 6. See the linked declaration for its exact quantified statement.

eight 7

Status: library

eight 7. See the linked declaration for its exact quantified statement.

roots derivative iff

Status: library

roots derivative iff. See the linked declaration for its exact quantified statement.

coeff mul 4

Status: library

coeff mul 4. See the linked declaration for its exact quantified statement.

coeff pow 2 4

Status: library

coeff pow 2 4. See the linked declaration for its exact quantified statement.

coeff pow 3 4

Status: library

coeff pow 3 4. See the linked declaration for its exact quantified statement.

coeff pow 4 4

Status: library

coeff pow 4 4. See the linked declaration for its exact quantified statement.

coeff pow 5 4

Status: library

coeff pow 5 4. See the linked declaration for its exact quantified statement.

coeff pow 6 4

Status: library

coeff pow 6 4. See the linked declaration for its exact quantified statement.

coeff pow 7 4

Status: library

coeff pow 7 4. See the linked declaration for its exact quantified statement.

sextic

Status: proved

sextic. See the linked declaration for its exact quantified statement.

divisionQuotient

Status: proved

divisionQuotient. See the linked declaration for its exact quantified statement.

divisionRemainder

Status: proved

divisionRemainder. See the linked declaration for its exact quantified statement.

division certificate

Status: proved

division certificate. See the linked declaration for its exact quantified statement.

sextic degree

Status: proved

sextic degree. See the linked declaration for its exact quantified statement.

remainder degree

Status: proved

remainder degree. See the linked declaration for its exact quantified statement.

remainder zero parameters

Status: proved

remainder zero parameters. See the linked declaration for its exact quantified statement.

divisibility classification

Status: proved

divisibility classification. See the linked declaration for its exact quantified statement.

no simple roots iff

Status: proved

no simple roots iff. See the linked declaration for its exact quantified statement.

sourceLift

Status: proved

sourceLift. See the linked declaration for its exact quantified statement.

sourceLift stages

Status: proved

sourceLift stages. See the linked declaration for its exact quantified statement.

sweep of root

Status: proved

sweep of root. See the linked declaration for its exact quantified statement.

lift sweep

Status: proved

lift sweep. See the linked declaration for its exact quantified statement.

fiberPolynomial

Status: proved

fiberPolynomial. See the linked declaration for its exact quantified statement.

fiberPolynomial eval

Status: proved

fiberPolynomial eval. See the linked declaration for its exact quantified statement.

fiberPolynomial derivative

Status: proved

fiberPolynomial derivative. See the linked declaration for its exact quantified statement.

parameters iff

Status: proved

parameters iff. See the linked declaration for its exact quantified statement.

all roots multiple iff

Status: proved

all roots multiple iff. See the linked declaration for its exact quantified statement.

normalizedTarget

Status: proved

normalizedTarget. See the linked declaration for its exact quantified statement.

normalized omitted iff

Status: proved

normalized omitted iff. See the linked declaration for its exact quantified statement.

preimage of simple root

Status: proved

preimage of simple root. See the linked declaration for its exact quantified statement.

full omitted locus

Status: proved

full omitted locus. See the linked declaration for its exact quantified statement.

divided numerator at zero

Status: proved

divided numerator at zero. See the linked declaration for its exact quantified statement.

boundary formula

Status: proved

boundary formula. See the linked declaration for its exact quantified statement.

boundary surjective

Status: proved

boundary surjective. See the linked declaration for its exact quantified statement.

The entire omitted set of Gao F6

Status: proved

A target is outside the actual polynomial map image exactly when its first coordinate C is nonzero and it lies on the explicitly parametrized omitted surface.

h

Status: proved

h. See the linked declaration for its exact quantified statement.

variance

Status: proved

variance. See the linked declaration for its exact quantified statement.

linearTerm

Status: proved

linearTerm. See the linked declaration for its exact quantified statement.

bias

Status: proved

bias. See the linked declaration for its exact quantified statement.

determinant identity

Status: proved

determinant identity. See the linked declaration for its exact quantified statement.

exponential identity

Status: proved

exponential identity. See the linked declaration for its exact quantified statement.

branch

Status: proved

branch. See the linked declaration for its exact quantified statement.

branch equation

Status: proved

branch equation. See the linked declaration for its exact quantified statement.

formal determinant cancellation

Status: proved

formal determinant cancellation. See the linked declaration for its exact quantified statement.

formal exponential cancellation

Status: proved

formal exponential cancellation. See the linked declaration for its exact quantified statement.

family

Status: proved

family. See the linked declaration for its exact quantified statement.

family specialization

Status: proved

family specialization. See the linked declaration for its exact quantified statement.

gaussian shear preserves covariance

Status: proved

gaussian shear preserves covariance. See the linked declaration for its exact quantified statement.

family shear

Status: proved

family shear. See the linked declaration for its exact quantified statement.

family reflection

Status: proved

family reflection. See the linked declaration for its exact quantified statement.

diagonal equivalence invariant

Status: proved

diagonal equivalence invariant. See the linked declaration for its exact quantified statement.

positive parameters distinct

Status: proved

positive parameters distinct. See the linked declaration for its exact quantified statement.

Infinitely many inequivalent quartic Gaussian counterexamples

Status: proved

Written proof: the family P_gamma has all pure moments zero and E[Z P_gamma^m]=m!, with complex-orthogonal/scalar equivalence exactly gamma=±delta. The full Wh+vT²+bT+c ansatz is classified.

Four research results and their proof boundaries

Status: proved

One earlier middle-branch construction and three additional results: an eight-dimensional Hurwitz counterexample, the entire omitted set of Gao F6, and a moduli classification of Gaussian counterexamples.

MarkusEight auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

MarkusPolynomial auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

MarkusResult auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

CalculusLibrary auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

VectorLibrary auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

PolynomialLibrary auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

JetLibrary auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

SexticClassification auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

GaoInverse auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

GaoImage auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.

GaussianFamily auxiliary declarations

Status: proved

Project-owned definitions and reusable certificates.