diff --git a/research/f9-character-audit/CLAIM.md b/research/f9-character-audit/CLAIM.md new file mode 100644 index 0000000000..854334ccbe --- /dev/null +++ b/research/f9-character-audit/CLAIM.md @@ -0,0 +1,49 @@ +# Local sprint claim + +- Track: independent verification (OS assignment seed **83**, drawn with + `secrets.randbelow(100)` on 2026-10-25 at session start). +- Base: `32890bc5de034ab8fc93ac88ead7279a6a416d04`, canonical main fetched + from CrocSwap; initial preloaded `66849e1` was historical and not used. +- Scope: independently check PR5459's automorphism determinant character + over F9, particularly nonlinear terms, unequal heights, and scalar-field + conventions. Source head: `bef3575ddb19c44434a7e2460a353eac7c4d9387`. +- Method: new exact quotient-algebra implementation, direct determinants, + division-free determinant checks and restriction-of-scalars norm checks. + No predecessor executable imports. +- Domain: all 72 automorphisms of F9[x]/x^3; every F9[x]/x^9 substitution + with at most two nonlinear monomials; all flag-preserving linear maps, + single-monomial nonlinear tails, and 83 seed-83 dense nonlinear maps on + F9[x,y]/(x^3,y^9). Stop at this fixed domain, including failure controls. +- Deliverable: exact deterministic receipt, scope/proof note, source pins, + standalone and registered replay, committed branch and publication kit. +- Finish: 2026-10-25 13:40 UTC; final ten minutes reserved for verification + and handoff. + +## Selection and overlap + +Three candidates: independent signed-invoice order check; neutral-completion +bookkeeping; extension-field automorphism character. The first already has +an exhaustive independent discrete-slope test; the second has the primary +eight-engine and PR5414 companion coverage. The third offers distinct coverage: +PR5459's scientific checker supports only F2, F3, F4, F5, F7. Seed 83 selects +odd characteristic 3 and 83 deterministic dense samples in addition to exact +finite censuses. Increasing field size alone is not the claimed contribution: +the F3 norm oracle and semilinearity rejection control test distinct obligations. + +Read the selected certificate, promotion, scientific review and current status: +selected kappa is 605457647/200000000000, conditional on the five retained +framework assumptions. No selected construction or upstream source is changed. +PR ledger lists #5252 and #5316 as partially reviewed; #5459 has no entry at +this base. Its theorem is pending, not accepted because its PR is open. + +At 13:05-13:07 UTC, checked 100 recently updated open PRs, all-state searches +for Frobenius/determinant and F9/determinant, discussion search for Frobenius, +and the latest 20 handoff comments. PR5540 addresses tensor recognition over +prime fields; that is a separate task. PR5459 already includes F4 tests, so +those are not repeated. Search coverage is bounded, not a novelty theorem. +GitHub GraphQL returned no pinned issues. This local claim follows the donor's +fallback; no new reservation issue or unsolicited Discussion post was made. + +Credit Ali Romman (#5459/#5316), Nick Petalas (#5252), David Ganz and the +classical local-algebra/character theory they cite. Prepared for Charan / +theon199 with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/f9-character-audit/README.md b/research/f9-character-audit/README.md new file mode 100644 index 0000000000..811a3ba41e --- /dev/null +++ b/research/f9-character-audit/README.md @@ -0,0 +1,147 @@ +# Independent F9 automorphism-character audit + +The finite audit corroborates PR5459's determinant character on **12,315 +substitutions over F9**, adding an odd-characteristic extension field absent +from its checker. It also supplies an explicit control showing that a +restriction-of-scalars determinant alone can accept a wrong F9 determinant. +No discrepancy was found in the tested character formula. No new kappa, +supplier, full theorem proof or independent human acceptance is claimed. + +The exact statement under test is, for +`A = F9[x_i]/(x_i^(3^e_i))`, `N = dim_F9 A`, and a valid substitution with +invertible height-preserving tangent blocks `L_e`, + +``` +det_F9(sigma) = product_e det(L_e)^(N (3^e - 1)/2). +``` + +Source: Ali Romman's [PR5459](https://github.com/CrocSwap/integer-mult-bounds/pull/5459), +head `bef3575ddb19c44434a7e2460a353eac7c4d9387`. Its theorem is pending, and its +checker covers F2, F3, F4, F5 and F7. The byte-exact source proof and checker +are retained in `source/`, with API Git blob IDs and SHA256 in +[REFERENCE.json](REFERENCE.json). They are authenticated but **never executed +or imported**. The F4 domains are not repeated. The new field, quotient algebra, +substitution evaluator and three determinant checks are separately written. +Classical methods and the mathematical formula remain credited source work. + +## Exact finite domain and result + +Let `K = F3[i]/(i^2+1)`. Elements are encoded as `a+3b` for `a+b*i`. + +| Algebra/domain | Completed maps | Observed determinant image | +| --- | ---: | --- | +| K[x]/x^3, every automorphism `x -> ax+bx^2`, a nonzero | 72 | all eight nonzero elements, nine each | +| K[x]/x^9, every nonzero linear coefficient and at most two nonzero nonlinear monomials | 11,208 | +1 and -1, 5,604 each | +| K[x,y]/(x^3,y^9), every height-preserving invertible linear map | 576 | all eight nonzero elements, 72 each | +| Same mixed algebra, identity tangent and exactly one admissible nonlinear monomial in one generator | 376 | 1 | +| Same mixed algebra, 83 seed-83 dense nonlinear samples | 83 | all eight nonzero elements | + +For the second row the exact count is +`8 * (1 + 7*8 + binom(7,2)*8^2) = 11208`; it is **not** the full nonlinear +automorphism group. The mixed linear maps are `x -> ax`, `y -> bx+cy`, +with a,c nonzero and b arbitrary. There are 23 admissible nonlinear monomials +for x and 24 for y, giving `(23+24)*8 = 376` one-tail maps. The 83 dense +samples are a deterministic bounded sample, not exhaustive coverage. Classes +can overlap across rows; counts describe checked presentations, not the +number of distinct maps across their union. The stopping rule is completion +of precisely these five domains and controls, with no adaptive search. + +All 12,315 maps pass defining-power relations, unit preservation, every +generator-times-basis product (156,978 checks), invertibility via nonzero +determinant and the stated character. The 11,280 one-variable matrices also +pass a division-free Leibniz subset determinant, independently of Gaussian +elimination. Simultaneous seeded row/column permutations avoid relying on +already triangular input matrices. All 72 cutoff-three maps, the eight +linear cutoff-nine maps and 83 dense mixed maps pass an independent F3 +restriction-of-scalars determinant, for **163 norm checks**. + +Every scientific output field, including the domain counts, spectra, +control list and streamed case digest, is compared with [RESULT.json](RESULT.json). +The digest binds the ordered presentations and their determinants; it is +not a proof of the general theorem or a replacement for rerunning the checks. + +## Why the norm check is not enough + +For `z=a+b*i`, multiplication on the F3 basis `(1,i)` is +`[[a,-b],[b,a]]`, so `Norm(z)=a^2+b^2`. Block replacement gives +`det_F3 Res(M) = Norm(det_F9 M)`. This standard identity supplies a second +arithmetic path through ordinary modular F3 elimination, independent of +the extension-field operation tables. It loses information: `Norm(i)=1` +although `i != 1`. In particular the cutoff-nine character image is +`{+1,-1}`, but the incorrect extra value `i` has the same norm as 1. +The executable control demonstrates this ambiguity. Exact F9 determinants +are retained; no norm-only acceptance claim is made. + +Nine semantic controls cover forbidden upward height mixing, a nonlinear +tail that violates x^3=0 despite an invertible tangent, singular tangent, +a corrupted substitution column, confusing p-Frobenius with a K-linear map, +using q instead of p in the exponent, norm-only false positives, Z/9 in +place of F9, and an off-by-one character exponent. Some are explicit +counterexamples to a shortcut, others are rejected mutated inputs; none +is presented as a counterexample to PR5459. The p-Frobenius control uses +`(1+i)^3 != (1+i)*1^3`, while q-Frobenius fixes K. + +The generator-times-basis checks, unit and defining relations bind all +monomial products by induction: repeatedly multiply by each generator, +using the checked transition at each step, and use the defining zero +products on crossing a cutoff. Linearity then extends to arbitrary inputs +for each checked finite substitution. This does not enumerate every possible +substitution or prove the all-field character theorem by testing. + +## Reproduce + +Python 3.12, standard library only, no network or Git needed by the checker: + +```sh +python3 -W error -B research/f9-character-audit/verify.py +``` + +Expected: `PASS_F9_CHARACTER_AUDIT` with 12,315 maps, 156,978 products, +11,280 division-free determinants, 163 norm checks and nine controls. +The registered command runs normal and optimized modes: + +```sh +python3 -B scripts/research_package.py --package research/f9-character-audit +``` + +`--emit` on the standalone checker prints the freshly computed JSON for +review; normal replay compares it with the committed receipt. Source hashes +are checked before any scientific work in either mode. See +[VALIDATION.md](VALIDATION.md) for executed checks and environments. + +## Scope, sources and next questions + +Base: `32890bc5de034ab8fc93ac88ead7279a6a416d04`; assignment and overlap +coverage are in [CLAIM.md](CLAIM.md). The selected conditional saving at +that base is 0.003027288235 (#5413), with its five inherited assumptions. +This algebraic side result does not reduce those assumptions. It does not +verify unit/autotopism characters, full three-factor stabilizer images, +orbit recognition, general equal-height blocks, arbitrary extension fields, +physical costs, compiler admission or a full multiplication theorem. +The pending source bytes are shipped locally so a clean checkout does not +depend on an unmerged Git object. The two main-branch predecessor proofs +are provenance, not imported runtime dependencies. + +## Open next questions + +These are also structured in TASK.json. + +- Audit nontrivial equal-height tangent blocks over an odd extension field. + They test determinant block coupling missing here. Start with F9[x,y]/(x^3,y^3) + and a bounded set of genuinely mixed GL2 blocks; full nonlinear enumeration + grows rapidly and needs a separate budget. +- Audit the full covariant autotopism determinant image over an extension + field, retaining inverse-input conventions. Start with explicit unit maps + and F9[x]/x^3. The normalization theorem and completeness of the image + require their own proof review; this automorphism audit does not supply it. + +## Attribution + +Ali Romman: PR5459's height-flag formula and PR5316's univariate result. +Nick Petalas: PR5252's normalization and determinant-image interface. +David Ganz: the atlas character-equation framework. Local-algebra +filtrations, finite-field norms and determinant algorithms are classical. +Their notices remain in the retained source files. New independent audit, +norm-ambiguity control and packaging prepared for Charan / theon199 with +substantial OpenAI Codex assistance. No subagents or human review claimed. +New work is Apache-2.0, as is the repository and retained source. diff --git a/research/f9-character-audit/REFERENCE.json b/research/f9-character-audit/REFERENCE.json new file mode 100644 index 0000000000..be41a13363 --- /dev/null +++ b/research/f9-character-audit/REFERENCE.json @@ -0,0 +1,19 @@ +{ + "source_repository": "aliromman/integer-mult-bounds", + "source_pr": 5459, + "source_head": "bef3575ddb19c44434a7e2460a353eac7c4d9387", + "files": [ + { + "local_path": "source/PR5459-README.md", + "path": "research/frobenius-tensor-characters/README.md", + "git_blob": "b62f9a906e6ed49605684cca52a221f064924461", + "sha256": "31573ba91ac69caff5b8e5a42ce7fd0d80a6d54673c08d7f225c9ee08e0e0893" + }, + { + "local_path": "source/PR5459-verify.py.txt", + "path": "research/frobenius-tensor-characters/verify.py", + "git_blob": "4d0edc29d6a0c859f40148ee0fe87a05147f16c9", + "sha256": "2e80a73f0990a83396485899e8d03fa9f8b6549ec189e5be93aa2d46a3edf68a" + } + ] +} diff --git a/research/f9-character-audit/RESULT.json b/research/f9-character-audit/RESULT.json new file mode 100644 index 0000000000..f9e78614c3 --- /dev/null +++ b/research/f9-character-audit/RESULT.json @@ -0,0 +1,78 @@ +{ + "coverage": { + "cutoff3_complete": 72, + "cutoff9_two_tail": 11208, + "mixed_dense_seed83": 83, + "mixed_linear_complete": 576, + "mixed_single_tail_complete": 376 + }, + "determinant_spectra": { + "cutoff3_complete": { + "1": 9, + "2": 9, + "3": 9, + "4": 9, + "5": 9, + "6": 9, + "7": 9, + "8": 9 + }, + "cutoff9_two_tail": { + "1": 5604, + "2": 5604 + }, + "mixed_dense_seed83": { + "1": 10, + "2": 10, + "3": 11, + "4": 15, + "5": 8, + "6": 10, + "7": 11, + "8": 8 + }, + "mixed_linear_complete": { + "1": 72, + "2": 72, + "3": 72, + "4": 72, + "5": 72, + "6": 72, + "7": 72, + "8": 72 + }, + "mixed_single_tail_complete": { + "1": 376 + } + }, + "division_free_determinants": 11280, + "field": "F3[i]/(i^2+1); a+3b encodes a+b*i", + "generator_basis_products": 156978, + "negative_controls": [ + "forbidden_linear_height", + "invalid_nonlinear_tail", + "singular_tangent", + "corrupted_substitution_column", + "semilinear_p_frobenius", + "wrong_characteristic_exponent", + "norm_only_false_positive", + "integer_mod9_is_not_a_field", + "off_by_one_character_exponent" + ], + "norm_ambiguity_witness": { + "actual_determinant": 1, + "actual_norm": 1, + "algebra": "F9[x]/x^9", + "counterfeit_determinant": 3, + "counterfeit_norm": 1, + "exact_character_rejects_counterfeit": true, + "map": "identity" + }, + "restriction_of_scalars_determinants": 163, + "schema": "f9-character-audit/v1", + "scope": "Finite independent corroboration of automorphism characters; no new kappa or full theorem proof.", + "seed": 83, + "source_head": "bef3575ddb19c44434a7e2460a353eac7c4d9387", + "substitution_maps": 12315, + "transcript_sha256": "a638540ca188e30c9c4c2a03da0b989f707bd7abecbbd6fe0ce604a73b398c36" +} diff --git a/research/f9-character-audit/SOURCES.json b/research/f9-character-audit/SOURCES.json new file mode 100644 index 0000000000..f69ee8e574 --- /dev/null +++ b/research/f9-character-audit/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/etale-tensor-determinant-image/README.md", + "usage": "provenance", + "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208", + "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba" + }, + { + "path": "research/truncated-tensor-characters/README.md", + "usage": "provenance", + "git_blob": "9dac5ac07eb867ff2ff44bd8f033d0ac1114fb82", + "sha256": "2ebd7660dc342ea7a20c3c67dd58530b8ebf3d224ca13c5f689956338d3a32d7" + } + ] +} diff --git a/research/f9-character-audit/TASK.json b/research/f9-character-audit/TASK.json new file mode 100644 index 0000000000..f39b922fad --- /dev/null +++ b/research/f9-character-audit/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Independent finite F9 audit of PR5459 automorphism determinant characters, with a restriction-of-scalars norm cross-check.", + "scope_change_reason": "The donor explicitly assigned independent verification or formalization by OS seed 83. This is a finite algebraic side audit, not the catalogue card's formal-kernel interface proof; that acceptance gate is not claimed met.", + "bottleneck_link": "Algebraic side result: checks a determinant-character interface used in tensor orbit work. It does not alter a paid supplier or close a selected multiplication assumption.", + "budget_minutes": 40, + "stop_rule": "Complete precisely the five finite domains in README and nine semantic controls; stop without extending the search or claiming a general theorem.", + "outcome": "completed", + "evidence": "RESULT.json, README.md, VALIDATION.md", + "author": "Charan / theon199, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for source review, independent implementation, evidence and packaging. No subagents; no independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Audit nontrivial equal-height tangent blocks over F9.", + "why_it_matters": "This audit has only one-dimensional height blocks.", + "first_step": "Test genuinely mixed GL2 blocks on F9[x,y]/(x^3,y^3) with exact independent determinants.", + "blocked_by": "Full nonlinear enumeration requires a separately bounded domain and budget." + }, + { + "question": "Audit full covariant autotopism determinant images over F9.", + "why_it_matters": "Automorphism determinants alone do not verify the inverse-input triple or its completeness.", + "first_step": "Construct explicit unit maps and autotopisms on F9[x]/x^3.", + "blocked_by": "Retain and review the normalization theorem separately." + } + ], + "assignment_seed": 83 +} diff --git a/research/f9-character-audit/VALIDATION.md b/research/f9-character-audit/VALIDATION.md new file mode 100644 index 0000000000..608bd604af --- /dev/null +++ b/research/f9-character-audit/VALIDATION.md @@ -0,0 +1,51 @@ +# Validation receipt + +Environment: CPython 3.12.14, Linux x86_64, glibc 2.41; standard library only. +Canonical base: `32890bc5de034ab8fc93ac88ead7279a6a416d04`. +Scientific source: PR5459 `bef3575ddb19c44434a7e2460a353eac7c4d9387`. +This is local independent finite verification, not hosted CI or human review. + +Completed: + +- `python3 -B scripts/research_package.py --package research/f9-character-audit --check-only`: + metadata and main-branch provenance pins pass. +- `python3 -B scripts/research_package.py --package research/f9-character-audit`: + normal and `-O` warning-strict commands pass, each with all 12,315 maps, + 156,978 generator products, 11,280 division-free determinant comparisons, + 163 norm comparisons and nine controls. Every field agrees with RESULT.json. +- The standalone computation takes approximately six seconds locally. This + is a runtime observation, not a performance comparison or speedup claim. +- Retained PR5459 proof/checker bytes match their GitHub API Git blob IDs + and recorded SHA256 hashes. Scientific code never imports them. + +Additional completed checks: + +- `scripts/check_research_commit.py --package research/f9-character-audit + --check-source-history`: all 11 package files match committed bytes; the + sole declared history commit is the canonical base and is an ancestor. + PR5459's pending head is independently identified in REFERENCE.json and its + exact consumed bytes are shipped, not required as a Git-history object. +- `scripts/export_research_package.py export` and `check`: a committed + 11-file package export passes the integrity inventory. The source copy, + local reference manifest and frozen result are included. +- A relocated export in a path containing spaces passes `python -I -O -B` + with empty PATH, no Git checkout and read-only files. All 12 exported files + (11 package files plus export receipt) retain their SHA256 values afterward. +- Separate disposable copies reject (1) an altered source proof before + scientific execution and (2) a changed expected map count after replay, + both under optimized Python. These complement the nine mathematical + controls; they are not additional theorem cases. +- `git diff --check` passes. Final canonical-main refresh remains the exact + base above, and PR5459 remains at the pinned head. A renewed all-state + F9/character PR search found no overlapping audit; this is bounded search + coverage, not a novelty theorem. + +The export and corruption controls do not import predecessor executables. +Only this validation prose was completed after the first committed export; +scientific code, sources and RESULT.json remain byte-identical. The final +handoff records the exact publication commit, patch and export integrity. + +The selected cold replay, unrelated historical suites, full-source theorem +proofs and hosted CI are not required or run for this isolated audit. Selected +sources, upstream/ and predecessors stay unchanged. See the separate handoff +for publication status; a successful push or CI job is not mathematical adoption. diff --git a/research/f9-character-audit/VERIFY.json b/research/f9-character-audit/VERIFY.json new file mode 100644 index 0000000000..d64afedea5 --- /dev/null +++ b/research/f9-character-audit/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent F9 finite character audit, source binding and nine semantic controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete receipt and controls with Python assertions disabled." + } + ] +} diff --git a/research/f9-character-audit/source/PR5459-README.md b/research/f9-character-audit/source/PR5459-README.md new file mode 100644 index 0000000000..b62f9a906e --- /dev/null +++ b/research/f9-character-audit/source/PR5459-README.md @@ -0,0 +1,160 @@ +# Determinant characters for Frobenius-truncated local algebras + +This package extends the promised tensor class in PR5316 to multivariable local +algebras with unequal characteristic-power cutoffs. It derives the full +stabilizer determinant image and the resulting special-linear orbit count. +It is an algebraic interface result. The complete kappa calculation is unchanged. + +## The algebra and character formula + +Let K=F_q have characteristic p. Choose r>=1 integers e_i>=1, set n_i=p^e_i, +and let + +``` +A = K[x_1,...,x_r] / (x_i^n_i for every i), +N = product_i n_i, +E_i = N (n_i-1) / 2, +h = gcd(q-1,E_1,...,E_r). +``` + +Each E_i is an integer. Let mu in A* tensor A* tensor A be multiplication, +with the ordinary covariant action on its three tensor factors. Then + +``` +Delta(mu) = {(u,v,w) in (K*)^3 : (u v w)^((q-1)/h) = 1}. +``` + +The image has (q-1)^3/h elements. The one GL orbit splits into exactly h +orbits under the product of the three special linear groups. These statements +hold after independent changes of basis in all three tensor factors. +They assume the tensor belongs to this algebra's GL orbit. They do not +recognize that orbit or produce a transporter. + +For equal e_i=1 and odd p, h=(p-1)/2, independent of r and the extension degree +of K. For p=2 and e_i=1, h=1. Unequal or higher cutoffs can change the image: +over F4, the univariate cutoff four has h=3, whereas two cutoff-two variables +have h=1. Both algebras have dimension four, but their determinant images differ. + +## Automorphisms must preserve the height flag + +Write J for the radical. Every automorphism induces an invertible map L on J/J +squared. If the image of x_i has a nonzero linear x_j term, then e_j<=e_i. +Indeed the p^e_i power of that linear term gives a nonzero x_j^(p^e_i) term +when e_j>e_i. Frobenius removes mixed terms. Terms of degree at least two have +power degree at least 2p^e_i and cannot cancel that term. Thus L preserves the +flag given by the spans of variables of height at most e. + +Conversely, every invertible flag-preserving linear substitution respects all +relations: each allowed x_j has n_j dividing n_i. Its inverse preserves the same +flag and relations, so it is an algebra automorphism. More generally, a valid +substitution with invertible tangent map is an automorphism by the finite +radical filtration. Validity of the relations remains a separate condition; +an invertible tangent matrix alone does not authorize forbidden height mixing. + +An automorphism and its linear substitution induce the same map on the +associated graded algebra. Ordering monomials by total degree therefore shows +that they have equal determinants. Higher terms do not change the determinant. + +## Compute the automorphism and unit characters + +A diagonal change x_i -> c x_i has determinant c^E_i. The sum of the x_i +exponents over all N monomials is N(n_i-1)/2. An allowed elementary change +x_i -> x_i+c x_j has determinant one: order monomials by the x_i exponent; +every new term has a smaller exponent, and the diagonal stays one. The +flag-preserving linear group is generated by these elementary changes and +diagonal changes. Within an equal-height block, they generate its full GL group. +If L_e is the tangent block for height e, this proves + +``` +det(sigma) = product_e det(L_e)^(N(p^e-1)/2). +``` + +Independent diagonal scalings attain all products of these power subgroups. +Since K* is cyclic, the exact automorphism determinant image is H_h={c^h:c in K*}. +No determinant of a formal untwisted group algebra is used. + +For a unit a, multiplication by a is triangular on the radical filtration +with constant diagonal a_0. Thus det(L_a)=a_0^N. Since N is a power of p, +N is coprime to q-1, so these unit determinants fill K*. + +The classical unital commutative autotopism normalization, retained in PR5316 +and PR5252, writes every F(x)G(y)=H(xy) as + +``` +F=L_a sigma, G=L_b sigma, H=L_(ab) sigma. +``` + +For completeness, evaluate at 1 to get H(x)=F(x)b=aG(x), where a=F(1), b=G(1). +Bijectivity makes both multiplication maps bijective, hence a,b are units. +Then sigma=(ab)^-1 H is an algebra automorphism. The converse follows by +multiplication. The covariant tensor action uses (F^-T,G^-T,H). If x,y are the +unit determinants and z the automorphism determinant, its ordered triple is + +``` +(u,v,w) = (x^-1 z^-1, y^-1 z^-1, x y z). +``` + +The inverse equations x=vw, y=uw, z=(uvw)^-1 prove the displayed image formula. +Conjugation preserves determinants under independent basis changes. Finally, +the product SL group is the kernel of the determinant map from the product GL +group; its orbits in the fixed GL orbit are the cosets of Delta(mu). This proves +the image size and orbit count. + +The promised character equation can be computed without constructing A. To +compute E_i modulo m=q-1, multiply p^(sum e_i) and p^e_i-1 modulo 2m, then +halve the even residue. Use modular powers and gcd. This uses polynomially +many bit operations in the supplied parameter sizes and avoids constructing +the potentially huge integer N. The characteristic and algebra-class promise +are inputs; this calculation does not factor q or recognize a tensor. + +## Evidence and reproduction + +```sh +python3.12 -B scripts/research_package.py --package research/frobenius-tensor-characters +``` + +The standalone Python 3.12 checker uses its standard library. It implements F4 +as F2[t]/(t squared+t+1), as well as prime fields. It builds literal quotient +multiplication tables and substitution matrices, checks all defining power +relations, compares ambient determinants with the tangent-block formula, and +checks basis products. Three complete automorphism domains include nonlinear +substitutions and unequal heights. Additional bounded domains check elementary +linear and nonlinear maps through algebra dimension 49. Unit multiplication +matrices and the full determinant-triple sets are checked independently. + +Controls distinguish forbidden height mixing, equal dimensions with different +images, the inverse-input convention, and modular exponent extraction. Normal +and optimized checks use explicit exceptions. The written proof supplies the +general finite-field theorem; finite matrix checks are corroboration, not +proof-kernel verification. No predecessor executable is imported. + +## Sources and scope + +The direct handoff is [PR #5316](https://github.com/CrocSwap/integer-mult-bounds/pull/5316) +and its [pinned univariate proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/truncated-tensor-characters/README.md). +Nick Petalas's [PR #5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) +and [finite-etale proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/etale-tensor-determinant-image/README.md) +retain the normalization and inverse-input convention. David Ganz's atlas +retains the character-equation and tensor-action framework. Sources are pinned +as provenance in SOURCES.json. The all-state multivariable/determinant search +and full tracked-note/Discussion search found no same height-flag result; +unposted work and arbitrary historical diffs remain outside coverage. + +## Open next questions + +A next useful task is recognition of this promised algebra class from a +multiplication tensor, with a verified transporter. Start with its radical +filtration and recover the allowed height flag. A field factorization and +basis-recovery algorithm with complete correctness bounds is still missing. +Physical coefficient preparation, native realization, movement, precision and +supplier admission remain separate and unpriced. No selected cold replay, +Lean, Docker, independent human review or new multiplication theorem is claimed. + +## Credit + +Ali Romman's PR5316 supplies the univariate method and explicit multivariable +question. Nick Petalas (@petalas) supplies the finite-etale normalization and +nilpotent follow-up. David Ganz and the atlas sources retain their attribution. +Finite local-algebra filtrations, elementary generators and cyclic power +subgroups are classical. New proof and checks by Ali Romman with substantial +OpenAI Codex assistance; Apache-2.0. No general literature-priority claim is made. diff --git a/research/f9-character-audit/source/PR5459-verify.py.txt b/research/f9-character-audit/source/PR5459-verify.py.txt new file mode 100644 index 0000000000..4d0edc29d6 --- /dev/null +++ b/research/f9-character-audit/source/PR5459-verify.py.txt @@ -0,0 +1,214 @@ +#!/usr/bin/env python3 +"""Check determinant characters in exact finite local algebras. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from itertools import product +from math import gcd,prod +import json + + +def require(c,m): + if not c: raise ValueError(m) + + +class Field: + def __init__(self,q): + require(q in (2,3,4,5,7),'unsupported fixture field') + self.q=q; self.p=2 if q==4 else q + self.plus=[[a^b if q==4 else (a+b)%q for b in range(q)] for a in range(q)] + def multiply(a,b): + if q!=4: return a*b%q + c=0 + for _ in range(2): + if b&1: c^=a + b>>=1; a<<=1 + if a&4: a^=7 + return c + self.times=[[multiply(a,b) for b in range(q)] for a in range(q)] + def add(self,a,b): return self.plus[a][b] + def neg(self,a): return a if self.q==4 else -a%self.q + def mul(self,a,b): return self.times[a][b] + def power(self,a,n): + out=1 + while n: + if n&1: out=self.mul(out,a) + a=self.mul(a,a); n//=2 + return out + def inv(self,a): + require(a!=0,'zero inverse'); return self.power(a,self.q-2) + def det(self,A): + A=[list(r) for r in A]; out=1 + for k in range(len(A)): + pivot=next((i for i in range(k,len(A)) if A[i][k]),None) + if pivot is None: return 0 + if pivot!=k: A[k],A[pivot]=A[pivot],A[k]; out=self.neg(out) + out=self.mul(out,A[k][k]); iv=self.inv(A[k][k]) + for i in range(k+1,len(A)): + if A[i][k]: + factor=self.mul(A[i][k],iv) + for j in range(k+1,len(A)): + A[i][j]=self.add(A[i][j],self.neg(self.mul(factor,A[k][j]))) + return out + + +class Algebra: + def __init__(self,q,heights): + self.F=Field(q); self.heights=heights; self.r=len(heights) + self.cutoffs=[self.F.p**e for e in heights] + self.monomials=list(product(*(range(n) for n in self.cutoffs))) + self.N=len(self.monomials); self.index={m:i for i,m in enumerate(self.monomials)} + self.zero=(0,)*self.N; self.one=(1,)+(0,)*(self.N-1) + self.variables=[] + for i in range(self.r): + ex=[0]*self.r; ex[i]=1; v=[0]*self.N; v[self.index[tuple(ex)]]=1; self.variables.append(tuple(v)) + self.table=[] + for a in self.monomials: + row=[] + for b in self.monomials: + c=tuple(x+y for x,y in zip(a,b)); row.append(self.index.get(c,-1)) + self.table.append(row) + def add(self,a,b): return tuple(self.F.add(x,y) for x,y in zip(a,b)) + def scaled(self,c,a): return tuple(self.F.mul(c,x) for x in a) + def mul(self,a,b): + out=[0]*self.N + for i,x in enumerate(a): + if x: + for j,y in enumerate(b): + k=self.table[i][j] + if y and k>=0: out[k]=self.F.add(out[k],self.F.mul(x,y)) + return tuple(out) + def power(self,a,n): + out=self.one + while n: + if n&1: out=self.mul(out,a) + a=self.mul(a,a); n//=2 + return out + def tangent(self,images): + indices=[v.index(1) for v in self.variables] + return [[images[j][i] for j in range(self.r)] for i in indices] + def substitution(self,images): + powers=[] + for a,n in zip(images,self.cutoffs): + row=[self.one] + for _ in range(1,n): row.append(self.mul(row[-1],a)) + powers.append(row) + columns=[] + for monomial in self.monomials: + v=self.one + for i,e in enumerate(monomial): v=self.mul(v,powers[i][e]) + columns.append(v) + return columns + + +def image_index(p,q,heights): + m=q-1; modulus=2*m; N=pow(p,sum(heights),modulus); h=m + for e in heights: + residue=N*(pow(p,e,modulus)-1)%modulus + require(residue%2==0,'even exponent numerator') + h=gcd(h,residue//2) + return h + + +def verify_map(A,images,full): + F=A.F + require(all(a[0]==0 and A.power(a,n)==A.zero for a,n in zip(images,A.cutoffs)), 'invalid substitution relation') + L=A.tangent(images); require(F.det(L)!=0,'singular tangent') + for i,ei in enumerate(A.heights): + for j,ej in enumerate(A.heights): + require(ej<=ei or L[j][i]==0,'height flag violation') + predicted=1 + for e in set(A.heights): + ids=[i for i,h in enumerate(A.heights) if h==e] + block=[[L[i][j] for j in ids] for i in ids] + predicted=F.mul(predicted,F.power(F.det(block),A.N*(F.p**e-1)//2)) + columns=A.substitution(images); actual=F.det(list(zip(*columns))) + require(actual==predicted,'automorphism determinant character') + pairs=0 + indices=range(A.N) if full else [x.index(1) for x in A.variables] + for i in indices: + for j in range(A.N): + k=A.table[i][j]; expected=A.zero if k<0 else columns[k] + require(A.mul(columns[i],columns[j])==expected,'literal multiplication identity'); pairs+=1 + return actual,pairs + + +def main(): + maps=products=units=controls=0; contexts=[]; complete={} + for q,heights in [(4,(2,)),(4,(1,1)),(2,(1,2))]: + A=Algebra(q,heights); count=0; images_seen=set() + radical=[(0,)+v for v in product(range(q),repeat=A.N-1)] + for images in product(radical,repeat=A.r): + if not A.F.det(A.tangent(images)): continue + if any(A.power(a,n)!=A.zero for a,n in zip(images,A.cutoffs)): continue + value,checks=verify_map(A,images,True); images_seen.add(value); count+=1; maps+=1; products+=checks + predicted={A.F.power(c,image_index(A.F.p,q,heights)) for c in range(1,q)} + require(images_seen==predicted,'complete automorphism image') + expected={(4,(2,)):48,(4,(1,1)):2880,(2,(1,2)):2048}[(q,heights)] + require(count==expected,'complete substitution census') + complete[str((q,heights))]=count; contexts.append((q,heights)) + for q,heights in [(2,(1,1,1)),(3,(1,)),(3,(1,1)),(3,(1,1,1)),(5,(1,)),(5,(1,1)),(7,(1,)),(7,(1,1)),(4,(1,2))]: + A=Algebra(q,heights); images_seen=set(); candidates=[] + for i in range(A.r): + for c in range(1,q): + images=list(A.variables); images[i]=A.scaled(c,images[i]); candidates.append(images) + for j in range(A.r): + if i!=j and heights[j]<=heights[i]: + for c in range(1,q): + images=list(A.variables); images[i]=A.add(images[i],A.scaled(c,images[j])); candidates.append(images) + nonlinear=[] + for k,m in enumerate(A.monomials): + if sum(m)<2: continue + v=tuple(int(j==k) for j in range(A.N)) + if A.power(v,A.cutoffs[i])==A.zero: nonlinear.append(v) + for v in nonlinear[:3]: + images=list(A.variables); images[i]=A.add(images[i],v); candidates.append(images) + for images in candidates: + value,checks=verify_map(A,images,A.N<=9); images_seen.add(value); maps+=1; products+=checks + h=image_index(A.F.p,q,heights) + predicted={A.F.power(c,h) for c in range(1,q)} + # Independent diagonal scales attain the entire product subgroup. + attained={1} + for i in range(A.r): + values={A.F.power(c,A.N*(A.cutoffs[i]-1)//2) for c in range(1,q)} + attained={A.F.mul(x,y) for x in attained for y in values} + require(attained==predicted and images_seen<=predicted,'predicted determinant subgroup') + contexts.append((q,heights)) + triples=0 + for q,heights in contexts: + A=Algebra(q,heights); F=A.F; h=image_index(F.p,q,heights) + selected=[] + if A.N<=4: + selected=[v for v in product(range(q),repeat=A.N) if v[0]] + else: + for c in range(1,q): + for j in range(A.N): + v=[0]*A.N; v[0]=c + if j: v[j]=1 + selected.append(tuple(v)) + for u in selected: + columns=[A.mul(u,tuple(int(i==j) for i in range(A.N))) for j in range(A.N)] + require(F.det(list(zip(*columns)))==F.power(u[0],A.N),'unit determinant'); units+=1 + zs={F.power(c,h) for c in range(1,q)} + actual={(F.inv(F.mul(x,z)),F.inv(F.mul(y,z)),F.mul(F.mul(x,y),z)) + for x,y,z in product(range(1,q),range(1,q),zs)} + predicted={(u,v,w) for u,v,w in product(range(1,q),repeat=3) + if F.power(F.mul(F.mul(u,v),w),(q-1)//h)==1} + require(actual==predicted and len(actual)==(q-1)**3//h,'covariant determinant image'); triples+=len(actual) + A=Algebra(4,(1,2)); bad=list(A.variables); bad[0]=A.add(bad[0],bad[1]) + require(A.power(bad[0],2)!=A.zero,'forbidden height mixing'); controls+=1 + require(image_index(2,4,(2,))==3 and image_index(2,4,(1,1))==1,'height-sensitive image'); controls+=1 + F=Field(7); require(F.power(4,2)!=1 and F.power(F.mul(F.mul(4,1),2),2)==1,'inverse input convention'); controls+=1 + for p in (2,3,5,7): + for q in (p,p*p,p**3): + for heights in ((1,),(2,),(1,2),(2,3),(3,3)): + N=p**sum(heights); expected=q-1 + for e in heights: expected=gcd(expected,N*(p**e-1)//2) + require(image_index(p,q,heights)==expected,'modular exponent extraction'); controls+=1 + require(image_index(2,4,(10**100+1,10**90+2))==1,'large binary-encoded heights'); controls+=1 + print('PASS_FROBENIUS_TENSOR_CHARACTERS '+json.dumps(dict(contexts=len(contexts), + substitution_maps=maps,basis_product_checks=products,unit_maps=units, + determinant_triples=triples,controls=controls,complete_automorphism_domains=complete),sort_keys=True)) + + +if __name__=='__main__': main() diff --git a/research/f9-character-audit/verify.py b/research/f9-character-audit/verify.py new file mode 100644 index 0000000000..d0011c0a68 --- /dev/null +++ b/research/f9-character-audit/verify.py @@ -0,0 +1,333 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent finite audit of PR5459 over F3[i]/(i^2+1). + +Prepared for Charan / theon199 with substantial OpenAI Codex assistance. +No predecessor executable is imported. See README for finite coverage limits. +""" +from collections import Counter +from hashlib import sha1, sha256 +from itertools import combinations, product +import json +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +SEED = 83 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +# a+3b encodes a+b*i, i^2=-1, with a,b in F3. +ADD = [[(a % 3 + b % 3) % 3 + 3 * ((a // 3 + b // 3) % 3) + for b in range(9)] for a in range(9)] +MUL = [[((a % 3) * (b % 3) - (a // 3) * (b // 3)) % 3 + + 3 * (((a % 3) * (b // 3) + (a // 3) * (b % 3)) % 3) + for b in range(9)] for a in range(9)] +NEG = [(-(a % 3)) % 3 + 3 * (-(a // 3) % 3) for a in range(9)] +INV = [0] + [next(b for b in range(1, 9) if MUL[a][b] == 1) for a in range(1, 9)] + + +def power(a, n): + result = 1 + for _ in range(n): + result = MUL[result][a] + return result + + +def determinant(matrix): + """Eliminate over F9, retaining actual row operations and signs.""" + rows = [list(row) for row in matrix] + result = 1 + for j in range(len(rows)): + k = next((k for k in range(j, len(rows)) if rows[k][j]), None) + if k is None: + return 0 + if k != j: + rows[k], rows[j] = rows[j], rows[k] + result = NEG[result] + pivot = rows[j][j] + result = MUL[result][pivot] + for k in range(j + 1, len(rows)): + coefficient = MUL[rows[k][j]][INV[pivot]] + if coefficient: + rows[k] = [ADD[x][NEG[MUL[coefficient][y]]] + for x, y in zip(rows[k], rows[j])] + return result + + +def determinant_by_subsets(matrix): + """Division-free Leibniz sum, sharing partial column subsets (no pivots).""" + states = {0: 1} + for row in matrix: + following = {} + for mask, value in states.items(): + for j, entry in enumerate(row): + if entry and not (mask >> j & 1): + term = MUL[value][entry] + if (mask >> (j + 1)).bit_count() % 2: + term = NEG[term] + key = mask | (1 << j) + following[key] = ADD[following.get(key, 0)][term] + states = {key: value for key, value in following.items() if value} + return states.get((1 << len(matrix)) - 1, 0) + + +def prime_determinant(rows): + """Independent F3 elimination, with no F9 tables or inverse routine.""" + a = [list(row) for row in rows] + sign = 1 + for col in range(len(a)): + pivot = next((r for r in range(col, len(a)) if a[r][col] % 3), None) + if pivot is None: + return 0 + if pivot != col: + a[pivot], a[col] = a[col], a[pivot] + sign = -sign + value = a[col][col] % 3 + sign *= value + for r in range(col + 1, len(a)): + scale = a[r][col] * value % 3 + if scale: + for j in range(col, len(a)): + a[r][j] = (a[r][j] - scale * a[col][j]) % 3 + return sign % 3 + + +def restrict_scalars(matrix): + """Replace a+b*i by its multiplication matrix [[a,-b],[b,a]].""" + result = [[0] * (2 * len(matrix)) for _ in range(2 * len(matrix))] + for r, row in enumerate(matrix): + for c, value in enumerate(row): + a, b = value % 3, value // 3 + result[2*r][2*c:2*c+2] = [a, -b % 3] + result[2*r+1][2*c:2*c+2] = [b, a] + return result + + +class Quotient: + def __init__(self, cutoffs): + self.cutoffs = tuple(cutoffs) + self.basis = list(product(*(range(n) for n in cutoffs))) + self.index = {m: i for i, m in enumerate(self.basis)} + self.n = len(self.basis) + self.one = {(0,) * len(cutoffs): 1} + self.generators = [] + for j in range(len(cutoffs)): + m = tuple(int(i == j) for i in range(len(cutoffs))) + self.generators.append({m: 1}) + # Conjugate by a deterministic permutation to avoid testing only + # already-triangular matrices. The permutation has determinant square 1. + self.order = list(range(self.n)) + random.Random(SEED + self.n).shuffle(self.order) + + def multiply(self, left, right): + result = {} + for a, x in left.items(): + for b, y in right.items(): + m = tuple(i + j for i, j in zip(a, b)) + if all(e < n for e, n in zip(m, self.cutoffs)): + result[m] = ADD[result.get(m, 0)][MUL[x][y]] + return {m: c for m, c in result.items() if c} + + def pow(self, value, exponent): + result = self.one + for _ in range(exponent): + result = self.multiply(result, value) + return result + + def columns(self, images): + powers = [[self.pow(image, e) for e in range(n)] + for image, n in zip(images, self.cutoffs)] + columns = [] + for m in self.basis: + value = self.one + for j, e in enumerate(m): + value = self.multiply(value, powers[j][e]) + columns.append(value) + return columns + + def matrix(self, columns): + return [[columns[c].get(self.basis[r], 0) for c in self.order] + for r in self.order] + + def predicted(self, images): + # Each height block in these three contexts is one dimensional. + result = 1 + for image, generator, cutoff in zip(images, self.generators, self.cutoffs): + c = image.get(next(iter(generator)), 0) + require(c != 0, "singular tangent") + result = MUL[result][power(c, self.n * (cutoff - 1) // 2)] + return result + + def check_relations(self, images): + for image, cutoff in zip(images, self.cutoffs): + require(not self.pow(image, cutoff), "defining power relation") + + def check_products(self, images, columns): + checks = 0 + require(columns[0] == self.one, "unit image") + # Every generator times every basis monomial, including zero products. + for image, generator in zip(images, self.generators): + for j, monomial in enumerate(self.basis): + source = self.multiply(generator, {monomial: 1}) + expected = columns[self.index[next(iter(source))]] if source else {} + require(self.multiply(image, columns[j]) == expected, "generator product") + checks += 1 + return checks + + +def cases(): + for a, b in product(range(1, 9), range(9)): + yield "cutoff3_complete", (3,), [{(1,): a, **({(2,): b} if b else {})}], True + # All supports of size <=2 among nonlinear degrees 2..8; no duplicates. + for size in range(3): + for degrees in combinations(range(2, 9), size): + for coefficients in product(range(1, 9), repeat=size + 1): + image = {(1,): coefficients[0]} + image.update({(d,): c for d, c in zip(degrees, coefficients[1:])}) + yield "cutoff9_two_tail", (9,), [image], size == 0 + # All flag-preserving linear substitutions: x->a*x; y->b*x+c*y. + for a, b, c in product(range(1, 9), range(9), range(1, 9)): + yield "mixed_linear_complete", (3, 9), [{(1, 0): a}, + {(0, 1): c, **({(1, 0): b} if b else {})}], False + A = Quotient((3, 9)) + allowed = [[m for m in A.basis if sum(m) >= 2 and + not A.pow({m: 1}, cutoff)] for cutoff in A.cutoffs] + for variable, monomials in enumerate(allowed): + for m, c in product(monomials, range(1, 9)): + images = [dict(g) for g in A.generators] + images[variable][m] = c + yield "mixed_single_tail_complete", (3, 9), images, False + rng = random.Random(SEED) + for _ in range(SEED): + images = [{(1, 0): rng.randrange(1, 9)}, {(0, 1): rng.randrange(1, 9)}] + cross = rng.randrange(9) + if cross: + images[1][(1, 0)] = cross + for image, monomials in zip(images, allowed): + for m in monomials: + c = rng.randrange(9) + if c: + image[m] = c + yield "mixed_dense_seed83", (3, 9), images, True + + +def reject(call, diagnostic): + try: + call() + except ValueError as error: + require(diagnostic in str(error), "wrong failure: " + str(error)) + else: + raise ValueError("negative control accepted: " + diagnostic) + + +def source_checks(): + pins = json.loads((HERE / "REFERENCE.json").read_text()) + for row in pins["files"]: + raw = (HERE / row["local_path"]).read_bytes() + require(sha256(raw).hexdigest() == row["sha256"], "source SHA256") + require(sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + == row["git_blob"], "source Git blob") + return pins["source_head"] + + +def audit(): + source_head = source_checks() + for a, b, c in product(range(9), repeat=3): + require(MUL[a][ADD[b][c]] == ADD[MUL[a][b]][MUL[a][c]], "distributivity") + require(MUL[MUL[a][b]][c] == MUL[a][MUL[b][c]], "associativity") + for a in range(1, 9): + require(MUL[a][INV[a]] == 1, "field inverse") + require(power(4, 8) == 1 and power(4, 4) != 1, "primitive extension element") + contexts = {c: Quotient(c) for c in ((3,), (9,), (3, 9))} + counts, spectra = Counter(), {} + products_checked = subset_checks = norm_checks = 0 + transcript = sha256() + for label, cutoffs, images, norm_check in cases(): + A = contexts[cutoffs] + A.check_relations(images) + columns = A.columns(images) + products_checked += A.check_products(images, columns) + matrix = A.matrix(columns) + actual, expected = determinant(matrix), A.predicted(images) + require(actual == expected, "automorphism determinant character") + if A.n <= 9: + require(determinant_by_subsets(matrix) == actual, "Leibniz determinant") + subset_checks += 1 + if norm_check: + a, b = actual % 3, actual // 3 + require(prime_determinant(restrict_scalars(matrix)) == (a*a + b*b) % 3, + "restriction-of-scalars norm") + norm_checks += 1 + counts[label] += 1 + spectra.setdefault(label, Counter())[str(actual)] += 1 + transcript.update(json.dumps([label, [sorted(image.items()) for image in images], + actual], separators=(",", ":")).encode() + b"\n") + require(dict(counts) == {"cutoff3_complete": 72, "cutoff9_two_tail": 11208, + "mixed_linear_complete": 576, + "mixed_single_tail_complete": 376, "mixed_dense_seed83": 83}, + "domain coverage") + require(set(spectra["cutoff3_complete"]) == set(map(str, range(1, 9))), "cutoff3 image") + require(set(spectra["cutoff9_two_tail"]) == {"1", "2"}, "cutoff9 image") + require(set(spectra["mixed_linear_complete"]) == set(map(str, range(1, 9))), "mixed image") + A = contexts[(3, 9)] + controls = [] + for name, images in [ + ("forbidden_linear_height", [{(1, 0): 1, (0, 1): 1}, {(0, 1): 1}]), + ("invalid_nonlinear_tail", [{(1, 0): 1, (0, 2): 1}, {(0, 1): 1}]), + ]: + reject(lambda: A.check_relations(images), "defining power relation") + controls.append(name) + reject(lambda: A.predicted([{}, {(0, 1): 1}]), "singular tangent") + controls.append("singular_tangent") + columns = A.columns(A.generators) + columns[A.index[(1, 1)]] = {(1, 1): 2} + reject(lambda: A.check_products(A.generators, columns), "generator product") + controls.append("corrupted_substitution_column") + require(power(4, 3) != MUL[4][power(1, 3)], "p-Frobenius must fail K-linearity") + controls.append("semilinear_p_frobenius") + require(power(4, 3) != power(4, 12), "using q instead of p must change character") + controls.append("wrong_characteristic_exponent") + identity9 = contexts[(9,)].matrix(contexts[(9,)].columns(contexts[(9,)].generators)) + require(prime_determinant(restrict_scalars(identity9)) == 1 + and prime_determinant(restrict_scalars([[3]])) == 1, + "norm-only control must admit the counterfeit i") + reject(lambda: require(determinant(identity9) == 3, "counterfeit F9 determinant"), + "counterfeit F9 determinant") + controls.append("norm_only_false_positive") + require(all((3 * b) % 9 != 1 for b in range(9)), "Z/9 is not F9") + controls.append("integer_mod9_is_not_a_field") + reject(lambda: require(determinant(A.matrix(A.columns([{(1, 0): 4}, {(0, 1): 1}]))) + == power(4, 26), "mutated exponent"), "mutated exponent") + controls.append("off_by_one_character_exponent") + return {"schema": "f9-character-audit/v1", "source_head": source_head, + "seed": SEED, "field": "F3[i]/(i^2+1); a+3b encodes a+b*i", + "coverage": dict(counts), "substitution_maps": sum(counts.values()), + "generator_basis_products": products_checked, "division_free_determinants": subset_checks, + "restriction_of_scalars_determinants": norm_checks, + "norm_ambiguity_witness": {"algebra": "F9[x]/x^9", "map": "identity", + "actual_determinant": 1, "counterfeit_determinant": 3, + "actual_norm": 1, "counterfeit_norm": 1, + "exact_character_rejects_counterfeit": True}, + "determinant_spectra": {k: dict(sorted(v.items())) for k, v in spectra.items()}, + "transcript_sha256": transcript.hexdigest(), "negative_controls": controls, + "scope": "Finite independent corroboration of automorphism characters; no new kappa or full theorem proof."} + + +def main(): + result = audit() + if sys.argv[1:] == ["--emit"]: + print(json.dumps(result, indent=2, sort_keys=True)) + return + require(not sys.argv[1:], "usage: verify.py [--emit]") + require(result == json.loads((HERE / "RESULT.json").read_text()), "frozen result mismatch") + print("PASS_F9_CHARACTER_AUDIT " + json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()