Skip to content

Latest commit

 

History

History
206 lines (156 loc) · 8.39 KB

File metadata and controls

206 lines (156 loc) · 8.39 KB

Reproduce the degree-125 submission

This document is written for the extracted submission supplement, not for a Git checkout. It covers both Proposition 4.3 Newton configurations and the separate, external-preprint-dependent degree consequence.

All proof-bearing computer algebra commands use the immutable image

sagemath/sagemath@sha256:e068670ae5863b54b2550e72437ec637b0283acb0dc712c8584c124dbf44e667

It contains SageMath 10.9 and Singular 4.4.1. No floating-point value, prime enumeration, or unbounded certificate-degree search is a theorem premise.

0. Verify archive integrity and environment

From the extracted supplement root:

python tools/verify_supplement_manifest.py

This must report zero missing, mismatched, and unlisted files. Then run:

docker run --rm --memory 30g --memory-swap 30g `
  -v "${PWD}:/repo" `
  sagemath/sagemath@sha256:e068670ae5863b54b2550e72437ec637b0283acb0dc712c8584c124dbf44e667 `
  bash -lc "export SAGE_DOT_SAGE=/tmp/sage; cd /repo; sage --version; Singular --version"

All remaining commands are shown without the Docker wrapper. Run them inside the same container with working directory /repo.

The integrity check is a pre-replay check. Sage creates .sage.py, __pycache__, and pytest cache files, while several regenerated JSON reports record nondeterministic elapsed_seconds. Consequently, rerunning the top-level manifest verifier in the same mutated directory is expected to report those new files and timing-only output differences. Re-extract the ZIP to a fresh directory to repeat the archive-integrity check. The mathematical statuses, fixed hashes, ranks, factors, and exact identities checked below are deterministic.

1. Recompute the smaller-configuration lift obstruction

The exact recurrence generator checks that the seven tail equations are precisely d_11=...=d_17=0. The two Sage verifiers then consume the frozen six-element lex basis, independently reconstruct the degree-35 field and all lift operators, and decide the terminal compatibility by different methods.

python experiments/breakthrough_program/belyi_edge_solver.py
sage experiments/breakthrough_program/belyi_lift_over_number_field.sage
sage experiments/breakthrough_program/independent_belyi_lift_verifier.sage

The primary output must contain BREAKTHROUGH_GATE_5=True; the independent output must end with a direct compatibility Groebner basis ["1"]. The full characteristic-zero Singular input and FGLM scripts are included as results/belyi_edge_Q.sing, results/belyi_edge_Q_fglm.sing, and results/belyi_edge_Q_fglm_export.sing. They are the from-scratch basis construction path; the two Sage commands above are the fast exact replay of the serialized basis and all theorem-bearing lift equations.

2. Rebuild the larger layer source chain

These commands regenerate the 61/125 support, all 302 Laurent-Jacobian coefficient equations, layers 1--5, the layer-1--4 state, the principal generators, and the exceptional-chart generators. Thus the later certificate verifiers are bound to the original Newton coefficient system rather than to unexplained JSON files.

sage -python experiments/larger_polygon_program/primary_verifier.py
sage -python experiments/larger_polygon_program/principal_exact_generators.py
sage -python experiments/larger_polygon_program/exceptional_chart.py
sage experiments/larger_polygon_program/verify_logical_principal_source_chain.sage

The last command must print

LOGICAL_PRINCIPAL_SOURCE_CHAIN_VERIFIED

It reconstructs the degree-five descent from the degree-35 principal generators, checks the field round trip and invertible coordinate change, replays the exact 2 x 5 quotient matrix and its constant right inverse, and reconstructs all six row-split generators.

3. Verify the exceptional chart V(c)

sage experiments/larger_polygon_program/verify_exceptional_unit_certificate.py
sage experiments/larger_polygon_program/independent_verify_exceptional_certificate.py

Both commands read the regenerated exceptional_chart_layers_5_7.json. They recompute every generator and multiplier hash and expand the five-multiplier characteristic-zero identity to exactly one. The second implementation uses a different reconstruction path and includes corruption controls.

4. Close the principal chart D(c)

The finite case split is driven by

b2*p0-a2*r7 = D*Y+E.

Every point therefore lies in D!=0 or D=0,E=0.

4.1 Close D!=0

sage experiments/larger_polygon_program/verify_generic_short_subbranches.sage
sage experiments/larger_polygon_program/verify_degree18_denominator_linear_factor.sage
sage experiments/larger_polygon_program/verify_degree18_good_reduction_witness.sage
sage experiments/larger_polygon_program/verify_degree18_denominator_component_independent.sage

These commands close the a2=0, degree-one, and degree-18 strata. The last stratum proves L | D,E, L^2 | Q0,P1, and nonvanishing of one fixed 11 x 11 Sylvester determinant. The finite-field calculation is only a guarded homomorphic image of that fixed characteristic-zero determinant.

4.2 Close D=0,E=0

sage experiments/larger_polygon_program/construct_d0_projection_checkpoints.sage
sage experiments/larger_polygon_program/prove_d0_factorwise_evaluation.sage
sage experiments/larger_polygon_program/verify_d0_factorwise_evaluation_independent.sage

Required statuses are

D0_EXCEPTIONAL_BRANCH_CLOSED_BY_FACTORIZED_EVALUATION
D0_EXCEPTIONAL_BRANCH_INDEPENDENTLY_VERIFIED

The exact resultant Res_X(D,E) is squarefree of degree 19 with irreducible factor degrees (1,18). Both factors are closed by exact fraction-free evaluations in characteristic zero.

5. Compose the larger theorem and global consequence

Still inside the container:

python experiments/larger_polygon_program/logical_coverage_audit.py
python experiments/larger_polygon_program/global_degree_bound_audit.py
python -m pytest -q tests/test_larger_polygon_logical_closure.py

The first status is

LARGE_POLYGON_EXCLUDED_BY_LOGICAL_BRANCH_CERTIFICATES

The global audit reruns both smaller-configuration Sage verifiers by default, checks their numerical and unit-ideal invariants, verifies the five actual distributed arXiv source archives byte-for-byte, and then emits GLOBAL_DEGREE_BOUND_125. It does not require Git metadata and does not use substring tests on project-authored Markdown as evidence. This final status is explicitly conditional on the pinned external preprint reduction.

The three pytest tests are regression checks for the generated JSON objects; they are not described as an independent mathematical verifier.

6. Optional forced recomputation of expensive checkpoints

The theorem replay above verifies serialized exact checkpoints. A stronger but much slower provenance audit can recompute the large resultants and all projection checkpoints from their displayed generators:

sage experiments/larger_polygon_program/sage_exact_resultant_r1.sage
sage experiments/larger_polygon_program/sage_exact_resultant_r4.sage
JACOBIAN_FORCE_RECOMPUTE=1 sage experiments/larger_polygon_program/verify_degree18_denominator_linear_factor.sage
JACOBIAN_FORCE_RECOMPUTE=1 sage experiments/larger_polygon_program/construct_d0_projection_checkpoints.sage

Each command compares the newly derived object with the distributed checkpoint before replacing it. The R4, H, A, and B checks require exact equality and print a RECOMPUTED_MATCHED marker. The historical R1 checkpoint differs from the freshly computed resultant by a nonzero rational scalar. Because the consumer immediately applies .monic() to R1 and R4, the R1 hook checks exact equality up to that scalar, verifies equality of the monic representatives, and prints R1_RECOMPUTED_MATCHED_UP_TO_SCALAR scale=.... This normalization does not change the gcd, radical, factorization, or any theorem branch.

This path can take hours and is not needed to check the finite identities, but it prevents a cold-provenance audit from silently short-circuiting at H, A, B, R1, or R4.

Scope

The theorem proved in the manuscript excludes both exact Proposition 4.3 Newton configurations. Combining it with the explicitly pinned external preprint reduction gives max(deg(P),deg(Q)) >= 125 for a hypothetical characteristic-zero plane Jacobian counterexample. The work does not prove the plane Jacobian conjecture and does not exclude degree 125 or larger.