diff --git a/research/quinary-repair-lucas-formula/PROOF.md b/research/quinary-repair-lucas-formula/PROOF.md new file mode 100644 index 0000000000..892c526bc6 --- /dev/null +++ b/research/quinary-repair-lucas-formula/PROOF.md @@ -0,0 +1,105 @@ +# A Lucas formula for the resonant disjointness repair + +## Result and dependency boundary + +Let F be a field of characteristic five, h=4k with k>=1, and A_h the +disjointness matrix on the nonempty proper subsets of [h]. Let L_0=2, +L_1=1 and L_(n+2)=L_(n+1)+L_n be the Lucas numbers. Then + +```text +rank_F(I-A_h) = (4*2^h - 2*L_h - 5)/5. (1) +``` + +This is an explicit evaluation of Brian / JoyboyBrian's PR5221 theorem, +not a new proof of its matrix or endpoint-deletion claims. The precise +premises used from that package are: + +1. Its ordinary integer multiplicities c_(h,j) start at (1,0,0,0,0). +2. One step applies the replacements + `1 -> 2; 2 -> 1+3; 3 -> 2+4; 4 -> 3+5; 5 -> 5+5`. +3. For h=4k>=4, its rank is `2^h-1-b_h`, where `b_h=sum_j c_(h,j)`. + +The new step is the arithmetic identity + +```text +b_h = (2^h + 2*L_h)/5 for every even h>=0. (2) +``` + +Combining the cited rank theorem with (2) gives (1). Consequently (1) is +also the exact number of additive scalar rank-one corrections, under the +same algebraic repair model as PR5221. No physical correction cost is inferred. + +## Evaluate the recurrence + +Write c_h=(a_h,b_h',d_h,e_h,p_h), using b_h' to distinguish the second +multiplicity from the total block count b_h. The cited replacements give + +```text +c_(h+1) = (b_h', a_h+d_h, b_h'+e_h, d_h, e_h+2*p_h). +``` + +At even h, only the first, third and fifth multiplicities can be nonzero. +At odd h, only the second, fourth and fifth can be nonzero. This follows +inductively from the displayed update, starting at h=0. + +Let F_0=0, F_1=1 and F_(n+2)=F_(n+1)+F_n. For every even h>=2, + +```text +a_h=F_(h-1), d_h=F_h, b_h'=e_h=0. (3) +``` + +Indeed c_2=(1,0,1,0,0). Two steps send the first and third +multiplicities (a,d) to (a+d,a+2d). The Fibonacci recurrence sends +(F_(h-1),F_h) to (F_(h+1),F_(h+2)) by exactly that map. Induction +proves (3). This Fibonacci pattern is classical; it is not new here. + +The weighted dimension identity is + +```text +sum_(j=1)^5 j*c_(h,j) = 2^h. (4) +``` + +For completeness, each replacement doubles its label's weight: +2=2*1, 1+3=2*2, 2+4=2*3, 3+5=2*4 and 5+5=2*5. +The initial weight is one, so induction gives (4) as an integer identity. + +For even h>=2, subtract (4) from five times the block count and use (3): + +```text +5*b_h - 2^h = 4*F_(h-1) + 2*F_h + = 2*(F_(h-1)+F_(h+1)) + = 2*L_h. +``` + +The identity `L_h=F_(h-1)+F_(h+1)` for h>=1 follows from the two +recurrences and their initial values. At h=0, (2) holds separately since +b_0=1 and L_0=2. This proves (2) for all even h, including its exact +divisibility by five. Substitution in PR5221's rank formula proves (1). + +For example (1) gives 9 at h=4 and 185 at h=8, the inherited examples. +Those evaluations are not new independent matrix-rank checks. + +## Credit and scope + +The source is PR5221 at `ad83478022fed6c1d6a6014096bd8b443e8c9d9a`, +retained in this package's base. Its Jordan rules and endpoint theorem are +cited premises. Its predecessors include Ali Romman / PR4962, Nick +Petalas / PR5173, mikey1201 / PR172, and icekylinx / PR144. + +The modular Jordan/Fibonacci description is classical. See David Benson, +[Commutative Banach algebras, representations of finite groups, and +Hilbert space](https://homepages.abdn.ac.uk/d.j.benson/pages/papers/b/benson/banach-book.pdf), +Section 5.1, page 83, for the same tensor-product rules and Fibonacci +multiplicities. The proof above is self-contained arithmetic once PR5221's +premises are granted. The contribution here is the explicit Lucas-number +specialization to the repository's resonant proper-subset repair rank. +No general literature-priority claim is made. + +This scoped written proof was produced by Nick Petalas. Independent human +and formal proof-kernel review are unclaimed. Apache-2.0. + +This proof does not decide nonresonant ranks, validate PR5221's algebraic +premises, supply a physical caller, or reduce the number of required repairs. +It replaces the recurrence presentation by a closed formula for the same +quantity. All five selected framework assumptions remain. No selected-frontier +change or complete multiplication theorem is claimed. diff --git a/research/quinary-repair-lucas-formula/README.md b/research/quinary-repair-lucas-formula/README.md new file mode 100644 index 0000000000..44d5516fea --- /dev/null +++ b/research/quinary-repair-lucas-formula/README.md @@ -0,0 +1,97 @@ +# A closed Lucas formula for the resonant repair rank + +For every field F of characteristic five and every positive h divisible by +four, the proper-subset disjointness matrix A_h has + +```text +rank_F(I-A_h) = (4*2^h - 2*L_h - 5)/5, +L_0=2, L_1=1, L_(n+2)=L_(n+1)+L_n. +``` + +Claim type: scoped written arithmetic proof with exact finite corroboration, +depending on Brian / JoyboyBrian's [PR5221](https://github.com/CrocSwap/integer-mult-bounds/pull/5221) +rank theorem. The new contribution evaluates its five-state integer recurrence +in closed form. It proves `total_blocks=(2^h+2*L_h)/5` for every even h. +The inherited rank and additive rank-one correction count are unchanged. +See [PROOF.md](PROOF.md) for the complete argument and premise boundary. + +The Fibonacci multiplicities and modular Jordan theory are classical. David +Benson's [Section 5.1, page 83](https://homepages.abdn.ac.uk/d.j.benson/pages/papers/b/benson/banach-book.pdf) +describes the same tensor/Fibonacci pattern. The claimed contribution is its +explicit Lucas specialization to the repository's resonant repair endpoint; +no literature-priority claim is made for the classical ingredients. + +## Evidence and reproduction + +The direct verifier applies the quoted replacements as integer bookkeeping; +it does not import or replay a predecessor scientific verifier. Iterative fast +doubling and a separate binomial sum agree on all 513 Lucas values through +index 512. The literal recurrence agrees with 512 parity/multiplicity formulas, +257 even block-count formulas and 128 resonant rank substitutions. Fifteen +invalid inputs and five named formula mutations are rejected. A generated +stdout receipt binds every package file and the exact recurrence transcript. +No receipt is handwritten or committed. + +From the worktree root, with the local interpreter or any CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -X dev -B research/quinary-repair-lucas-formula/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -X dev -B research/quinary-repair-lucas-formula/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/quinary-repair-lucas-formula +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/quinary-repair-lucas-formula --check-source-history +``` + +Expected direct marker: `PASS_QUINARY_REPAIR_LUCAS_FORMULA`. The registered +commands run both warning-strict normal and optimized modes, each with a +120-second limit. Direct verification needs only these six files and the +standard library. Repository metadata validation additionally needs reachable +Git provenance from [SOURCES.json](SOURCES.json). + +## Limits and implementation bounds + +The all-dimensional conclusion follows from the written arithmetic proof and +the cited rank premise. Bounded replay is corroboration. This contribution +does not audit PR5221's Jordan rules, deletion argument or matrix ranks. +Nonresonant dimensions, physical realization, native calls, routing, dirty +restoration, precision, stock, compiler and outer admission remain outside +scope. All five selected assumptions remain. No new kappa, selected-frontier +change or complete multiplication theorem is claimed. No predecessor scientific +suite, selected cold replay, Lean or Docker run is required or claimed. + +The verifier has no recursion or subprocesses. Its outer domain is 0..512, +fast doubling uses at most ten bit steps and each binomial sum at most 256 +terms. The bookkeeping has five integer counts; its extra terminal update +has total dimension 2^513. Each formula mutation checks at most 128 indices. +Explicit checks remain active under optimization. Power of Ten's fixed-memory +rule has a bounded CPython allocation deviation: arithmetic, six source reads +and JSON serialization allocate managed objects during this terminating run. +All functions are below 60 physical lines. Warning-strict execution and +in-memory syntax checks are the available diagnostics; no separate static +analyzer or formal proof kernel is claimed. + +## Open next questions + +Can a nonadditive physical repair avoid this additive rank obstruction? +First specify its arbitrary-input identity and full preparation, routing and +dirty-restoration invoice. The missing physical caller blocks any supplier +conclusion. No continuation is reserved. + +## Credit and coordination + +This contribution was produced by Nick Petalas. Independent human and formal +proof-kernel review are unclaimed. Apache-2.0. + +Credit Brian / JoyboyBrian PR5221 for the recurrence and rank theorem; Ali +Romman PR4962, Nick Petalas PR5173, mikey1201 PR172 and icekylinx PR144 for +the retained tensor, endpoint and compiler lineage; and David Benson for the +classical modular-representation context. Predecessor files and credits are +unchanged. Exact base-file Git and SHA256 pins are provenance, not live inputs. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370178). +Base `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priorities revision 8, +selected PR6030. This changes the coframe card to a historical arithmetic +side result, as recorded in [TASK.json](TASK.json). PR6469 studies the speed +of a bounded rank evaluator. No evaluator, matrix corpus or implementation +question from that work is extended here. Live handoffs, open PR bodies, +merged formula/object searches and main READMEs were checked. Arbitrary +historical diffs and unpublished work remain coverage limits. diff --git a/research/quinary-repair-lucas-formula/SOURCES.json b/research/quinary-repair-lucas-formula/SOURCES.json new file mode 100644 index 0000000000..d19918ebcc --- /dev/null +++ b/research/quinary-repair-lucas-formula/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/quinary-resonant-disjointness-repair/PROOF.md", + "usage": "provenance", + "git_blob": "8cf640e2063512c24d9fa9c02a77249b3ad852dc", + "sha256": "a0a821bfbbd772e04efd8cfbbde44d8a7ddfbd3986738ea54e70dc0d599b42ef" + }, + { + "path": "research/quinary-resonant-disjointness-repair/README.md", + "usage": "provenance", + "git_blob": "f0ee79a05770a50004032c4b8536182e19264d73", + "sha256": "d8dfd60d785fc353f02d2cfaf20de86a922e98b1e36b9b18fe3d2b1deb8650c8" + } + ] +} diff --git a/research/quinary-repair-lucas-formula/TASK.json b/research/quinary-repair-lucas-formula/TASK.json new file mode 100644 index 0000000000..0d62fdef25 --- /dev/null +++ b/research/quinary-repair-lucas-formula/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Closed Lucas-number evaluation of the ordinary integer recurrence in PR5221, specialized to its resonant characteristic-five proper-subset repair rank.", + "scope_change_reason": "A scoped arithmetic side result replaces a supplier coframe experiment. It cites the existing Jordan and endpoint theorem instead of auditing or extending its matrix implementation.", + "bottleneck_link": "Makes an existing exact additive repair obstruction explicit in the dimension. This is a historical algebraic side result, not a current supplier improvement.", + "budget_minutes": 60, + "stop_rule": "Ship the first exact closed form; do not extend to nonresonant ranks, physical realization or new characteristic families.", + "outcome": "completed", + "evidence": "PROOF.md supplies the all-even recurrence evaluation and cited rank corollary; verify.py corroborates exact arithmetic through index 512 without predecessor scientific replays.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a nonadditive physical repair avoid this additive rank obstruction?", + "why_it_matters": "An explicit count of additive corrections does not bound a changed operator contract.", + "first_step": "Write an arbitrary-input identity and the full paid preparation, routing and dirty-restoration bill.", + "blocked_by": "No physical caller or complete invoice is supplied." + } + ], + "predecessor": { + "pr": 5221, + "author": "JoyboyBrian", + "head": "ad83478022fed6c1d6a6014096bd8b443e8c9d9a", + "premises": "Five-state integer recurrence and rank = 2^h-1-total_blocks for h divisible by four." + }, + "related_account_work": { + "pr": 6469, + "distinction": "A bounded rank-evaluator implementation and replay-time improvement. No evaluator, matrix corpus, performance question or implementation is extended here." + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370178", + "environment": { + "python": "3.12.15", + "implementation": "cpython", + "dependencies": "standard library" + }, + "overlap": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "selected_pr": 6030, + "limitations": "Live metadata, main READMEs and source-specific formula searches do not cover arbitrary historical diffs or unpublished work." + } +} diff --git a/research/quinary-repair-lucas-formula/VERIFY.json b/research/quinary-repair-lucas-formula/VERIFY.json new file mode 100644 index 0000000000..8d416a4b70 --- /dev/null +++ b/research/quinary-repair-lucas-formula/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-X", + "dev", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact recurrence/Lucas/binomial corroboration, domain rejections and five formula mutations." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-X", + "dev", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact recurrence/Lucas/binomial corroboration, domain rejections and five formula mutations." + } + ] +} diff --git a/research/quinary-repair-lucas-formula/verify.py b/research/quinary-repair-lucas-formula/verify.py new file mode 100644 index 0000000000..0477a634f6 --- /dev/null +++ b/research/quinary-repair-lucas-formula/verify.py @@ -0,0 +1,166 @@ +"""Exact arithmetic corroboration of the Lucas specialization; no matrix replay.""" + +from hashlib import sha256 +from math import comb +from pathlib import Path +import json + + +MAX_H = 512 +FILES = ("PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def checked_index(h: int) -> None: + if type(h) is not int or not 0 <= h <= MAX_H: + raise ValueError("index must be an integer between zero and MAX_H") + + +def fibonacci_pair(h: int) -> tuple[int, int]: + """Return F_h,F_(h+1) by bounded, iterative fast doubling.""" + checked_index(h) + a, b = 0, 1 + for bit in bin(h)[2:]: + c, d = a * (2 * b - a), a * a + b * b + a, b = (c, d) if bit == "0" else (d, c + d) + return a, b + + +def lucas(h: int) -> int: + a, b = fibonacci_pair(h) + return 2 * b - a + + +def closed_blocks(h: int) -> int: + checked_index(h) + if h % 2: + raise ValueError("block formula requires an even index") + numerator = (1 << h) + 2 * lucas(h) + value, remainder = divmod(numerator, 5) + require(remainder == 0, "block numerator is not divisible by five") + return value + + +def repair_rank(h: int) -> int: + checked_index(h) + if h < 4 or h % 4: + raise ValueError("rank specialization requires a positive multiple of four") + numerator = 4 * (1 << h) - 2 * lucas(h) - 5 + value, remainder = divmod(numerator, 5) + require(remainder == 0, "rank numerator is not divisible by five") + require(0 <= value <= (1 << h) - 2, "rank outside proper-subset dimension") + return value + + +def literal_step(counts: tuple[int, ...]) -> tuple[int, ...]: + """Apply the cited replacements literally, without a Fibonacci formula.""" + rules = ((1,), (0, 2), (1, 3), (2, 4), (4, 4)) + result = [0] * 5 + for count, replacements in zip(counts, rules, strict=True): + for target in replacements: + result[target] += count + return tuple(result) + + +def binomial_lucas(h: int) -> int: + """Independent sum for cycle matchings; no Fibonacci calls or recurrence.""" + checked_index(h) + if h == 0: + return 2 + return 1 + sum( + comb(h - j, j) + comb(h - j - 1, j - 1) + for j in range(1, h // 2 + 1) + ) + + +def check_formulas() -> dict: + counts = (1, 0, 0, 0, 0) + even_cases, rank_cases, formula_cases = 0, 0, 0 + digest = sha256() + for h in range(MAX_H + 1): + require(sum((j + 1) * c for j, c in enumerate(counts)) == 1 << h, + f"dimension invariant failed at {h}") + require(lucas(h) == binomial_lucas(h), f"Lucas engines disagree at {h}") + if h >= 1: + f, g = fibonacci_pair(h) + first, third = g - f, f + actual = (counts[0], counts[2]) if h % 2 == 0 else (counts[3], counts[1]) + require(actual == (first, third), f"multiplicity formula failed at {h}") + require(counts[1] == counts[3] == 0 if h % 2 == 0 + else counts[0] == counts[2] == 0, f"parity failed at {h}") + formula_cases += 1 + if h % 2 == 0: + require(closed_blocks(h) == sum(counts), f"block count failed at {h}") + even_cases += 1 + if h >= 4 and h % 4 == 0: + expected = (1 << h) - 1 - sum(counts) + require(repair_rank(h) == expected, f"rank substitution failed at {h}") + rank_cases += 1 + digest.update((json.dumps([h, counts], separators=(",", ":")) + "\n").encode()) + counts = literal_step(counts) + require((repair_rank(4), repair_rank(8)) == (9, 185), "inherited examples changed") + return {"indices": MAX_H + 1, "multiplicity_cases": formula_cases, + "even_block_cases": even_cases, "rank_specializations": rank_cases, + "transcript_sha256": digest.hexdigest()} + + +def check_controls() -> dict: + invalid = (-1, MAX_H + 1, True, 1.5, "4", None) + rejected = 0 + for h in invalid: + try: + fibonacci_pair(h) + except ValueError: + rejected += 1 + else: + raise ValueError(f"accepted invalid index {h!r}") + for h in (0, 1, 2, 3, 6, MAX_H + 4): + try: + repair_rank(h) + except ValueError: + rejected += 1 + else: + raise ValueError(f"accepted invalid rank dimension {h}") + for h in (1, 3, MAX_H - 1): + try: + closed_blocks(h) + except ValueError: + rejected += 1 + else: + raise ValueError(f"accepted odd block dimension {h}") + witnesses = {} + for name, exponential, coefficient, constant, denominator in ( + ("wrong_exponential", 3, -2, -5, 5), + ("wrong_lucas_sign", 4, 2, -5, 5), + ("missing_lucas_factor", 4, -1, -5, 5), + ("missing_endpoint", 4, -2, 0, 5), + ("wrong_denominator", 4, -2, -5, 4), + ): + for h in range(4, MAX_H + 1, 4): + wrong = exponential * (1 << h) + coefficient * lucas(h) + constant + if wrong != denominator * repair_rank(h): + witnesses[name] = h + break + require(name in witnesses, f"mutant survived: {name}") + return {"invalid_inputs_rejected": rejected, "mutant_first_counterexamples": witnesses} + + +def main() -> None: + package = Path(__file__).resolve().parent + require(tuple(sorted(p.name for p in package.iterdir() if p.is_file())) == FILES, + "unexpected package file inventory") + results = check_formulas() + controls = check_controls() + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in FILES} + print(json.dumps({"claim_type": "scoped arithmetic proof with cited rank premise", + "results": results, "controls": controls, + "package_sha256": hashes}, sort_keys=True, indent=2)) + print("PASS_QUINARY_REPAIR_LUCAS_FORMULA") + + +if __name__ == "__main__": + main()