diff --git a/research/pr5681-characteristic-zero-trace-qualification/NOTICE b/research/pr5681-characteristic-zero-trace-qualification/NOTICE new file mode 100644 index 0000000000..2b36c8a00f --- /dev/null +++ b/research/pr5681-characteristic-zero-trace-qualification/NOTICE @@ -0,0 +1,29 @@ +PR5681 characteristic-zero trace qualification + +This contribution applies the classical trace identity to two explicitly +specified additional contracts. It claims no new trace identity, error in +PR5681's characteristic-two witness, general complex/native obstruction, +physical price or kappa result. + +inputs/PR5681-PROOF.md is an unchanged copy of Ali Romman's PR5681 proof at +67f07448eec5ad8d84bdf96b46981ac0b893592f, +research/one-sided-connector-audit/PROOF.md. + +inputs/PR5673-PROOF.md is the unchanged source proof retained at that same +head under research/one-sided-connector-audit/vendor/PR5673-PROOF.md. Its +original source is c10f75f09e41803ae8efe478331a7509b7379b2f, +research/crossed-connector-caller/PROOF.md. + +Retain Ali Romman's source attribution and substantial OpenAI Codex assistance +disclosure. Credit Cinna Davis's controller/simplex work, PR5617/5631/5649's +query-frame/fixed-star lineage and the complete P104/native/helper/compiler +predecessors named in the retained primary proofs. Formulation B was independently identified during review of formulation A. + +The new note and its separate local paper reviews were prepared with substantial +OpenAI Codex assistance. Local AI paper review is not independent human +scientific acceptance or proof-assistant validation. + +New contribution and retained primary proofs: Apache-2.0, consistently with +the repository contribution policy and original source notices. The intended +upstream overlay uses the repository-root LICENSE. Standalone redistribution +must also include that license text. Retain this notice and all source notices. diff --git a/research/pr5681-characteristic-zero-trace-qualification/PROOF.md b/research/pr5681-characteristic-zero-trace-qualification/PROOF.md new file mode 100644 index 0000000000..46706ba7bb --- /dev/null +++ b/research/pr5681-characteristic-zero-trace-qualification/PROOF.md @@ -0,0 +1,123 @@ +# Two characteristic-zero trace qualifications of the PR5681 static fixture + +This note applies the classical first-order trace identity to two specified additional characteristic-zero contracts suggested by the [PR5681](https://github.com/CrocSwap/integer-mult-bounds/pull/5681) static fixture. It is a conditional source-qualification argument, not a contradiction in the source construction. The elementary trace identity is not new. + +The primary source texts are the unchanged [PR5681 proof](inputs/PR5681-PROOF.md), sections 2–3, and its retained [PR5673 proof](inputs/PR5673-PROOF.md), section 1. Their immutable source pins are in [SOURCES.json](SOURCES.json). PR5681 works over characteristic two and supplies a static recipe, not a complete chronological word or a native lift. Its selected fixture has 31 leaves, block dimension four, and five square-zero thin maps of rank two over F2. Copying binary entries to another field is not asserted to preserve those properties. + +## 1. Common additional characteristic-zero contract + +Let F be a field of characteristic zero. Let + +$$ +W=W_0\oplus\cdots\oplus W_{31},\qquad \dim_F W_j=d=4, +$$ + +so that W has dimension 128. Use ordinary finite matrices over the free dual-number polynomial ring + +$$ +F[e,x_1,\ldots,x_{31}]/(e^2),\qquad x_j=D_j+1. +$$ + +The variables x_j are independent and central. All query matrices and projectors are constant over F. The element e is central and nonzero, and 1,e are linearly independent over F[x_1,…,x_31]. No additional quotient kills or identifies the first-order coefficient. This is an ordinary trace contract, not a graded or supertrace contract. Transferring the argument to a physical representation would require proof that it faithfully preserves this normalized coefficient identity. + +For stage j let E_j be identity on the core W_0 and leaf W_j, and zero elsewhere. Each stage has a finite full resolution by idempotent orthogonal projectors P_jh satisfying + +$$ +\sum_h P_{jh}=E_j, +$$ + +with the source support conditions and commutation with its stage kernel T_j. A full call is + +$$ +(I+x_jP_{jh})(I+eR_{jh}),\qquad R_{jh}=P_{jh}T_j. +$$ + +A thin call is I+eZ_l. Consider any finite ordering of all the declared full and thin calls. The required complete endpoint is + +$$ +(1+e)\prod_{j=1}^{31}(I+x_jE_j). +$$ + +The stage supports commute; no commutation among query matrices is assumed. Five thin calls is the selected fixture contract. The first case also holds for any finite number of square-zero thin derivatives. + +A claimed polynomial endpoint identity can be specialized at x_j=0 for every j, because the variables are independent. In characteristic zero this means **D_j=−1**, not D_j=1. The latter agrees only in the source characteristic-two setting. + +At this specialization every full-stage prefactor becomes identity. Writing Q_l for the query derivative of each full or thin call in its actual order gives + +$$ +\prod_l(I+eQ_l)=I+e\sum_lQ_l, +$$ + +since e²=0. The specialized target is I+eI_W. The free coefficient requirement therefore implies the necessary identity + +$$ +\sum_{\mathrm{full}}R_{jh}+\sum_{\mathrm{thin}}Z_l=I_W. \tag{E} +$$ + +Order cannot affect this particular coefficient. This is only a necessary condition; no converse or chronological construction follows. + +## 2. Case A: all query derivatives are square zero + +**Additional hypothesis A:** every full and thin query derivative is square zero over F. This may require a changed full-stage kernel. The verbatim source kernel is not identified with a square-zero matrix over characteristic zero. + +For example, if a newly supplied T_j satisfies T_j²=0 and commutes with its idempotent projectors, then + +$$ +(P_{jh}T_j)^2=P_{jh}^2T_j^2=0. +$$ + +For a square-zero matrix Q, image Q is contained in kernel Q. A basis adapted to these subspaces gives a matrix with zero diagonal, so tr Q=0. Taking ordinary traces in (E) would give + +$$ +0=\operatorname{tr}(I_W)=128, +$$ + +which is impossible in characteristic zero. + +Thus no word satisfies this 128-dimensional scalar target when all full and thin query derivatives are square zero over F. The conclusion needs no rank-two hypothesis or bound on stage splits or call order. It applies to the stated all-query-square-zero contract and is not a general assertion about complex callers. + +The hypothesis concerns Q²=0 for the derivative matrix over F. Automatic (eQ)²=0 says nothing about Q, because e²=0 holds for every Q. Likewise I+eQ is invertible with inverse I−eQ for arbitrary Q. Neither automatic nilpotence of eQ nor this invertibility implies derivative nilpotence or zero trace. + +## 3. Case B: verbatim full-stage kernel and square-zero thin derivatives + +**Additional hypothesis B:** keep the full-stage kernel verbatim on core and leaf j, + +$$ +T_j=\begin{pmatrix}I_d&I_d\\I_d&I_d\end{pmatrix}, +$$ + +retain the full resolutions, and require all five thin derivative matrices Z_l to remain square zero over F. Here T_j²=2T_j. Full-query nilpotence is not assumed. + +The full resolution gives + +$$ +\sum_hR_{jh}=\left(\sum_hP_{jh}\right)T_j=E_jT_j=T_j. +$$ + +Hence the total full-query trace is + +$$ +\sum_{j=1}^{31}\operatorname{tr}T_j=2gd=2\cdot31\cdot4=248. +$$ + +The target trace in (E) is (g+1)d=128. Consequently every successful word under the verbatim-full-stage contract must satisfy + +$$ +\sum_{\mathrm{thin}}\operatorname{tr}Z_l=(g+1)d-2gd=(1-g)d=-120. +$$ + +Square-zero thin derivatives have total trace zero, giving a contradiction. Thus no word satisfies this same target with the verbatim full-stage kernels, full resolutions and square-zero thin derivatives over characteristic zero. + +This conclusion assumes no nilpotence of the full derivatives. If arbitrary thin matrices are permitted instead, this argument supplies only the necessary equation Σthin tr Z_l=−120. It does not prove that arbitrary thin maps or a complete word are impossible. + +## 4. Source boundary and consequences + +PR5673 expressly permits arbitrary thin matrices Z. Its general theorem does not assume square-zero thin maps. Square-zero thin derivatives are additional hypotheses in the two proposed lifts above, motivated by the selected characteristic-two static fixture. + +The valid F2 witness is unaffected: 128,248 and120 vanish in characteristic two. Neither proof challenges its static ranks, signatures or source theorem. Neither proves that literal copying of its binary matrix entries preserves nilpotence over characteristic zero. + +These qualifications exclude neither all characteristic-zero/complex callers nor arbitrary-thin PR5673 contracts. They establish no general Fourier-character or native Gaussian obstruction, graded/supertrace extension, different-dimensional or changed-target exclusion, nonfull-stage result, or paid-idle-multiplier result. A different representation or contract requires its own endpoint and complete-cost argument. + +The useful result is the exact distinction between two source-bound counterfactuals: all-query nilpotence has trace zero against target 128; verbatim full T with full resolutions requires thin trace −120 against square-zero thin trace zero. It identifies an assumption that must change before these proposed chronological constructions could succeed. No actual word, native phase, frame adapter, ownership/stock/precision/tape bill, paid profile, complete caller, compiler/outer admission or κ follows. The selected frontier is unchanged. + +The classical trace identity receives no novelty claim. Credit Ali Romman's PR5681 static construction/audit and retained PR5673 proof, Cinna Davis's controller lineage, PR5617/5631/5649's query-frame and fixed-star line, and the retained P104/native/helper/compiler predecessors. Formulation B was independently identified during review of formulation A. Prepared with substantial OpenAI Codex assistance, including independent local AI paper review; no human-independent scientific acceptance or proof-assistant theorem is claimed. diff --git a/research/pr5681-characteristic-zero-trace-qualification/README.md b/research/pr5681-characteristic-zero-trace-qualification/README.md new file mode 100644 index 0000000000..3cd424aa53 --- /dev/null +++ b/research/pr5681-characteristic-zero-trace-qualification/README.md @@ -0,0 +1,40 @@ +# Two source-bound characteristic-zero trace qualifications + +Two specific characteristic-zero contracts suggested by [PR5681](https://github.com/CrocSwap/integer-mult-bounds/pull/5681)'s static connector fixture cannot satisfy its retained scalar endpoint. With every query derivative square zero, the necessary trace equation is 0=128. With the verbatim full-stage kernel and full resolutions, the thin derivatives must instead have total trace −120, whereas square-zero thin derivatives have total trace zero. The [proof](PROOF.md) states the exact additional hypotheses and derives each qualification. + +This applies a classical trace identity to specified contracts. It does not identify an error or contradiction in the source author's characteristic-two construction. The valid F2 witness is unaffected, and [PR5673](https://github.com/CrocSwap/integer-mult-bounds/pull/5673)'s arbitrary-thin-matrix class is not excluded. No general complex/native/caller exclusion, chronological construction, physical tariff or κ result is claimed. The selected frontier is unchanged. + +## Exact source and version provenance + +The primary source object is PR5681 head `67f07448eec5ad8d84bdf96b46981ac0b893592f`, package `research/one-sided-connector-audit`. Two unchanged source proofs are supplied locally: + +- [PR5681-PROOF.md](inputs/PR5681-PROOF.md), sections 2–3: characteristic-two static square-zero maps, including the 31-leaf fixture with block dimension four and five rank-two thin maps. +- [PR5673-PROOF.md](inputs/PR5673-PROOF.md), section 1: stage kernels, full resolutions, arbitrary thin matrices, independent stage variables and the complete ordered target. PR5681 retains this proof from source commit `c10f75f09e41803ae8efe478331a7509b7379b2f`. + +[SOURCES.json](SOURCES.json) records immutable public paths, Git blobs, SHA256 hashes and exact preparation provenance. The two source copies preserve original text and credit. Their scientific execution statements are source-author evidence; no source checker was run here. + +The new PROOF.md is a standalone adaptation of the locally frozen, independently reviewed V2 trace tuple. That tuple comprises proof SHA256 `37d13fa8d60115fdf4ff62c89ed2361d7a898aa99ed7f0931cc31d8711149469` and contract SHA256 `65bd829e2b17382029b6d1ee16d248e2116a059e5de47824a8099029789c7b02`. Its separate V2 review has SHA256 `9f168e80009239a6a6de23e82e75e10e698f5779024a88320df2d71236f3c956`. The review accepted the specified conditional paper arguments. It is not an acceptance of these adapted package bytes. The adapted package has a separate review obligation; acceptance of an earlier tuple is not silently transferred to changed bytes. + +The original and clarified argument versions retain separate immutable provenance. The source-specific contribution is the two explicit conditional trace budgets; no exhaustive novelty claim follows from source or overlap qualification. + +## Evidence and qualification boundary + +The argument works over ordinary matrices in the free ring F[e,x₁,…,x₃₁]/(e²), with F of characteristic zero, independent central x_j=D_j+1, and constant query coefficients. The elements 1,e must remain linearly independent over F[x]. Specializing x=0 means D=−1 in characteristic zero. Faithful preservation of that normalized first-order coefficient identity is required before transferring the argument to a physical representation. + +Both qualifications concern derivative matrices Q satisfying Q²=0 over F. Automatic (eQ)²=0 and invertibility of I+eQ hold for arbitrary Q and do not supply this hypothesis. Case A may change the full kernel; Case B keeps the verbatim T, for which T²=2T, and assumes no full-query nilpotence. Thin rank two is fixture context rather than a trace-proof premise. + +This is an unregistered static proof package. Its explicitly named custom custody manifest is not generic research-runner metadata. No verifier, `TASK.json`, `VERIFY.json`, synthetic `RESULT.json` or CI receipt is supplied. Local source-copy hashes were checked only as packaging bookkeeping against existing authenticated pins. No new source query, numeric or scientific run, source import, matrix/WORD generation, constructor, chronological search or native replay occurred. + +## Credit + +Credit Ali Romman for PR5681's static construction/audit and the retained PR5673 proof and source bounds; Cinna Davis's controller and simplex lineage; [PR5617](https://github.com/CrocSwap/integer-mult-bounds/pull/5617), [PR5631](https://github.com/CrocSwap/integer-mult-bounds/pull/5631) and [PR5649](https://github.com/CrocSwap/integer-mult-bounds/pull/5649) for the query-frame/fixed-star line; and the complete retained P104/native/helper/compiler lineage. Formulation B was independently identified during review of formulation A. The source's existing caveat that a characteristic-two static witness supplies no native lift remains predecessor work. + +The trace identity is classical. No novelty of that identity or source-author contradiction is claimed. Prepared with substantial OpenAI Codex assistance, including separate local AI paper reviews; these are not human scientific acceptance or formal proof-kernel validation. Source notices and Apache-2.0 terms are retained; see [NOTICE](NOTICE). + +## Open next questions + +1. **Which additional contract could support a characteristic-zero construction?** The exact trace budgets show that either derivative nilpotence, verbatim full-stage structure/resolutions, scalar target/dimension, or the faithful coefficient model must change. First specify one concrete revised contract and derive its necessary coefficient equation. No changed family is nominated here, and its endpoint/native/cost obligations would need separate scope and source review. +2. **Can arbitrary thin derivatives satisfy the full ordered endpoint?** PR5673 permits them, and the verbatim-full-T case only imposes total thin trace −120. That necessary condition is not a construction. A useful first step is a specified source-bound candidate with the exact polynomial endpoint; no synthesis or search is authorized by this note. +3. **Can a physical representation faithfully preserve the normalized coefficient identity?** That is required before either qualification transfers. Begin with an explicit representation and proof of the relevant coefficient binding. A physical first-order shear or invertible I+eQ alone does not prove Q²=0. + +The smallest useful follow-up is review of the exact source contracts and paper argument before proposing a revised lift. No new scientific execution is needed to inspect the two paper arguments. diff --git a/research/pr5681-characteristic-zero-trace-qualification/SOURCES.json b/research/pr5681-characteristic-zero-trace-qualification/SOURCES.json new file mode 100644 index 0000000000..88624e46bf --- /dev/null +++ b/research/pr5681-characteristic-zero-trace-qualification/SOURCES.json @@ -0,0 +1,71 @@ +{ + "schema": "pr5681-characteristic-zero-trace-qualification-custody/1", + "status": "STATIC_CONDITIONAL_SOURCE_QUALIFICATION", + "registration": { + "generic_runner_registered": false, + "no_verifier_or_execution_receipt": true, + "meaning": "This is a custom custody manifest, not TASK/SOURCES/VERIFY runner metadata" + }, + "primary_object": { + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/5681", + "head": "67f07448eec5ad8d84bdf96b46981ac0b893592f", + "package": "research/one-sided-connector-audit" + }, + "files": [ + { + "local_path": "inputs/PR5681-PROOF.md", + "repository_path": "research/one-sided-connector-audit/PROOF.md", + "commit": "67f07448eec5ad8d84bdf96b46981ac0b893592f", + "immutable_public_url": "https://github.com/aliromman/integer-mult-bounds/blob/67f07448eec5ad8d84bdf96b46981ac0b893592f/research/one-sided-connector-audit/PROOF.md", + "sha256": "2e52ac6d32923a1ce6f9693415df553b2d4c38c1a103b9e1968c4e114044d800", + "git_blob": "e3be1bb272f3a73a8c6cd248fec69dec498e401d", + "bytes": 8205, + "license": "Apache-2.0", + "use": "Unchanged primary proof read as text; source execution claims remain author evidence" + }, + { + "local_path": "inputs/PR5673-PROOF.md", + "repository_path": "research/one-sided-connector-audit/vendor/PR5673-PROOF.md", + "commit": "67f07448eec5ad8d84bdf96b46981ac0b893592f", + "immutable_public_url": "https://github.com/aliromman/integer-mult-bounds/blob/67f07448eec5ad8d84bdf96b46981ac0b893592f/research/one-sided-connector-audit/vendor/PR5673-PROOF.md", + "sha256": "e086b3376173f6b790e05ef09f23b4d5970c8ac5145ab2970e084743f782190b", + "git_blob": "e3800fbcf1c5f5633e14d9856ca1400985292a0d", + "bytes": 9581, + "license": "Apache-2.0", + "use": "Unchanged primary proof read as text; source execution claims remain author evidence", + "original_source": { + "repository": "aliromman/integer-mult-bounds", + "commit": "c10f75f09e41803ae8efe478331a7509b7379b2f", + "path": "research/crossed-connector-caller/PROOF.md" + } + } + ], + "version_binding": { + "adapted_proof": "PROOF.md", + "basis": "Standalone adaptation retaining the accepted conditional mathematics, extra hypotheses and source boundaries", + "review_scope": "The adapted publication bytes require a separate exact-byte review; earlier acceptance is version-specific", + "identity_novelty": "Classical; none claimed", + "source_specific_coverage": "Bounded source qualification does not establish exhaustive global novelty" + }, + "checks_performed": "SHA256/Git-blob/length source-copy custody and accepted-local-file hash bookkeeping only; no fresh authentication or scientific execution", + "claims_not_made": [ + "Novel trace identity", + "Contradiction in PR5681 source witness", + "Exclusion of arbitrary thin PR5673", + "General characteristic-zero/complex/native/caller obstruction", + "Physical price or kappa improvement", + "CI pass or proof-kernel verification" + ], + "license": "Apache-2.0; root LICENSE supplied by intended upstream overlay", + "publication_base": { + "commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "tree": "b2cba28bc921bd50607d1417b43fbafdfe9058cf", + "meaning": "Exact upstream preparation base; no selected-result change" + }, + "argument_provenance": { + "accepted_proof_sha256": "37d13fa8d60115fdf4ff62c89ed2361d7a898aa99ed7f0931cc31d8711149469", + "accepted_contract_sha256": "65bd829e2b17382029b6d1ee16d248e2116a059e5de47824a8099029789c7b02", + "separate_paper_review_sha256": "9f168e80009239a6a6de23e82e75e10e698f5779024a88320df2d71236f3c956", + "meaning": "These hashes identify the earlier accepted conditional argument and contract adapted into PROOF.md; they are not proof-kernel or CI receipts and do not bind changed package bytes" + } +} diff --git a/research/pr5681-characteristic-zero-trace-qualification/inputs/PR5673-PROOF.md b/research/pr5681-characteristic-zero-trace-qualification/inputs/PR5673-PROOF.md new file mode 100644 index 0000000000..e3800fbcf1 --- /dev/null +++ b/research/pr5681-characteristic-zero-trace-qualification/inputs/PR5673-PROOF.md @@ -0,0 +1,231 @@ +# A connector must distinguish leaves in both directions + +This is a theorem about finite matrices in characteristic two. It is not a +native multiplication theorem. No new kappa is established. + +## 1. Contract + +Let the main space be `W_0 + W_1 + ... + W_g`, with each block of dimension +`d > 0`. Block zero is the core. Stage j acts on the core and leaf j. On these +two blocks put + +```text +E_j = diag(I,I), T_j = [[I,I],[I,I]]. +``` + +Thus `T_j^2=0`. Stage j can have any finite number of full calls. Their +projectors `P_jh` form an orthogonal resolution of `E_j`, and commute with +`T_j`. Their query maps are `R_jh=P_jh T_j`. There is no bound on the number +of stages, the number of splits, the block dimension, or their call order. + +In the normalized ring `F[e,D_1,...,D_g]/(e^2)`, a full call is + +```text +(I+(D_j+1)P_jh)(I+e R_jh). +``` + +A thin call is `I+e Z`. The proof permits arbitrary matrices Z. In particular, +it does not impose a rank, a square-zero condition, or a count on thin calls. +The required word is `Q product_j (I+(D_j+1)E_j)`, where `Q=1+e`. +The main fields are independent. All D variables remain independent. + +This is the star stage contract from PR5631/5649, with arbitrary stage splits +and a much larger connector class. It excludes no general complex or dyadic +caller. It also excludes no caller with a different grouped stage map, a +nonfull stage, a different output, or paid idle multipliers. + +## 2. The one-sided theorem + +**Theorem.** A successful word cannot have three distinct leaves whose block +columns are identical in every thin matrix Z. It also cannot have three +leaves whose block rows are identical in every thin matrix Z. + +Only one of these two equalities is needed for exclusion. Thus changing the +forward split, adding more queries, increasing their rank, or adding more +stage splits cannot repair connectors which only see the sum of the leaves. + +### Local form and chronology + +Commutation with T and the local support give + +```text +P_jh = [[A_jh+B_jh, B_jh], [B_jh, A_jh+B_jh]], +R_jh = [[A_jh, A_jh], [A_jh, A_jh]]. +``` + +The A matrices form an orthogonal resolution of I. In particular, +`A_jh A_jk=0` for `h!=k`, `A_jh^2=A_jh`, and `sum_h A_jh=I`. +These statements do not require the A matrices of different stages to commute. +The orthogonal-resolution hypothesis also follows from full rank use: if the +projectors sum to E and their ranks sum to rank E, their images form a direct +sum. Each projector is then the corresponding coordinate projection on that +sum. Stages with a rank deficit are a different contract. + +Set all D variables to one. The coefficient of e requires `sum R=I`, including +thin queries. The mixed coefficient of `e(D_j+1)` then requires + +```text +sum_(full call i in stage j) [P_i, sum_(calls l later than i) R_l] = 0. (1) +``` + +This necessary condition follows by expanding the literal ordered word. +No full-word converse is used. + +For distinct selected stages j,k define + +```text +S_jk = sum_(call (j,h) before call (k,l)) A_jh A_kl. (2) +``` + +In (1), add block rows zero and j, and read block column k. The contribution +of good calls is S_jk. The contribution of a later thin map Z is +`A_jh (Z_0k+Z_jk)`. If the three selected leaf columns of every Z are equal, +this thin contribution is the same for the two choices of k other than j. +Consequently + +```text +S_jk = S_jl for each permutation (j,k,l) of the three stages. (3) +``` + +Other good stages do not contribute to these blocks. Thus the argument +restricts to any three selected leaves in a larger star. + +### The prefix determinant argument + +Read just the calls of the three selected stages in their original order. +Before a call with projection A from stage j, let P_k be the sum of the A +projections already read from stage k. Left multiplication of (2) by A and +orthogonality within stage j give + +```text +A S_jk = A(I+P_k). +``` + +Equation (3) gives `A P_k=A P_l`. Also `A P_j=0`. Therefore, for the total +prefix `S=P_0+P_1+P_2`, every update satisfies + +```text +A S=0. (4) +``` + +Introduce an independent central variable x. Equation (4) implies + +```text +(I+xA)(I+xS) = I+x(S+A). +``` + +Starting at S=0, the product of all these factors is `I+xS_final`. +At the end, `S_final=I+I+I=I`. On the other hand, an idempotent of rank r +has determinant `det(I+xA)=(1+x)^r`. Each stage is a resolution of I, +so its ranks sum to d. Taking determinants now gives + +```text +(1+x)^(3d) = det(product(I+xA)) = det((1+x)I) = (1+x)^d. +``` + +This is impossible for positive d. This proves the column statement for +all finite dimensions and all finite split counts. It uses no list of orders. +Transpose all matrices and reverse the order to obtain the row statement. + +## 3. A paid-rank and finite-field cut + +Assume g is at least three. The sum of the good queries is +`sum T_j`. Hence the thin sum must be + +```text +K = I+sum T_j = epsilon E_core + F+G, +epsilon = (g+1) mod 2, +F: each leaf -> core by I, G: core -> each leaf by I. +``` + +The rank of K is `2d`. Its column space is the core plus the diagonal leaf +space, and its row space is the core plus the leaf-sum space. + +Let U be the span of all thin images, and V the span of all thin row spaces. +Write `dim U=2d+a`, `dim V=2d+b`, and let R be the sum of thin ranks. +Factor each thin map at its actual rank, then concatenate those factors. +Sylvester's rank inequality gives + +```text +R >= dim U + dim V - rank K = 2d+a+b. (5) +``` + +Both a and b must be positive. Otherwise one side of the one-sided theorem +applies to all leaves. In particular **R >= 2d+2**, over any field of +characteristic two. + +For a finite field of size s, choose b additional row basis vectors beyond +the row space of K. Their restriction to one leaf is a `b by d` matrix. +There are at most `s^(bd)` such signatures. Equal signatures imply equal +leaf columns for every thin map. Each signature can occur at most twice. +The column-space argument is the same. Therefore + +```text +g <= 2 s^(bd), g <= 2 s^(ad), +R >= 2d + 2 h, h = min {z >= 0 : g <= 2 s^(dz)}. (6) +``` + +This is a necessary condition, not a construction or a sufficient test. +It concerns a common field and a fixed block basis. For one-port binary +copies, d=2. It gives R>=6 for g=3..8, R>=8 for g=9..32, and R>=10 for +g=33..128. For coupled ports, use the actual larger d. Do not apply the +one-port bound per port after ports have been coupled. + +At g=31, five rank-one connectors fail this cut. Five rank-two connectors +with d=4 meet it exactly: `2d+2=10`. Thus coupled pairs of ports are a precise +remaining target. The cut does not prove that such a word exists. + +## 4. Constructive escape and its price + +`ESCAPE-WORD.json` contains a complete eight-field binary word. It has three +paired stages, six full calls with rank-one queries, and eight rank-one thin calls. +Every local projector, query rank and compatibility relation is checked. +The verifier retains every exponent of each independent D variable and +checks every coefficient of the full word. It also checks that the thin +maps distinguish all three leaves in both directions. + +Thus the changed connector contract has a real positive operator. It does +not give a profitable supplier. At the pinned PR5599 tariff, 104 copies have +complete optimistic moment coefficients + +```text +208 H25 + 624 H9 + 6 helpers - 6 paid - 832 H1. +``` + +Its linear margin is -336. After common ranks are cancelled, all positive +terms have rank at least eight and all negative terms have rank at most +seven. For every `0<=t<=1`, the margin is at most `8^(t-1)*(-336)<0`. +Additional physical adapters cannot repair that price. + +The new cut still leaves a useful target. At g=127, ten thin queries are +allowed by (6) for one-port binary copies. The optimistic PR5599 profile +has a positive exact margin at saving `7/2000=.0035`, and its numerical +crossing is about .00364156. **No 127-leaf word is supplied.** This screen +also does not establish a characteristic-zero lift, native frame adapters, +compiler admission, an outer transfer, or a new kappa. + +A smaller coupled target is g=31 with five rank-two connectors per two-port +block. Its optimistic bill, scaled to 104 ports, also has positive exact +margin at .0035. It needs only 62 full calls. No such word is supplied either. +Coupling physical ports can require new frame maps; their costs must be +charged before this screen can become a supplier claim. + +## 5. Evidence and limits + +The main result is a written finite-dimensional matrix proof. The checker +also verifies fifteen exact free-algebra certificates for the paired-stage +case, without a solver or the discovery implementation. Matrix and formal +polynomial controls test the chronology extraction, restriction to three +leaves, prefix factorization and determinant formula. They support the +proof; finite tests alone do not prove its unbounded statements. + +The discovery archive retains changed C,D splits, arbitrary aggregate maps, +extra thin queries, a different cycle frame, and three-/four-way splits. +Timeouts remain unknown. Passing first mixed coefficients is not passing the +full word. No proof assistant or independent human acceptance is claimed. + +Credit Cinna Davis's controller and simplex work; PR5617/5631/5649 for the +query-frame and fixed-star line; and the complete P104/native/helper/compiler +lineage for the tariff. This proof, cut, search and escape word were prepared +for Ali Romman with substantial OpenAI Codex assistance. No subagents. +New work is Apache-2.0. diff --git a/research/pr5681-characteristic-zero-trace-qualification/inputs/PR5681-PROOF.md b/research/pr5681-characteristic-zero-trace-qualification/inputs/PR5681-PROOF.md new file mode 100644 index 0000000000..e3be1bb272 --- /dev/null +++ b/research/pr5681-characteristic-zero-trace-qualification/inputs/PR5681-PROOF.md @@ -0,0 +1,169 @@ +# The static connector rank cut is sharp + +This package checks the proof in the retained PR5673 source. It also gives +new static witnesses at its rank lower bound. A static witness gives the +thin query maps, their sum, ranks and leaf signatures. It does not give a +chronological word. No new kappa follows. + +## 1. Audit of the source implication + +Use the source contract, over a field of characteristic two. Each stage j +has full projectors P_jh supported on the core and leaf j. They give an +orthogonal resolution of that support. They commute with the local query +T_j, whose four blocks are I. Their queries are R_jh=P_jh T_j. +A thin map Z has no stage variable. All stage variables are independent. +The target is the stated product of full stages, times the scalar 1+e, +where e squared is zero. These hypotheses are required. + +Put x_j=D_j+1. Work first in the quotient which also sets x_j squared to +zero and every other x to zero. This quotient supplies necessary conditions +only. Read the literal calls in application order. If R_< and R_> are the +sums before and after a full call (P,R), the coefficient of e x_j contributed +by that call is + +```text +P R_< + R_> P + P R. +``` + +The coefficient of e first gives sum R=I. Since P R=R, the expression becomes +`P + P R_> + R_> P`. Summing the stage projectors gives E_j. The target has +e x_j coefficient E_j. Thus its defect is exactly the sum of commutators +`P R_> + R_> P`. No pure higher coefficient or endpoint converse is assumed. + +Commutation with T gives P=[[A+B,B],[B,A+B]]. The idempotent and orthogonality +relations imply that the A matrices in each stage are orthogonal idempotents +with sum I. Add block rows core and j, then take leaf column k, where k!=j. +The right product R_> P has no such column. A later stage k contributes +A_jh A_kl. Other full stages contribute zero. A thin map contributes +`A_jh (Z_0k+Z_jk)`. This proves the source restriction even when there are +other leaves, noncommuting stage flags and arbitrary blocks outside the +chosen three columns. + +If three leaf columns of every thin map agree, the thin contribution does +not depend on which of the other two leaves is k. Therefore S_jk=S_jl, +where S_jk is the sum of A_jh A_kl for jh before kl. For a given call A_jh, +orthogonality within j gives `A_jh S_jk=A_jh(I+P_k)`, with P_k the earlier +prefix of stage k. Thus A_jh P_k=A_jh P_l. Its own earlier prefix is +annihilated. The total prefix S obeys A_jh S=0. + +For a formal central variable x, this gives +`(I+xA)(I+xS)=I+x(A+S)` at every step. The product of factors is therefore +`(1+x)I`, since the three final stage prefixes each equal I. Each idempotent +of rank r has determinant (1+x)^r: its image and kernel give a direct sum +basis. Each stage contributes total rank d. The same determinant would have +to be both (1+x)^(3d) and (1+x)^d. These polynomials have different degrees +for d>0. This is a contradiction over every field of characteristic two. +Transpose and reverse the whole word for the row version. The target is +preserved by this operation because its full stage supports commute. + +No mathematical gap was found in this implication under these hypotheses. +The source does not exclude a different stage support, an incomplete stage, +a different target or a characteristic-zero caller. This audit does not +supply human review or a proof-assistant theorem. + +## 2. Rank cut and its exact static realization + +Let F have q elements, where q is a power of two. Let d,h be positive +integers. Put + +```text +g = 2 q^(d h) - 1, W = F^d + (F^d)^g. +``` + +Index the leaves by all h-by-d matrices M over F: use the zero matrix once +and every nonzero matrix twice. On W, define F_i to send coordinate i of +every leaf to core coordinate i. Define G_i to send core coordinate i to +coordinate i of every leaf. Both have rank one and square zero. Put + +```text +K = sum_i (F_i+G_i). +``` + +This is the required thin sum for odd g. It has rank 2d. Its image consists +of the core and the diagonal leaf space. Its row space consists of the core +and the leaf-sum space. + +For 1<=a<=h, let u_a have zero core and leaf block equal to row a of M, +viewed as a column. Let v_a have zero core and the same leaf entries as a +row. Put E_a=u_a v_a. Each E_a has rank one. Every nonzero signature occurs +twice, so + +```text +sum_leaf u_a = 0, sum_leaf v_a = 0, v_a u_b = 0 +``` + +for all a,b. Consequently E_a E_b=0; F_i E_a=E_a F_i=0; and +G_i E_a=E_a G_i=0. In particular all these maps have square zero. +Take the following thin maps, with both copies of each E_a charged: + +```text +F_0,...,F_(d-1), G_0,...,G_(d-1), E_1,E_1,...,E_h,E_h. +``` + +Their sum is K and their total rank is exactly 2d+2h. Their image span and +row span each have dimension 2d+h. To see independence of the extra h +vectors modulo the diagonal space, first inspect the zero-signature leaf. +It forces any diagonal component to vanish. Then inspect signatures with +one nonzero matrix entry; these force each coefficient of u_a to vanish. +The row proof is the same. + +Two leaves have the same block columns in all thin maps exactly when their +matrices M agree. Indeed the F/G columns are constant across leaves, and +E_a recovers row a of M because u_a is nonzero. The row statement uses v_a. +Thus there are exactly q^(dh) signatures; each occurs once or twice. +No forbidden triple occurs. + +The source Sylvester bound is R>=2d+a+b, with extra image and row dimensions +a,b. Both equal h here, so equality holds. The source signature bound asks +for the least z such that g<=2q^(dz). For this g, that least z is h. +Thus **both bounds are attained together by square-zero maps**, for every +q,d,h above. This proves sharpness of these static bounds at an unbounded +family of sizes. It does not prove sharpness for complete chronological +words. + +## 3. Five rank-two maps for the 31-leaf target + +When h=1 and d>=2, write E=E_1 and group the charged rank-one maps as + +```text +Z_0 = F_0 + E, +Z_1 = G_1 + E, +Z_(i+1) = F_i + G_((i+1) mod d), 1<=i