Prove sharp boundary-rank tradeoff for cyclic reversal (no κ)

research/cyclic-reversal-rank-tradeoff/PROOF.md

@@ -0,0 +1,141 @@
+# Sharp rank cost of noncentral cyclic reversal
+
+This contribution is produced by Nick Petalas. Apache-2.0.
+
+## Contract and statement
+
+Let K be any field, p >= 2, q >= 1 and w >= 0. Let C_p be the permutation
+matrix sending e_i to e_(i+1 mod p). On K^(pq+w), put
+
+    U = C_p direct-sum ... direct-sum C_p direct-sum I_w,
+                q copies
+    g = gcd(p,2),    D = q(p-g),    N = D/2.
+
+The w workspace coordinates have arbitrary initial values. A boundary map
+J is any invertible K-linear map on this complete space. It may couple
+different cycles and workspace coordinates. Its rank charge is rank(J-I).
+Define the complete reversal defect by
+
+    E(U,J) = J^-1 U J - U^-1.
+
+All ranks include workspace rows and columns. Exact reversal means E=0,
+so the complete conjugated program acts as the inverse on every cycle and
+as the identity on every workspace coordinate, with no input promise.
+
+**Theorem.** For every integer r >= 0,
+
+    min { rank E(U,J) : J invertible, rank(J-I) <= r }
+        = max(0, D-2r).                                      (1)
+
+In particular, the exact minimum boundary rank for reversal is N,
+independently of w. One attaining boundary is the permutation reflection
+i -> -i modulo p on each cycle, extended by identity on workspace.
+The theorem includes characteristic two and characteristics dividing p.
+
+The defect rank is an exact algebraic error measure. It is not an
+entrywise error, a norm error or a recursive power tariff.
+
+## Lower bound, including arbitrary workspace mixing
+
+The kernel of C_p-C_p^-1 is the kernel of C_p^2-I, after multiplication
+by an invertible matrix. The latter consists of vectors constant on each
+orbit of adding two modulo p. There are g such orbits. This argument uses
+only equality of coordinates, so it works in every characteristic.
+Consequently rank(U-U^-1)=D, including the identity workspace block.
+
+Set A=J-I. Multiplication by invertible J preserves rank, and
+
+    J E(U,J) = UJ-JU^-1
+             = (U-U^-1) + UA-AU^-1.
+
+Rank subadditivity and the reverse triangle inequality give
+
+    rank E(U,J) >= D-rank(UA-AU^-1)
+                >= D-2 rank A >= D-2r.
+
+Nonnegativity supplies the other lower bound. No block structure, field
+extension, diagonalization or restriction on J was used. In particular,
+an arbitrarily large finite identity-stage workspace cannot lower it.
+
+## Attainment by partial reflections
+
+First take q=1 and w=0. Put n=(p-g)/2. For 0 <= s <= n, let J_s be the
+product of the disjoint transpositions
+
+    (1,p-1), (2,p-2), ..., (s,p-s).
+
+Thus J_s is involutory and rank(J_s-I)=s over every field. Each swapped
+pair contributes a nonzero rank-one block, even in characteristic two.
+
+The permutation J_s C_p consists of the s transpositions
+
+    (0,p-1), (1,p-2), ..., (s-1,p-s)
+
+and one cycle on s,s+1,...,p-s-1, of length L=p-2s. A cycle of length one
+is allowed. Squaring fixes every transposition coordinate, and its action
+on the remaining cycle has gcd(L,2)=g cycles. Therefore
+
+    rank((J_s C_p)^2-I) = L-g = p-g-2s.
+
+The identity
+
+    C_p J_s-J_s C_p^-1
+        = J_s ((J_s C_p)^2-I) C_p^-1
+
+shows that this is exactly the reversal defect rank. This proves (1)
+for one cycle up to budget n; the full reflection gives zero for larger
+budgets.
+
+For q cycles, set r'=min(r,qn) and choose integers s_i in [0,n] summing
+to r'. Fill one cycle up to n, then the next, until r' is exhausted.
+Take the direct sum of their J_(s_i), together with I_w. Its boundary rank
+is r' and its defect rank is
+
+    sum_i (p-g-2s_i) = D-2r' = max(0,D-2r).
+
+This proves attainment for every parameter and completes the theorem.
+
+## A two-sided boundary consequence
+
+Even if the input and output boundaries are different, any invertible
+L,R with L U R=U^-1 must satisfy
+
+    rank(L-I)+rank(R-I) >= D.                                (2)
+
+Indeed U^-1-U=(L-I)UR+U(R-I), and both U and R are invertible.
+The two full reflections attain equality in (2). This is the total
+ordinary boundary-rank allowance, which is positive for p>2. It does not
+determine a concave price, physical realization or complete cost.
+
+## Relevance and limits
+
+Ali Romman's [PR6168](https://github.com/CrocSwap/integer-mult-bounds/pull/6168)
+leaves noncommuting native address maps outside its forward cyclic tariff.
+The new result quantifies one such changed boundary, on the regular cyclic
+coordinate representation, including arbitrary finite dirty workspace.
+It neither invokes nor replays the predecessor tariff. Its rank inequality
+and elementary permutation facts are standard; the scoped sharp tradeoff
+and its application are the contribution here. No literature-priority
+claim is made.
+
+Adam Gall / [PR1941](https://github.com/CrocSwap/integer-mult-bounds/pull/1941)
+already gives concrete cyclic-reflection permutations and swap counts for
+even cycles. This result adds optimality over all invertible boundaries,
+the residual-rank tradeoff and arbitrary-field workspace stability.
+
+
+For example p=7,q=1 has exact reversal boundary rank 3. Budgets 0,1,2,3
+leave minimum defect ranks 6,4,2,0. All are attained by the displayed
+partial reflections. The checker computes these cases directly.
+
+A regular permutation representation is essential to the stated formula.
+An action whose order merely divides p can have a smaller rank difference.
+The result does not identify this matrix rank with a Clifford symplectic
+rank, a Gaussian/BIT child rank or an ordinary execution cost. A native
+realization, phases, productive credits, caller, precision, movement and
+compiler bill remain separate obligations. There is no supplier admission,
+new kappa or change to the selected frontier or its five assumptions.
+
+The universal statement follows from the written proof. Finite checking
+corroborates it and checks the implementation. Independent human and
+formal proof-kernel review are unclaimed.

research/cyclic-reversal-rank-tradeoff/README.md

@@ -0,0 +1,110 @@
+# Sharp rank cost of noncentral cyclic reversal
+
+For q independent p-cycles over any field, the exact minimum rank of J-I
+needed to conjugate the complete stage to its inverse is
+
+    q floor((p-1)/2).
+
+This holds with any finite identity-stage workspace and arbitrary mixing
+with it. For a boundary rank budget r, the exact minimum rank of the
+complete reversal defect is
+
+    max(0, q*(p-gcd(p,2))-2r).
+
+Partial permutation reflections attain every budget, including in
+characteristics dividing p. Different input and output boundaries must
+have total rank at least q*(p-gcd(p,2)), also sharply. [PROOF.md](PROOF.md)
+states the complete all-input contract and proves these claims.
+
+Claim type: **scoped proof with finite exact corroboration**. No new kappa
+is claimed. Ordinary matrix rank is not automatically a native tariff.
+
+## Source and contribution
+
+The source question is Ali Romman's
+[PR6168](https://github.com/CrocSwap/integer-mult-bounds/pull/6168), specifically
+the noncommuting native-map route left open in
+`research/cyclic-stage-rank-budget/README.md`. This result changes that
+constant-in-stage premise to a specified noncentral boundary. It supplies
+a necessary boundary-rank allowance before attempting a physical cyclic
+reversal. The predecessor's query tariff is not rechecked or used as a
+theorem dependency. No predecessor implementation is copied or imported.
+
+Base: canonical main `a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority
+revision 8. The selected conditional kappa `781451/250000000` is unchanged.
+The decoder card is explicitly changed to this boundary-rank subproblem.
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19272032).
+Source pins and exact scope are in [SOURCES.json](SOURCES.json) and
+[TASK.json](TASK.json).
+
+The rank inequalities and permutation-cycle facts are classical. The
+sharp stable rank tradeoff and this application are produced by Nick Petalas.
+Ali Romman retains the question and cyclic caller context; Cinna Davis and
+the retained native/query/caller lineage retain their source contributions.
+No worldwide priority claim is made. Apache-2.0.
+
+Adam Gall / [PR1941](https://github.com/CrocSwap/integer-mult-bounds/pull/1941)
+already gives concrete cyclic-reflection permutations and swap counts for
+even cycles. This result adds optimality over all invertible boundaries,
+the residual-rank tradeoff and arbitrary-field workspace stability.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/cyclic-reversal-rank-tradeoff/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/cyclic-reversal-rank-tradeoff/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cyclic-reversal-rank-tradeoff
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cyclic-reversal-rank-tradeoff --check-source-history
+```
+
+The direct marker is `PASS_CYCLIC_REVERSAL_RANK_TRADEOFF`. Every replay emits
+a generated JSON receipt binding the six package files by SHA256. It writes
+no files and needs neither Git nor a network connection. Registered replay
+runs both warning-strict normal and optimized modes.
+
+Evidence covers partial-reflection constructions at periods 2 through 32,
+one through four cycles and zero or three workspace coordinates. A separate
+dense elimination checks fields F2,F3,F5,F7,F11 through period 12. Complete
+binary matrix enumerations include a dirty-workspace case and characteristic
+dividing the period. The replay checks 5,544 constructions, 1,560 dense
+field cases and 5,912 two-sided permutation boundaries. It enumerates 132,096 binary matrices,
+including 40,656 invertible boundaries. The receipt reports each census
+and minimum defect rank. Controls check a wrong rank-one boundary, a boundary
+mixing dirty workspace, a nonfaithful stage, and agreement of the dense and
+bit-matrix implementations. These finite domains are not the proof of the
+unbounded theorem.
+
+## Limitations
+
+The stage is the stated direct sum of regular permutation cycles and an
+identity workspace action. The charge is rank(J-I), with the complete
+defect measured on all rows and columns. It does not cover a promised input
+subspace or equate rank with a norm-error guarantee. Native Clifford
+realization and phases, concave recursive price, helper targets, restoration
+outside this identity-stage model, caller, compiler, precision, storage and
+movement have not been established. The selected scientific cold replay,
+Lean and Docker are not run. Independent human and formal proof-kernel
+review are unclaimed.
+
+## Open next questions
+
+- Bind one explicit native noncentral map to this regular-cycle action and
+  derive its actual paid rank profile. First identify the complete native
+  action, including phases and every spectator. This needs a source-specific
+  realization; ordinary rank alone does not price the map.
+- Price a complete caller using a noncentral boundary. First include both
+  boundaries and all productive target changes in its signed invoice.
+  This result supplies a rank floor, not a passing bill or a physical word.
+
+## Verification design
+
+The finite domains bound every loop. The largest exhaustive domain contains
+2^16 binary matrices. Functions are at most one page; failures raise explicit
+exceptions under normal and optimized Python. Python-managed allocation is
+a documented Power of Ten deviation, bounded by the fixed domain sizes.
+No recursion, dynamic code loading, solver, dependency or shared-state write
+is used. Build the Lever shaped the rerunnable exact checker; Prove It Works
+requires complete-matrix checks, including workspace coordinates. Laziness
+Protocol kept this to one self-contained package.

research/cyclic-reversal-rank-tradeoff/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/cyclic-stage-rank-budget/README.md",
+      "usage": "provenance",
+      "git_blob": "85a463f5156254e7a83ccee3d19b5264c9a67ab1",
+      "sha256": "622ba2e38db14ce65a6d3aba282aa1a2ee09a869a07b829b1bc14e86fd3961cd"
+    },
+    {
+      "path": "research/cyclic-stage-rank-budget/FORWARD-TARIFF.md",
+      "usage": "provenance",
+      "git_blob": "a7561f372eb7c63cbd3db21a3f0b4a04d0af8aa7",
+      "sha256": "7abdf4c7f64d8e7f3b7c604ce29c7eeaa04c04e41885483539f6aac3eaf706c0"
+    },
+    {
+      "path": "research/finite-dihedral-cut-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "7ef17c9f10e4c32292f6cb92ea6e19628b1638f1",
+      "sha256": "d8a94457ecb8e79caa22bd66d34b873556c365d2b5847d936b3ab531cc79c04a"
+    }
+  ]
+}

research/cyclic-reversal-rank-tradeoff/TASK.json

@@ -0,0 +1,88 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp ordinary matrix-rank cost and residual-rank tradeoff for noncentral reversal of q regular p-cycles, with arbitrary finite identity-stage dirty workspace, over every field.",
+  "scope_change_reason": "PR6168 explicitly leaves noncommuting native maps open. This takes one specified noncentral boundary before a physical caller search, rather than another fixed coframe itinerary. The result is a scoped boundary lemma, not the card's complete signed-moment construction.",
+  "bottleneck_link": "A changed noncentral boundary can escape the constant-in-stage query model. Its complete boundary rank must be included before attempting a favorable supplier invoice; converting this rank to native child costs is still open.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified sharp boundary result; do not extend into native realization or a larger caller search.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the universal lower bound and attaining partial reflections. verify.py checks finite constructions, independent dense field ranks, all small binary invertible boundaries and semantic controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a specific native noncentral map realize this regular-cycle boundary with a favorable complete paid profile?",
+      "why_it_matters": "Ordinary rank does not by itself price a Gaussian or BIT child.",
+      "first_step": "Identify one literal native action including phases and every spectator, then derive its exact adapter profile.",
+      "blocked_by": "No source-specific native realization is supplied."
+    },
+    {
+      "question": "Can a complete caller using a noncentral cyclic boundary earn a signed-moment gain?",
+      "why_it_matters": "The new boundary allowance may repay an apparent inverse-query saving.",
+      "first_step": "Include both boundaries, restored workspace and productive target changes in one explicit caller invoice.",
+      "blocked_by": "A complete physical word and its native, precision, storage and compiler costs remain open."
+    }
+  ],
+  "verification_environment": {
+    "python": "CPython 3.12.15",
+    "platform": "macOS 27.0.1 arm64",
+    "dependencies": "standard library only",
+    "diagnostics": "Isolated warning-strict normal and optimized Python; explicit runtime invariants; AST inspection. Ruff and pyright were not on PATH.",
+    "allocation_deviation": "Python-managed allocation; fixed domains, at most 131 permutation coordinates, dense matrices at most 26 square, and streamed enumeration of at most 65536 matrices per census."
+  }
+}