Repository navigation
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This answers Nick Petalas's PR #6682 unequal-cutoff question: classify every unital K-linear automorphism of
K[x,y]/(x²,y³)over every finite field K. In basis(1,x,y,xy,y²,xy²), the complete normal form isHere
a,dare nonzero;beta=0unless characteristic 2 andc=0unless characteristic 3. Every other coefficient is free and every allowed lift is invertible. The order is(q-1)^2 q^6in characteristics 2 or 3, otherwise(q-1)^2 q^5. The full six-dimensional determinant isa^3 d^6, with exact image the cube subgroupH3. The proof derives the relations and complete graded blocks; this is a fixed(2,3)classification.Executable evidence is separately bounded:
90961ea96ee98b5b77102fbcf660fb5a01dbdfcaa96c74100c989f56ebc5513c. Actual decompressed map data, rather than gzip container bytes, determine equality.b6a3955e80d9b787d0109eec1776efdf95d6f48a, all four registered commands, 23-file byte/mode/source-history preflight, official export integrity and four read-only Git-free, empty-PATH cold commands pass. Final documentation commit25500a2d75b54fa44ed0d2156384d45cf27aa553 and the exact public head also pass all23committed byte/mode/history checks; final official export/input1 and four unchanged read-only cold commands pass.The external mutation harness initially failed to change pretty oracle JSON; the clean oracle correctly passed. Its preserved no-op attempt was corrected only in the harness, with explicit mutation preconditions. A precommit registered invocation correctly rejected the untracked map sidecar; the declaration was retained and replay passed after committing it. Neither was an engine failure.
VALIDATION.mdandRUN-RECORDS.jsonpreserve exact first clocks and these distinctions.Credit: Nick Petalas #6682/#6578/#5252; Ali Romman #5316/#5459; Armin Pourshafeie #5656/#5663; David Ganz and retained tensor-atlas lineage. Exact source pins, original headers and classical radical/filtration/determinant-method credit are retained. The pair
(2,3)is outside the prior same-characteristic-power family.No all-cutoff family, tensor recognition/stabilizer implementation, semilinear count, physical field preparation, caller saving, κ or frontier change is claimed. No merge; maintainer edits and auto-merge remain disabled. Hosted CI succeeded on original run
41724318493: 711 helper tests (24 skipped), all four registered package commands, both full-map comparisons and both staged/unstaged drift checks passed. Synthetic test commitd8e4eff58f61d128a18d2080e1ab5f4dd80efe42has the exact verified tree and expected main/PR parents; no actual merge occurred. The mode, source-history and export checks above were local. Public head:64e08a1b1a73f80c814f2a6954c693c26bebf358.Substantial OpenAI Codex assistance with separate AI primary/oracle implementations and static review; independent human or formal proof-kernel acceptance is unclaimed.