DONE: formal integer retraction and monomial gluing bridge (PR1610)

[an664]

DONE (2026-10-14) - PR1610, head 985fd79ffea7ae7375fe6aa3ce9940b125c7dca2, from main 81e81af67714bdc8d1693b0bf5c29468b92f62ff. Claim complete and scope released.

The abstract bridge requested by PR1497 is now kernel-checked: integer identities MP=0, QP=I, I-PQ=WM imply integer row-image/kernel equality, an actual additive quotient isomorphism, lattice saturation and unique monomial reconstruction. Finite integer products and signed powers are defined and proved under the stated ordinary commutative-group laws.

The dedicated Lean 4.30.0 core/Std replay passes universal and positive-fixture compilation, all 197 queried declaration axiom reports, three intended negative controls, and ten tooling/arithmetic checks. The observed axiom dependencies are propext and Quot.sound. Signed nonzero-W, negative-power and torsion-group fixtures are included. The generic Python package hook passes but does not execute Lean; the package's dedicated replay.py performs that kernel replay with the pinned, already installed compiler. Exact commands, source hashes and full receipts are in the package.

This is conditional on the displayed matrix identities and group laws. No actual E8/P112/P120 matrix instance, field nonzero-element adapter, geometric generator/coverage bridge, numeric rank API, local Lemma 5, structural I2 theorem or complete multiplication theorem is formalized. No supplier or selected-frontier change. The next bounded step is a pinned numerical certificate instantiation together with its exact adapter and geometry obligations; the universal bridge alone does not discharge them. Hosted CI and maintainer review are separate from the local evidence.

The final complete overlap snapshot covered 733 open PRs and 244 Discussion records with no pagination warnings, followed by direct claim/source-head checks. No matching competing formal bridge was identified; this is not a novelty proof. Historical revision-2 selection/source provenance is retained alongside the revision-3 checkpoint.

Credit PR1497's written audit, Brett Halligan/@burntout76 and Ninefold (PR1212), DreamingOfClouds (PR717) and themilkman216 (PR968). Prepared by Andrey Mas with substantial GPT-6 Pro formalization and diagnostic-repair assistance through ChatGPT; Codex coordinated sources, audited execution, replayed and packaged. Apache-2.0. No independent human review is claimed.

Original claim and source history

CLAIM: kernel-check the abstract integer-retraction-to-monomial bridge from PR1497.

The open question in PR1497, head 7a1309f18f56d04c2db33bf1607e0332d19f72b3, asks for a proof-assistant check of the implication from integer identities MP=0, QP=I, I-PQ=WM to a free/saturated exponent quotient and global multiplicative reconstruction. This claim targets that abstract conditional implication, with explicit algebraic hypotheses and a precise report of which bridges are formalized.

Use the already installed Lean4.30.0 kernel and bundled core/Std; no Mathlib environment or toolchain installation is assumed. Expected result: a small standalone Lean source, reproducible isolated local compilation, theorem axiom report, meaningful negative controls, and clear assumptions. No sorry/admit, added axiom declarations, opaque external evaluation or unsupported claim of execution. Standard foundational kernel dependencies will be disclosed.

The numerical E8 geometry, actual P112/P120 matrix-certificate instantiation, zero exclusion, full rigidity, cost theorems, physical supplier and complete multiplication theorem remain outside this formal scope unless explicitly supplied and separately checked. A partial bridge will be labeled as such. This is an audit prerequisite under the original complex-mechanisms task, not a frontier improvement.

Main ef5f39403610d231a0c27e8a6b4f08c10209bcd6; priority revision2. Fresh overlap 02:12-02:13 UTC covered767 open PR bodies and198 Discussion records with complete pagination/no warnings. No matching active formal-gluing scope found. PR1309/1282 concern unitary prefix norms/partial stores; PR1494/1365 concern literal projector operators; PR1026 is a core/Std workflow precedent. They do not supply this theorem.

Credit Brett Halligan/@burntout76 and Ninefold (PR1212), retained PR717/968 lineage, and PR1497's GPT-6 Pro-assisted written audit. New Lean proof work will use substantial GPT-6 Pro assistance through ChatGPT; Codex handles source coordination, local compilation and packaging. Apache-2.0. No merge, closure or selected-frontier change.

Claim expires: 2026-10-14T04:14:36+00:00.

[an664]

DONE / reservation released. Published PR1701, head 830a94bf25479adf0694407e88cc5d15a9359d69, instantiating the exact P112 integer matrices from PR1497 under the unchanged PR1610 definitions. The closed Lean certificate proves MP=0, QP=I_33 and I_104-PQ=WM for M288x104/P104x33/Q33x104/W104x288, then instantiates the existing quotient, saturation and monomial consequences with their remaining hypotheses.

The advertised full runner passes isolated Lean 4.30.0 core/Std: 40 positive units, 636 named axiom reports and the intended damaged-W rejection. Observed axiom union is propext, Quot.sound; no positive errors, warnings, sorryAx or extra axioms are accepted. Total runtime 53.657 seconds, successor 50.120 seconds, within unchanged limits and the outer descendant-process watchdog. Six registered package commands pass; six external pins and the full saved-certificate subobject binding are checked. The exact Pro repair and source hashes are preserved. No hosted-CI pass is claimed.

This is one finite certificate-to-bridge instance. Geometry and generator-to-relation coverage, field/nonzero-element adapters, numeric rank, P120, zero exclusion, local Lemma 5 and physical construction remain outside scope. Rank 71 remains metadata; monomial consequences retain the lawful-group and individual-row relation hypotheses. No new kappa or selected-frontier change.

Credit PR1497/1610 and their retained lineage: Brett Halligan/@burntout76 and Ninefold (PR1212), DreamingOfClouds (PR717), themilkman216 (PR968). Andrey Mas with substantial GPT-6 Pro mathematical/source development, diagnostic repair and separate original-source review through ChatGPT; Codex coordination, execution audit, local kernel replay and packaging, with no mathematical repair. Apache-2.0. Original claim/status history follows unchanged.

---

UPDATE - closeout verification; reservation extended through 2026-10-14T08:00:00Z. The exact GPT-6 Pro repair has passed isolated local Lean 4.30.0 replay: all 40 positive units and 636 named axiom reports were accepted, and the damaged-W negative fixture failed at its intended false equality. The separate Pro review of the original source is complete. Final packaging and verification are still ongoing; no complete-package acceptance is claimed here. This is the existing finite P112 scope, with no new research, scope expansion or selected-frontier change. Original claim and history follow unchanged.

---

CLAIM: one pinned P112 integer-retraction certificate in Lean.

Follow-up to the explicit PR1610 open interface: check the actual P112 M/P/Q/W data from PR1497, head 7a1309f18f56d04c2db33bf1607e0332d19f72b3, under the unchanged concrete integer definitions of PR1610, head 985fd79ffea7ae7375fe6aa3ce9940b125c7dca2.

Scope is exactly MP=0, QP=I, I-PQ=WM for M288x104, P104x33, Q33x104 and W104x288, then only those already-proved bridge consequences that actually instantiate. The historical canonical certificate is SHA256 102cb8ddda027286b010b6edfd80c2b1c201a24020dfe32b0caee0f2a827c57e; the complete P112 subobject has 1,524 stored entries. This is a finite source-to-theorem binding, not a new mathematical novelty claim.

Expected evidence: an exact Lean4.30.0 core/Std instance, source/value binding, isolated local replay with bounded resource limits, complete theorem axiom reports and a meaningful damaged-certificate control. Kernel cost is unmeasured; if no bounded compilation method succeeds, report the exact remaining obligation. No installation, sorry, added axioms or unchecked native evaluation.

Excluded: E8 geometry reconstruction or generator-to-relation coverage, field/Units adapter, numeric rank API, P120, zero exclusion, local Lemma5, physical supplier, kappa or selected-frontier change. Existing bridge and predecessor history stay intact.

Revision3 independent-verification/formal-interface-lemma, checkpoint main c24fb5e6537d19d79c62265e4a12781aef9309cb. Complete fresh metadata covered 595 open PRs at05:15:32UTC and295 Discussion records at05:16:58UTC, with no warnings; direct1527 is released and no matching active numerical-instance scope was found. This is not proof of novelty. The active Boolean finite-image, cut-rank and H6 audits concern different objects.

Credit PR1497/1610 and their retained lineage: Brett Halligan/@burntout76 and Ninefold (PR1212), DreamingOfClouds (PR717), themilkman216 (PR968). New proof/source work will use substantial GPT-6 Pro assistance through ChatGPT for Andrey Mas; Codex will coordinate sources, audit execution, replay and package. No independent human review is claimed.

Claim expires: 2026-10-14T07:20:00Z (advisory, nonexclusive).