diff --git a/research/idempotent-factor-invariant/README.md b/research/idempotent-factor-invariant/README.md new file mode 100644 index 0000000000..48ce67bdc3 --- /dev/null +++ b/research/idempotent-factor-invariant/README.md @@ -0,0 +1,294 @@ +# A complete factor invariant for two idempotents + +**Written linear algebra lemma with exact finite corroboration; no new kappa.** +Prepared by the authorized automated research workflow with substantial +OpenAI Codex GPT-6.1 Sol assistance. Apache-2.0. Human and formal proof-kernel +review are unclaimed. + +This answers the sufficient higher-rank invariant question in +[codyw912's PR4735](https://github.com/CrocSwap/integer-mult-bounds/pull/4735) +at `4afbea22e79e19d1d65702eb4090d454ee39d967`. +Its rank-one proof already uses an extension lemma for an inclusion and an +observation map. Allowing their source to have dimension `r+s` gives a complete +invariant for **ordered idempotents of any ranks over any field**. This note +states that extension explicitly, supplies the precise realizability condition +and exact removable zero-space dimension, and checks the invariant against +direct matrix conjugation on complete small domains. + +The result is an algebraic state descriptor. It supplies no header count, +physical implementation, selected-caller binding, supplier admission or exponent +improvement. It does not claim a polynomial time canonical-form algorithm. + +## 1. Statement + +Let P,Q be idempotents on an n-dimensional vector space V over a field F, +with ranks r,s. They need not commute. Choose rank factorizations + +```text +P=XY, YX=I_r, Q=ZW, WZ=I_s. +``` + +Here X,Z are injective and Y,W are surjective. On U=F^r direct-sum F^s put + +```text +C=[X Z]: U -> V, D=[Y;W]: V -> U, +K=ker C, L=im D, +M=DC = [ I_r YZ ]. + [ WX I_s ] +``` + +K and L are **actual subspaces of U**, not just their dimensions. Let +g=diag(A,B), with A in GL_r(F), B in GL_s(F). Its action on the datum is + +```text +(K,L,M) -> (g^-1 K, g^-1 L, g^-1 M g). (1) +``` + +**Complete invariant.** Two ordered pairs are simultaneously conjugate if +and only if their fields, n,r,s agree and their triples (K,L,M) have the same +orbit under (1). Rank-factorization bases do not affect that orbit. + +**Realizability.** A triple of subspaces K,L of U and an endomorphism M of U +with diagonal blocks I_r,I_s is realizable in dimension n exactly when + +```text +K subset ker M, im M subset L, +n >= a+b-c, +a=(r+s)-dim K, b=dim L, c=rank M. (2) +``` + +**Exact active dimension.** The pair is conjugate to a pair on a space of +dimension + +```text +d_active = a+b-c (3) +``` + +direct-summed with two zero operators on dimension n-d_active. No larger +simultaneous zero direct summand can be removed. In particular + +```text +d_active <= r+s+min(r,s), (4) +``` + +and this bound is sharp over every field for every pair of nonnegative ranks. +For r=s it is the sharp bound 3r. Ambient n must still be retained in a +header-counting state: adding zero dimensions changes its header ensemble. + +## 2. Proof of completeness + +First consider arbitrary systems C:U->V, D:V->U and C':U->V', D':V'->U +with equal ambient dimensions and exactly equal data ker C=ker C', +im D=im D', and DC=D'C'=M. This is the extension argument of PR4735 with +no restriction on dim U. + +Let A0=im C and B0=ker D, and use primes for the other system. The map + +```text +f0(Cu)=C'u +``` + +is a well-defined isomorphism A0->A0', because the two C kernels agree. +It satisfies D'f0=D on A0. Consequently it maps A0 intersect B0 +isomorphically onto A0' intersect B0'. Since the D images and ambient +dimensions agree, dim B0=dim B0'. Extend this restriction to an isomorphism +fB:B0->B0'. The maps f0,fB agree on the intersection, so they combine to +an isomorphism on A0+B0 that still satisfies D'f=D. + +Choose a basis of a complement of im M in the common space L=im D. Choose +one lift of each basis vector in V and one in V'. These lifts complement +A0+B0 and A0'+B0', respectively, because D induces an isomorphism + +```text +V/(A0+B0) -> L/im M. +``` + +Mapping corresponding lifts extends f to an isomorphism V->V' with +fC=C' and D'f=D. This proves sufficiency for the system datum. Necessity +follows immediately from these two intertwining equations. + +Apply the system result to the displayed rank factorizations. If the data +agree, fX=X', fZ=Z', Y'f=Y, W'f=W; therefore + +```text +fP=fXY=X'Y=X'Y'f=P'f, fQ=Q'f. +``` + +Changing the image bases of P,Q gives C->Cg and D->g^-1D, exactly (1). +Conversely, conjugation of an ordered pair carries each image basis to an +image basis of the corresponding projector, giving such block changes of +basis. Thus equality of the orbit is both necessary and sufficient. No +commutation, orthogonality, invertibility of M or equal-rank assumption was +used. The proof also includes rank-zero factors with their empty spaces. + +## 3. Proof of realizability and the active-space formula + +For any system, K subset ker M and im M subset L are necessary. Moreover + +```text +dim(im C intersect ker D) = a-c, +dim ker D = n-b. +``` + +The intersection lies in ker D, so n>=a+b-c. Conversely take C to be the +quotient map U->U/K, followed by inclusion into the first a dimensions of V. +On im C define D(Cu)=Mu; this is well-defined by K subset ker M and has +image im M. Add b-c new independent directions whose D images are a basis +of a complement of im M in L, and send the remaining directions to zero. +Condition (2) is precisely the space needed for this construction. It has +the prescribed K,L,M. Splitting C into columns X,Z and D into rows Y,W, +the identity diagonal blocks of M give YX=I_r and WZ=I_s. Hence XY,ZW +are idempotents of ranks r,s. This proves (2) constructively. + +For an existing pair, let T be the sum of im C and the b-c lifts just +described. Then dim T=a+b-c and T intersect ker D=im C intersect ker D. +Choose Z0 complementary to that intersection in ker D. We obtain +V=T direct-sum Z0. Both projectors have image in im C subset T and kill +Z0, so this is the asserted simultaneous zero decomposition. Any zero +summand must lie in ker D and be disjoint from im C, so its dimension is at +most (n-b)-(a-c)=n-d_active. This also proves minimality in (3). + +Since a,b<=r+s and M has identity diagonal blocks, c>=max(r,s). This proves +(4). To attain it, use direct sums of the following rank-one pair: + +```text +P* = [1 1 0], Q* = [0 0 0]. + [0 0 0] [1 1 1] + [0 0 0] [0 0 0] +``` + +Over every field, a=b=2 and M is the 2-by-2 all-ones matrix of rank one; +therefore d_active=3. Take min(r,s) copies, and append |r-s| one-dimensional +blocks with (P,Q)=(1,0) or (0,1) to supply the excess rank. The dimension is +3 min(r,s)+|r-s|=r+s+min(r,s). Both-zero ranks give active dimension zero. + +The active formula can also be computed directly from the pair, without +choosing its factors: + +```text +a = rank [P Q], b = rank [P;Q], +c = rank [P PQ]. + [QP Q ] +``` + +For c, the displayed block matrix factors as diag(X,Z) M diag(Y,W), whose +outer maps are respectively injective and surjective, so its rank is rank M. +These formulas describe algebraic dimension; they assign no execution cost. + +## 4. Verification and boundaries + +The standard-library verifier imports no predecessor code or mathematical +inputs, writes no files, and uses explicit exceptions active under -O. Run + +```sh +python -B scripts/research_package.py --package research/idempotent-factor-invariant +``` + +The registered commands run both ordinary and optimized Python 3.12. A +Git-free package export can instead run `python -I -W error -O -B verify.py`. +The scientific marker is `PASS_IDEMPOTENT_FACTOR_INVARIANT`. + +Each census fixes P=diag(I_r,0), enumerates **every** second idempotent Q of +rank s, and compares two classifications. The direct matrix calculation +conjugates Q by GL_r x GL_(n-r), the full centralizer of P. The proposed +invariant acts on its factor data by GL_r x GL_s. Every direct class must have +one signature and every signature one direct class. This covers all ordered +pairs up to conjugacy because every first rank-r idempotent is conjugate to +that fixed P; it does not literally loop over every first P. + +| Field order | n | (r,s) | Second projectors | Direct classes | Direct/factor group orders | +|---:|---:|---:|---:|---:|---:| +| 2 | 4 | (2,2) | 560 | 30 | 36 / 36 | +| 2 | 4 | (1,2) | 560 | 8 | 168 / 6 | +| 2 | 3 | (1,2) | 28 | 7 | 6 / 6 | +| 2 | 3 | (1,1) | 28 | 7 | 6 / 1 | +| 3 | 3 | (1,1) | 117 | 8 | 96 / 4 | +| 3 | 2 | (1,1) | 12 | 7 | 4 / 4 | +| 4 | 2 | (1,1) | 20 | 8 | 9 / 9 | +| 5 | 2 | (1,1) | 30 | 9 | 16 / 16 | + +Every one of these 1,355 cases also reconstructs a pair from its abstract +datum, checks the factor identities, compares its orbit and independently +normalizes the reconstructed first projector to check direct conjugacy. The +coordinate-free block-rank formula for d_active is checked separately. Sixteen direct-sum +fixtures attain (4) at rank pairs (1,1),(2,2),(3,2),(2,3) over all four fields. +Eleven semantic controls distinguish dropping K, L, M or n, reject too-small +ambient dimensions, incompatible K/L/M, nonidempotence and invalid field +entries, and distinguish F4 from integer arithmetic modulo four. F4 is +F2[x]/(x^2+x+1). The universal statements rest on the written proofs, not these +finite samples. + +Observed local verification used CPython 3.12.10 on Windows. Metadata and both +registered ordinary/optimized commands passed. The first wrapper attempt passed +its scientific command but hit a sandbox TEMP cleanup permission error; setting +TEMP and TMP to a writable run-local directory allowed the complete unchanged +wrapper to pass. This is an environment limitation, not a scientific failure +or a portability repair in this package. + +The implementation enumerates small groups and bounded matrix domains. The +largest raw matrix domain is 2^16; it does not enumerate GL4 or GL5. It is +not an efficient general canonical form: enumeration remains exponential in +the ranks. No higher-rank transition probabilities, full-guard recurrence +values, header cover, physical reads, dirty restoration, precision/tape, +stock, dispatch or complete consumer bill is supplied. These obligations +remain unknown. No selected cold replay, Lean or Docker run is required by +this isolated algebraic package, and none is claimed. + +## 5. Sources, scope and attribution + +Canonical base is `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7, +selected conditional kappa 60403/20000000 (#4470). The task is a **changed** +formal-interface-lemma card, a written side result rather than a formal proof +or selected-caller binding. Current selected-baseline orientation was attempted +but stopped because the sparse checkout omits certificates/frontier4470/CLAIM.json; +no selected-baseline pass is claimed. The scientific verifier needs none of +the omitted inputs. The family decision is **narrow, then stop** after this +classification lemma and its corroboration. It justifies no construction +expansion from a positive count or an unpriced consumer. + +- **codyw912, PR4735**, `4afbea22e79e19d1d65702eb4090d454ee39d967`: the + sufficient binary rank-one invariant, inclusion/observation extension + argument and explicit higher-rank question. This proof generalizes that + argument; its mathematical idea retains this credit. Substantial GPT-6 + Astra assistance is disclosed in that predecessor. +- **Mihir Srivastava, PR4689**, `3a72fbad148294aa9ca7f900a48dbb10e64232be`: + seven residual states and finite full-guard counts, with Codex assistance. + Their numerical results are not reproduced or claimed here. The direct + centralizer calibration follows the image/kernel block method explained + in PR4735; the factor invariant does not depend on those seven states. +- **ssafwann, PR4678/PR4671**: one-block counts, sector criterion and the + earlier residual-state handoff; **Nick Petalas, PR4597 and its lineage**: + ordered Schur and header questions; **Ryanson Jonathan**: full-guard census; + **lee-phys**: binary dimension work; **Cinna Davis, PR4100**, and source527, + commdata2338, Jose Manuel: the earlier request/normalizer context. +- **Nick Petalas, PR4240**, `9f9c89ed75e9fdae6b6762925b080fb308824858`, + already proves the all-finite-field rank-one joint header law. The seven + binary terminal counts are not an uncovered counting theorem. That overlap + was found before starting this higher-rank task and is not republished as + a new result. + +SOURCES.json pins only canonical-main historical provenance. Exact pending +heads and README byte hashes are citations in TASK.json, not executable or +Git-history dependencies. No frozen archive or predecessor package changes. +Repository tooling retains its authors' attribution. No global mathematical +novelty or independent human acceptance is asserted. + +Submission overlap also found Nick Petalas's +[PR4746](https://github.com/CrocSwap/integer-mult-bounds/pull/4746), which +extends the initial commuting identity-pivot dimension theorem to arbitrary +fields. It studies a prescribed product compression and maximal Schur rank; +this note classifies arbitrary ordered, possibly noncommuting residual pairs. +No dimension-minimum or header-count number from that proposal is claimed here. + +## Open next questions + +1. Can this complete descriptor yield a useful higher-rank transition table + for one actual residual ensemble? The invariant controls state identity, + which is needed to avoid merging states with different continuations. + First compute split transitions for one fixed (n,r,s) and aggregate by the + descriptor, retaining multiplicities. Enumeration of the active group is + still exponential, and no transition cost or paid caller is supplied here. +2. Can actual odd-field requests use a fully charged header cover? This is + needed before any supplier consequence. First pin one producer and its + field, then price selection, emission, reads, dirty return and stock. + The algebraic descriptor supplies none of that implementation contract. diff --git a/research/idempotent-factor-invariant/SOURCES.json b/research/idempotent-factor-invariant/SOURCES.json new file mode 100644 index 0000000000..4916cee8e5 --- /dev/null +++ b/research/idempotent-factor-invariant/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ] +} diff --git a/research/idempotent-factor-invariant/TASK.json b/research/idempotent-factor-invariant/TASK.json new file mode 100644 index 0000000000..6d26f6c977 --- /dev/null +++ b/research/idempotent-factor-invariant/TASK.json @@ -0,0 +1,191 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "A complete GL_r x GL_s kernel/image/product orbit invariant for ordered idempotents of arbitrary ranks over any field; exact realizability and removable zero-summand dimension, with bounded direct conjugation corroboration.", + "scope_change_reason": "Complementary written algebraic answer to PR4735 Open next question 1, rather than a proof-assistant build or selected-caller binding. The tentative all-field terminal count was already covered by PR4240 and was discarded before this task.", + "bottleneck_link": "A state-aware Schur recursion needs sufficient invariants for noncommuting residuals. This resolves state identity algebraically; no transition count, executable header cover or complete physical bill follows.", + "budget_minutes": 60, + "stop_rule": "Stop after the stated invariant, realizability/active-space proof, scoped exact corroboration and packaging. No expansion into transition tables, selected replay or a supplier.", + "outcome": "partial", + "evidence": "Completed scoped result. On CPython 3.12.10 / Windows, package metadata and both registered ordinary/optimized replays passed. Exact direct/factor orbit agreement on 1,355 complete fixed-first-projector cases, 16 sharp direct-sum fixtures and 11 semantic controls. Abstract reconstruction also passes independent direct matrix conjugacy and block-rank active-size checks. Initial wrapper cleanup failed after scientific PASS with sandbox TEMP permissions; unchanged replay passed with run-local TEMP/TMP. External run logs preserve the observed checks; no selected cold replay, Lean, Docker, human or proof-kernel acceptance is claimed.", + "author": "Authorized automated research workflow", + "ai_assistance": "Substantial OpenAI Codex GPT-6.1 Sol / xhigh assistance in derivation, implementation and writing. The parent will request the separately authorized actual Astra / high brief check. Independent human and proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this descriptor aggregate a useful higher-rank split transition table for one actual residual ensemble?", + "why_it_matters": "A sufficient state identity prevents merging residuals with distinct continuations.", + "first_step": "Fix one (n,r,s), compute its split transitions, and aggregate by the descriptor while retaining multiplicities.", + "blocked_by": "Active-group enumeration remains exponential; no transition table or paid caller is supplied." + }, + { + "question": "Can actual odd-field requests use a fully paid header cover?", + "why_it_matters": "Algebraic classification alone yields no supplier consequence.", + "first_step": "Pin one producer and field, then price selection, emission, reads, dirty return and stock.", + "blocked_by": "The physical cover and complete consumer contract remain open." + } + ], + "family_expansion_decision": "Narrow, then stop. Algebraic classification only; no new construction expansion or paid-work saving is justified.", + "orientation": { + "command": "python -B scripts/research_selected_baseline.py", + "result": "FAIL_RESEARCH_BASELINE: Invalid selected file: certificates/frontier4470/CLAIM.json", + "reason": "Sparse omission; no baseline or scientific replay pass claimed." + }, + "selection": { + "nonce": "1c1723af6b9000d6e6596693d4d44a4f", + "track_override": "independent-verification", + "method": "Complementary written interface lemma, with explicitly changed card scope." + }, + "selected_result_unchanged": "60403/20000000 = 0.00302015 (#4470)", + "predecessor_credit": [ + "codyw912 PR4735: rank-one sufficient invariant and extension argument; explicitly generalized here. Substantial GPT-6 Astra assistance disclosed there.", + "Mihir Srivastava PR4689: seven residual states and full-guard counts; those counts are not new evidence here.", + "ssafwann PR4678/4671, Nick Petalas PR4597/4240 and preceding Schur/header work, Ryanson Jonathan, lee-phys, Cinna Davis and retained normalizer lineage." + ], + "overlap": { + "captured_at": "2026-10-22T19:10:07.274972+00:00", + "queries": [ + "invariant Schur", + "higher-rank invariant", + "rank factorization header", + "ker X im Y" + ], + "coverage": "Targeted GitHub REST search/issues across open and closed PR/Issue title/body matches; counts 10,5,1,5; incomplete_results=false. Relevant current source proofs and public newest handoffs read. Search snapshots are outside the package.", + "nearest": "PR4735 asks for a higher-rank sufficient invariant and proves only its rank-one version; this package generalizes its argument and gives realizability/active-space consequences. PR4240 already supplies terminal rank-one counting and is not repeated as new.", + "limits": [ + "No complete authenticated discussion snapshot yet", + "Sparse local notes: 5860 omitted", + "Arbitrary remote code diffs and unpublished work outside coverage", + "No global mathematical novelty claim" + ], + "final_captured_at": "2026-10-22T19:11:49.2071159+00:00", + "final_queries": [ + { + "query": "repo:CrocSwap/integer-mult-bounds \"higher-rank\" \"invariant\"", + "total": 5, + "incomplete_results": false + }, + { + "query": "repo:CrocSwap/integer-mult-bounds \"idempotent\" \"factor\" \"invariant\"", + "total": 9, + "incomplete_results": false + }, + { + "query": "repo:CrocSwap/integer-mult-bounds \"active dimension\"", + "total": 5, + "incomplete_results": false + }, + { + "query": "repo:CrocSwap/integer-mult-bounds \"30\" \"rank-two\"", + "total": 56, + "incomplete_results": false + } + ], + "new_relevant_match": "PR4746: all-field initial commuting identity-pivot dimension theorem; read current body, complementary to arbitrary noncommuting residual classification. No claimed numerical overlap.", + "canonical_refresh": "At 2026-10-22T19:11Z canonical main remained b58ad9ef4d4e861b0eaa5dba41742bdc072dca51 and PR4735 remained 4afbea22e79e19d1d65702eb4090d454ee39d967.", + "discussion_search": "Read public current board, #1163 and newest #1166, with relevant primary source links. Targeted search-engine Discussion queries yielded no reliable additional repository match. Authenticated complete discussion pagination unavailable; Astra must make a fresh targeted check before publication." + }, + "citations": [ + { + "pr": 4735, + "head": "4afbea22e79e19d1d65702eb4090d454ee39d967", + "path": "research/schur-invariant-transitions/README.md", + "sha256": "fccdd2bff1ee00c120796bb1b6c3739cce90dcffbff7c96e897300ed81bba72e", + "usage": "attributed citation only; no executable dependency" + }, + { + "pr": 4678, + "head": "af9cf805c501e4e9e947c98c0b97b2281b6b6e97", + "path": "research/schur-header-count/README.md", + "sha256": "472295f32ebf3fcdc8daa4137af63db70d9943de7cbb97e47ed272823b2a227e", + "usage": "attributed citation only; no executable dependency" + }, + { + "pr": 4671, + "head": "8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9", + "path": "research/identity-pivot-sector-bound/README.md", + "sha256": "c997446a1fc4683694987feea5f2a8423b57d48d5513a27e178f84ecf56ffc12", + "usage": "attributed citation only; no executable dependency" + }, + { + "pr": 4240, + "head": "9f9c89ed75e9fdae6b6762925b080fb308824858", + "path": "research/projector-pair-header-law/README.md", + "sha256": "49e2f01d95f856e366fd254320b78fa7e48dbad622b605fe2222b5755c403156", + "usage": "attributed citation only; no executable dependency" + } + ] +} diff --git a/research/idempotent-factor-invariant/VERIFY.json b/research/idempotent-factor-invariant/VERIFY.json new file mode 100644 index 0000000000..615fd2d425 --- /dev/null +++ b/research/idempotent-factor-invariant/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Direct centralizer classifications versus factor invariant, abstract realizability, sharp active dimension and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact checks with optimized Python; explicit exceptions remain active." + } + ] +} diff --git a/research/idempotent-factor-invariant/verify.py b/research/idempotent-factor-invariant/verify.py new file mode 100644 index 0000000000..c48079ea52 --- /dev/null +++ b/research/idempotent-factor-invariant/verify.py @@ -0,0 +1,331 @@ +#!/usr/bin/env python3 +"""Exact factor-invariant corroboration. GPT-6.1 Sol assistance; Apache-2.0. + +No predecessor code is imported. No files, subprocesses or network are used. +""" +from functools import lru_cache +from itertools import product +import json + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +class Field: + """Prime fields and F4=F2[x]/(x^2+x+1).""" + + def __init__(self, q): + require(q in (2, 3, 4, 5), "unsupported field") + self.q = q + if q == 4: + self.add = tuple(tuple(a ^ b for b in range(q)) for a in range(q)) + self.mul = tuple(tuple(self.four_mul(a, b) for b in range(q)) for a in range(q)) + self.neg = tuple(range(q)) + else: + self.add = tuple(tuple((a+b) % q for b in range(q)) for a in range(q)) + self.mul = tuple(tuple((a*b) % q for b in range(q)) for a in range(q)) + self.neg = tuple((-a) % q for a in range(q)) + self.inv = (0,) + tuple(next(b for b in range(1, q) if self.mul[a][b] == 1) + for a in range(1, q)) + + @staticmethod + def four_mul(a, b): + result = 0 + for bit in range(2): + if b & (1 << bit): + result ^= a << bit + return result ^ 7 if result & 4 else result + + +def eye(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def tr(a, width=None): + return tuple(zip(*a)) if a else tuple(() for _ in range(width or 0)) + + +def mm(a, b, f, width=None): + columns, result = tr(b, width), [] + for row in a: + out = [] + for col in columns: + require(len(row) == len(col), "product shape") + value = 0 + for x, y in zip(row, col): + value = f.add[value][f.mul[x][y]] + out.append(value) + result.append(tuple(out)) + return tuple(result) + + +def rref(a, width, f): + require(all(len(row) == width for row in a), "row width") + require(all(type(x) is int and 0 <= x < f.q for row in a for x in row), "field entry") + rows, pivots = [list(row) for row in a], [] + for col in range(width): + found = next((j for j in range(len(pivots), len(rows)) if rows[j][col]), None) + if found is None: + continue + i = len(pivots) + rows[i], rows[found] = rows[found], rows[i] + scale = f.inv[rows[i][col]] + rows[i] = [f.mul[scale][x] for x in rows[i]] + for j in range(len(rows)): + if j != i and rows[j][col]: + coeff = f.neg[rows[j][col]] + rows[j] = [f.add[x][f.mul[coeff][y]] for x, y in zip(rows[j], rows[i])] + pivots.append(col) + return tuple(tuple(row) for row in rows[:len(pivots)]), tuple(pivots) + + +def space(a, width, f): + return rref(a, width, f)[0] + + +def rank(a, width, f): + return len(space(a, width, f)) + + +def kernel(a, width, f): + reduced, pivots = rref(a, width, f) + vectors = [] + for j in range(width): + if j not in pivots: + vector = [int(i == j) for i in range(width)] + for i, pivot in enumerate(pivots): + vector[pivot] = f.neg[reduced[i][j]] + vectors.append(tuple(vector)) + return space(vectors, width, f) + + +def inverse(a, f): + n = len(a) + reduced, pivots = rref(tuple(row+unit for row, unit in zip(a, eye(n))), 2*n, f) + require(pivots == tuple(range(n)), "singular inverse") + return tuple(row[n:] for row in reduced) + + +def diag(a, b): + r, s = len(a), len(b) + return tuple(row+(0,)*s for row in a) + tuple((0,)*r+row for row in b) + + +@lru_cache(maxsize=None) +def gl(q, n): + require(n <= 3 and q**(n*n) <= 20000, "bounded GL domain") + f, values = Field(q), [] + for entries in product(range(q), repeat=n*n): + a = tuple(tuple(entries[i*n:(i+1)*n]) for i in range(n)) + if rank(a, n, f) == n: + values.append((a, inverse(a, f))) + return tuple(values) + + +@lru_cache(maxsize=None) +def group(q, r, s): + return tuple((diag(a, b), diag(ai, bi)) for a, ai in gl(q, r) for b, bi in gl(q, s)) + + +def factor(p, f): + n = len(p) + require(mm(p, p, f) == p, "not idempotent") + pivots = rref(p, n, f)[1] + x = tuple(tuple(row[j] for j in pivots) for row in p) + r = len(pivots) + if not r: + return x, () + selected = rref(tr(x), n, f)[1] + y = mm(inverse(tuple(x[i] for i in selected), f), tuple(p[i] for i in selected), f) + require(mm(x, y, f, n) == p and mm(y, x, f, r) == eye(r), "factor identities") + return x, y + + +def datum(p, q, f): + require(len(p) == len(q), "ambient mismatch") + x, y = factor(p, f) + z, w = factor(q, f) + r, s, n = len(y), len(w), len(p) + t = r+s + joined, stacked = tuple(a+b for a, b in zip(x, z)), y+w + m = mm(stacked, joined, f, t) + return n, r, s, kernel(joined, t, f), space(tr(stacked, n), t, f), m + + +def transformed(data, g, gi, f): + n, r, s, k, l, m = data + t = r+s + return (n, r, s, space(mm(k, tr(gi), f, t), t, f), + space(mm(l, tr(gi), f, t), t, f), mm(mm(gi, m, f), g, f)) + + +def signature(data, f): + return min(transformed(data, g, gi, f) for g, gi in group(f.q, data[1], data[2])) + + +def complement(initial, target, width, f): + basis, added = space(initial, width, f), [] + for vector in target: + candidate = space(basis+(vector,), width, f) + if len(candidate) > len(basis): + added.append(vector) + basis = candidate + return tuple(added) + + +def realize(data, f, ambient=None): + n, r, s, k, l, m = data + t = r+s + require(len(m) == t and all(len(row) == t for row in m), "product shape") + require(tuple(row[:r] for row in m[:r]) == eye(r), "first identity block") + require(tuple(row[r:] for row in m[r:]) == eye(s), "second identity block") + k, l = space(k, t, f), space(l, t, f) + require(not any(x for row in mm(m, tr(k, t), f) for x in row), "kernel not killed") + im = space(tr(m, t), t, f) + require(space(l+im, t, f) == l, "product image outside observation image") + a, b, c = t-len(k), len(l), len(im) + minimum = a+b-c + n = n if ambient is None else ambient + require(n >= minimum and n >= 1, "ambient below bound") + chosen = complement(k, eye(t), t, f) + quotient = inverse(tr(k+chosen, t), f)[len(k):] + lift = complement(im, l, t, f) + joined = quotient + ((0,)*t,)*(n-a) + columns = mm(m, tr(chosen, t), f, a) + stacked = tuple(row+tuple(v[i] for v in lift)+(0,)*(n-minimum) + for i, row in enumerate(columns)) + require(mm(stacked, joined, f, t) == m, "constructed product") + require(kernel(joined, t, f) == k, "constructed kernel") + require(space(tr(stacked, n), t, f) == l, "constructed observation image") + p = mm(tuple(row[:r] for row in joined), stacked[:r], f, n) + q = mm(tuple(row[r:] for row in joined), stacked[r:], f, n) + require(mm(p, p, f) == p and mm(q, q, f) == q, "constructed idempotents") + require(rank(p, n, f) == r and rank(q, n, f) == s, "constructed ranks") + return p, q, minimum + + +def projectors(q, n, desired): + require(q**(n*n) <= 65536, "bounded projector census") + f, result = Field(q), [] + for entries in product(range(q), repeat=n*n): + p = tuple(tuple(entries[i*n:(i+1)*n]) for i in range(n)) + if mm(p, p, f) == p and rank(p, n, f) == desired: + result.append(p) + return result + + +def direct_key(p, q, f): + """Normalize P and use its full ambient centralizer, independent of K/L/M.""" + n = len(p) + x, y = factor(p, f) + basis = tr(x) + kernel(p, n, f) + change = tr(basis) + normalized_q = mm(mm(inverse(change, f), q, f), change, f) + normalized_p = mm(mm(inverse(change, f), p, f), change, f) + expected = diag(eye(len(y)), tuple((0,)*(n-len(y)) for _ in range(n-len(y)))) + require(normalized_p == expected, "direct first-projector normalization") + return min(mm(mm(gi, normalized_q, f), g, f) + for g, gi in group(f.q, len(y), n-len(y))) + + +def census(q, n, r, s): + f = Field(q) + p = tuple(tuple(int(i == j and i < r) for j in range(n)) for i in range(n)) + direct_group, forward, reverse, active = group(q, r, n-r), {}, {}, {} + others = projectors(q, n, s) + for other in others: + data = datum(p, other, f) + invariant = signature(data, f) + direct = min(mm(mm(gi, other, f), g, f) for g, gi in direct_group) + require(forward.setdefault(invariant, direct) == direct, "invariant merges direct classes") + require(reverse.setdefault(direct, invariant) == invariant, "invariant splits direct class") + recovered_p, recovered_q, minimum = realize(data, f) + require(signature(datum(recovered_p, recovered_q, f), f) == invariant, + "reconstruction changes orbit") + require(direct_key(recovered_p, recovered_q, f) == direct, + "reconstructed pair not directly conjugate") + pq, qp = mm(p, other, f), mm(other, p, f) + block = tuple(a+b for a, b in zip(p, pq)) + tuple(a+b for a, b in zip(qp, other)) + direct_active = (rank(tuple(a+b for a, b in zip(p, other)), 2*n, f) + + rank(p+other, n, f) - rank(block, 2*n, f)) + require(direct_active == minimum, "direct active-dimension formula") + require(minimum <= r+s+min(r, s), "active upper bound") + active[minimum] = active.get(minimum, 0)+1 + return {"field": q, "n": n, "r": r, "s": s, "cases": len(others), + "orbits": len(forward), "direct_group_order": len(direct_group), + "factor_group_order": len(group(q, r, s)), "active_dimensions": active} + + +def rejected(call, message): + try: + call() + except ValueError: + return + raise ValueError("control accepted: "+message) + + +def controls(): + f = Field(2) + p = ((1, 0, 0), (0, 0, 0), (0, 0, 0)) + image = ((1, 1, 0), (0, 0, 0), (0, 0, 0)) + d0, di, dd = (datum(p, q, f) for q in (p, image, tr(image))) + require(d0[5] == di[5] == dd[5], "Gram counterexample") + require(d0[3] == di[3] and d0[4] != di[4], "image needed") + require(d0[4] == dd[4] and d0[3] != dd[3], "kernel needed") + require(len({signature(d, f) for d in (d0, di, dd)}) == 3, "kernel/image omitted") + ortho = datum(((1, 0), (0, 0)), ((0, 0), (0, 1)), f) + skew = datum(((1, 1), (0, 0)), ((0, 0), (0, 1)), f) + require(ortho[3:5] == skew[3:5] and ortho[5] != skew[5], "product needed") + require(signature(ortho, f) != signature(skew, f), "product omitted") + deg = datum(((1, 1, 0), (0, 0, 0), (0, 0, 0)), + ((0, 0, 0), (1, 1, 1), (0, 0, 0)), f) + require(realize(deg, f)[2] == 3, "sharp active bound") + rejected(lambda: realize(deg, f, ambient=2), "small ambient") + rejected(lambda: realize((*deg[:3], ((1, 0),), deg[4], deg[5]), f), "bad kernel") + rejected(lambda: realize((*deg[:4], (), deg[5]), f), "missing image") + rejected(lambda: realize((*deg[:5], ((0, 0), (0, 1))), f), "identity block") + rejected(lambda: factor(((1, 1), (1, 1)), f), "nonidempotent") + rejected(lambda: rref(((2,),), 1, f), "out-of-field entry") + require(Field(4).mul[2][2] == 3 and 2*2 % 4 != 3, "extension field arithmetic") + padded = realize(deg, f, ambient=5) + require(signature(datum(*padded[:2], f), f) != signature(deg, f), "ambient omitted") + zero = ((0, 0), (0, 0)) + for pair in ((zero, zero), (zero, ((1, 0), (0, 0)))): + data = datum(*pair, f) + recovered = realize(data, f) + require(datum(*recovered[:2], f)[:3] == data[:3], "rank-zero factor fixture") + return 11 + + +def sharp_families(): + receipts = [] + for q in (2, 3, 4, 5): + f = Field(q) + seed_p = ((1, 1, 0), (0, 0, 0), (0, 0, 0)) + seed_q = ((0, 0, 0), (1, 1, 1), (0, 0, 0)) + for r, s in ((1, 1), (2, 2), (3, 2), (2, 3)): + p, other = (), () + for _ in range(min(r, s)): + p, other = diag(p, seed_p), diag(other, seed_q) + for _ in range(abs(r-s)): + p, other = diag(p, ((int(r > s),),)), diag(other, ((int(s > r),),)) + data = datum(p, other, f) + minimum = r+s-len(data[3])+len(data[4])-rank(data[5], r+s, f) + require(minimum == r+s+min(r, s) == len(p), "sharp family formula") + require(realize(data, f)[2] == minimum, "sharp family reconstruction") + receipts.append([q, r, s, minimum]) + return receipts + + +def main(): + cases = ((2, 4, 2, 2), (2, 4, 1, 2), (2, 3, 1, 2), (2, 3, 1, 1), + (3, 3, 1, 1), (3, 2, 1, 1), (4, 2, 1, 1), (5, 2, 1, 1)) + print(json.dumps({"censuses": [census(*case) for case in cases], + "sharp_families": sharp_families(), "controls": controls()}, sort_keys=True)) + print("PASS_IDEMPOTENT_FACTOR_INVARIANT") + + +if __name__ == "__main__": + main()