diff --git a/research/clean-helper-flag-bound/PROOF.md b/research/clean-helper-flag-bound/PROOF.md new file mode 100644 index 0000000000..a6d2544238 --- /dev/null +++ b/research/clean-helper-flag-bound/PROOF.md @@ -0,0 +1,41 @@ +# Clean helpers in the two-support flag case + +This contribution was produced by Nick Petalas. The argument is a scoped written proof, not a formal proof-kernel result. + +## Statement + +Use PR6338's scalar-idempotent model. Fix `m >= 1`, `t >= 1` and `r >= 0`, and put `n=t+r`. Work in the group algebra `F_2[M_m(Q)]` of the additive group of rational matrices. A paid call is `I_n + ([A]-1)xy^T`, where `rank_Q(A)=1` and `y^T x=1` over `F_2`. The target is `diag([C_1],..., [C_t],1,...,1)` with `C_i` invertible. The last `r` registers are clean and return to identity. A word is an exact formal group-algebra identity; there are no interposed address maps. + +Suppose the rational span of the paid `A` has dimension at most `m+1`, and the relative matrices `C_1^{-1}C_i` have a common complete rational invariant flag. Then the word has at least `mt` paid calls. In particular this applies to lower-triangular invertible data targets. The hypothesis is invariant under common invertible left and right address changes. For diagonal targets the direct coordinate word attains `mt` within span `m`, so the bound is sharp for the class. It does not claim that a direct word for every prescribed set of targets has span at most `m+1`. + +## Two-dimensional lemma with zero helper blocks + +Suppose all data target exponents in a two-dimensional block are invertible lower-triangular matrices, and all helper exponents in that block are zero. Let `U` denote calls whose frame has nonzero upper-right entry. Project every frame to that entry. The target becomes identity, including the helper entries. Write the associated scalar columns and rows as `X,Y`, with ranks `r_X,r_Y` over `F_2`. PR468's product factorization gives + + r_X + r_Y <= U. (1) + +For `i=1,2`, let `l_i` count the other calls whose `i`th diagonal entry is nonzero. Project onto that diagonal entry. Its target-minus-identity has rank exactly `t` over the fraction field of the Laurent group algebra: the data diagonal entries are nonzero and the helpers are zero. The factorization bounds its rank by both scalar spans. The upper calls span at most `r_X` columns and `r_Y` rows; the other relevant calls contribute at most `l_i` each. Therefore + + t <= r_X + l_i, t <= r_Y + l_i. (2) + +A rank-one lower-triangular two-by-two frame has at most one nonzero diagonal entry. Thus `l_1+l_2 <= E-U`, where `E` is the number of calls assigned to this block. Adding (2) for both coordinates and using (1) gives + + 4t <= 2(r_X+r_Y+l_1+l_2) <= 2E, + +so `E >= 2t`. This is the new zero-helper adaptation of PR468's flag count. It does not assume that a clean helper's zero block is invertible. + +## Apply the lemma + +PR6338 proves the claimed lower bound for span at most `m`, and for span `m+1` with normalized support intersection `|K| != 2`. We cite those cases rather than re-prove them. For the remaining case, use the normalization in PR468 and PR5988: the span is block upper triangular after a common row and column permutation, with one two-dimensional diagonal block and `m-2` one-dimensional blocks. A rank-one frame has at most one nonzero diagonal block, so each call can be assigned to at most one block. This is an address-space fact, independent of the number of registers. + +All data target diagonal blocks are invertible, while all clean helper blocks are zero. The common flag of the relative data targets passes to each invariant subquotient of the block filtration: intersect the common flag with each invariant subspace and pass to the quotient. It follows that common invertible left and right changes within the two-dimensional block make all data target blocks lower triangular. Those changes preserve rank, the formal identity, and zero helper blocks. The lemma above gives at least `2t` calls in that block. Each one-dimensional block needs at least `t` by its diagonal projection and scalar rank. The disjoint assignments sum to `2t + (m-2)t = mt`. + +The exact finite checks in `verify.py` exercise the formal output identity, a nontrivial upper-entry cancellation, the scalar-span inequality on short words and a missing-cancellation control. They are corroboration, not a substitute for the argument. + +## Dependencies and limits + +Eumemic's PR288 supplies the model. Ali Romman's PR468 supplies normalization, projection and the original flag inequality. PR5988 supplies the all-dimensional support split. Unpaidmoon's PR6338 supplies the clean-helper question and all non-two-support cases. These are cited inputs, not results rechecked here. + +Ali Romman's PR4961 already proves the stronger unrestricted-span nine-call bound for three lower-triangular `3 x 3` data targets with one returned register. It contains that particular case of the present statement. The contribution here is the all-dimension, arbitrary-data-count and arbitrary-clean-helper-count small-span flag bound, not the three-data one-helper instance. Unpaidmoon's PR4118 gives a partial bound for arbitrary dirty auxiliaries at the same three-dimensional span; its unresolved five-call block case does not assert this general common-target-flag result. + +Targets without a common rational flag, nonzero dirty helper exponents in the two-block, span above `m+1`, free address maps, physical implementation, native and caller costs, and any complete multiplication theorem remain outside the statement. No new kappa is claimed. diff --git a/research/clean-helper-flag-bound/README.md b/research/clean-helper-flag-bound/README.md new file mode 100644 index 0000000000..bb54fca3cc --- /dev/null +++ b/research/clean-helper-flag-bound/README.md @@ -0,0 +1,25 @@ +# Clean helper registers preserve the common-flag span bound + +A scoped written proof shows that, in the rational scalar-idempotent model of PR6338, `t` invertible data targets and any number of clean identity helpers need at least `mt` paid calls when the frame span has dimension at most `m+1` and the data-target ratios share a complete rational flag. Diagonal data targets attain the bound with `mt` calls and span `m`. The result extends PR6338's non-two-support cases to its remaining two-support case under the common-flag hypothesis. It gives no new κ. + +The new step is a flag count with zero helper blocks. The upper-entry projection has identity output, while the diagonal projections have rank `t`. Their scalar rank inequalities force at least `2t` calls on the two-dimensional block. The one-dimensional blocks each need `t`. [PROOF.md](PROOF.md) gives the argument and states the exact hypotheses. The executable finite examples corroborate it; they do not formally certify the universal proof. + +From the repository root, with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/clean-helper-flag-bound/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/clean-helper-flag-bound/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clean-helper-flag-bound +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clean-helper-flag-bound --check-source-history +``` + +Use a local CPython 3.12 executable in place of the absolute path on another machine. The checks use exact finite group-algebra arithmetic, not a physical bit supplier. Common-flag hypotheses, clean helper restoration, and the span bound are essential parts of the claim. No complete multiplication theorem, physical schedule, native or compiler admission, or independent human or formal proof-kernel review is claimed. + +## Open next questions + +- Can the two-dimensional block bound be proved without a common rational flag? Start with two data matrices whose relative matrix has irreducible quadratic characteristic polynomial and keep helper outputs at zero. The upper-entry projection then need not have identity output. +- Can dirty monomial helper exponents be admitted when their upper-entry projections vanish? Start with the same inequalities and account for their potentially nonzero diagonal projections. Arbitrary helper blocks can make the upper projection nontrivial. + +## Credit + +This contribution was produced by Nick Petalas. Eumemic's PR288 supplies the model; Ali Romman's PR468 supplies the normalization, projections and original flag inequality. PR5988 supplies the all-dimensional support split. Unpaidmoon's PR6338 supplies the clean-helper question and the non-two-support cases. Ali Romman's PR4961 already proves the stronger unrestricted-span result for three lower-triangular 3-by-3 data targets and one returned register. Unpaidmoon's PR4118 proves a partial span-four result for dirty auxiliaries. These results are inputs, not audit targets. Apache-2.0. diff --git a/research/clean-helper-flag-bound/SOURCES.json b/research/clean-helper-flag-bound/SOURCES.json new file mode 100644 index 0000000000..2bbdffe550 --- /dev/null +++ b/research/clean-helper-flag-bound/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/span-lemma-every-dimension/PROOF.md", + "usage": "input", + "git_blob": "5f160fa562dbec44d7f5c388ffc9d0a8972223d3", + "sha256": "37aa8abd29629f8945710a0f675f3ad0a6241436d4e584b2e4741b36aead9f12" + }, + { + "path": "research/span-lemma-idle-helpers/PROOF.md", + "usage": "input", + "git_blob": "0a52d77f4ce557ad54f452c4a2c78ed130298216", + "sha256": "a0077416f35a7545dfe512ba3017b2d764d83af949583cfaaf5a30cb07001e4e" + } + ] +} diff --git a/research/clean-helper-flag-bound/TASK.json b/research/clean-helper-flag-bound/TASK.json new file mode 100644 index 0000000000..b6905c3246 --- /dev/null +++ b/research/clean-helper-flag-bound/TASK.json @@ -0,0 +1,75 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "In the rational scalar-idempotent model, t invertible data targets with a common rational flag and any number of clean identity helpers need at least m*t paid calls when the paid-frame span has dimension at most m+1. Diagonal data targets attain the bound.", + "scope_change_reason": "The card permits a larger register count. This addresses PR6338 open question 1, retaining its alphabet and adding clean helpers to the previously excluded two-support flag case. A common flag is required by the proof.", + "bottleneck_link": "The result rules out a clean-helper escape from the small-span BIT obstruction for common-flag targets. It does not implement a native supplier or price physical costs.", + "budget_minutes": 60, + "stop_rule": "Stop after the two-support flag proof and exact finite controls; do not extend to targets without a common flag.", + "outcome": "partial", + "evidence": "PROOF.md proves the two-dimensional clean-helper flag inequality and cites the retained address and non-two-support reductions. verify.py checks formal identities and scalar spans for bounded examples.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the bound hold without a common rational flag?", + "why_it_matters": "It is the unproved remainder of the two-support clean-helper question.", + "first_step": "Consider two data targets whose relative 2x2 block has irreducible quadratic characteristic polynomial.", + "blocked_by": "The upper-entry projection need not have identity output." + }, + { + "question": "Can the argument cover nonzero dirty helper exponents with zero upper projection?", + "why_it_matters": "Dirty helpers are a broader register contract.", + "first_step": "Track helper contributions in both diagonal rank projections.", + "blocked_by": "General helper exponents need not project to zero above the diagonal." + } + ], + "question_source": { + "pr": 6338, + "author": "unpaidmoon", + "question": "Open next question 1: extend the two-support flag bound to clean identity helper registers." + } +} diff --git a/research/clean-helper-flag-bound/VERIFY.json b/research/clean-helper-flag-bound/VERIFY.json new file mode 100644 index 0000000000..8a8768de2c --- /dev/null +++ b/research/clean-helper-flag-bound/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md", + "research/span-lemma-every-dimension/PROOF.md", + "research/span-lemma-idle-helpers/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact short upper-projection identities, scalar-span bounds, clean restoration and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same finite controls with Python assertions disabled." + } + ] +} diff --git a/research/clean-helper-flag-bound/verify.py b/research/clean-helper-flag-bound/verify.py new file mode 100644 index 0000000000..287aea3a13 --- /dev/null +++ b/research/clean-helper-flag-bound/verify.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Exact finite controls for the clean-helper flag-count proof.""" +from itertools import product + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank(vectors, n): + basis = [0] * n + for value in vectors: + x = value + for bit in range(n - 1, -1, -1): + if x & (1 << bit): + if basis[bit]: + x ^= basis[bit] + else: + basis[bit] = x + break + return sum(bool(x) for x in basis) + + +def step(state, frame, x, y): + """Multiply a formal group-algebra matrix by I+([frame]+1)xy^T.""" + result = dict(state) + for exponent, rows in state.items(): + term = tuple(y if (row & x).bit_count() % 2 else 0 for row in rows) + shifted = tuple(a + b for a, b in zip(exponent, frame)) + for key in (exponent, shifted): + before = result.get(key, (0,) * len(rows)) + after = tuple(a ^ b for a, b in zip(before, term)) + if any(after): + result[key] = after + else: + result.pop(key, None) + return result + + +def word(n, frames): + state = {(0,) * len(frames[0][0]): tuple(1 << i for i in range(n))} + for frame, x, y in frames: + state = step(state, frame, x, y) + return state + + +def projectors(n): + return [(x, y) for x in range(1, 1 << n) for y in range(1, 1 << n) + if (x & y).bit_count() % 2 == 1] + + +def short_identity_controls(): + ps = projectors(3) + require(len(ps) == 28, "wrong scalar projector count") + total = 0 + identities = 0 + letters = [(sign, x, y) for sign in (-1, 1) for x, y in ps] + for length in range(1, 4): + for choices in product(letters, repeat=length): + frames = [((sign,), x, y) for sign, x, y in choices] + state = word(3, frames) + total += 1 + if state == {(0,): (1, 2, 4)}: + identities += 1 + rx = rank([x for _, x, _ in choices], 3) + ry = rank([y for _, _, y in choices], 3) + require(rx + ry <= length, "identity span inequality") + require(identities > 0, "missing identity controls") + return total, identities + + +def example_controls(): + e11, e22, e12 = (1, 0, 0, 0), (0, 0, 0, 1), (0, 1, 0, 0) + direct = [(e11, 1, 1), (e22, 1, 1), (e11, 2, 2), (e22, 2, 2)] + upper = (e12, 3, 1) + inverse = (tuple(-v for v in e12), 3, 1) + calls = direct[:2] + [upper, inverse] + direct[2:] + expected = {(1, 0, 0, 1): (1, 2, 0), (0, 0, 0, 0): (0, 0, 4)} + require(word(3, calls) == expected, "restored output or upper cancellation") + require(word(3, calls[:3] + calls[4:]) != expected, "missing upper call accepted") + require(word(3, direct) == expected, "direct sharp fixture") + e21 = (0, 0, 1, 0) + asymmetric = direct + [(e21, 2, 2)] + expected_asymmetric = {(1, 0, 0, 1): (1, 0, 0), + (1, 0, 1, 1): (0, 2, 0), + (0, 0, 0, 0): (0, 0, 4)} + require(word(3, asymmetric) == expected_asymmetric, "triangular targets") + return len(calls), len(direct) + + +def main(): + total, identities = short_identity_controls() + with_pair, direct = example_controls() + print(f"PASS_CLEAN_HELPER_FLAG_BOUND short_words={total} " + f"identity_words={identities} cancellation_calls={with_pair} " + f"sharp_calls={direct} controls=4") + + +if __name__ == "__main__": + main()