diff --git a/research/selected-live-row-divisor/PREDECESSORS.json b/research/selected-live-row-divisor/PREDECESSORS.json new file mode 100644 index 0000000000..c1e95bf6ae --- /dev/null +++ b/research/selected-live-row-divisor/PREDECESSORS.json @@ -0,0 +1,62 @@ +[ + { + "pr": 2195, + "commit": "3a1cf78a1ba6322129e42d80c50d21765524d612", + "source_path": "research/selected-bit-local-ring-sweeps/PROOF.md", + "path": "sources/pr2195/PROOF.md", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3a1cf78a1ba6322129e42d80c50d21765524d612/research/selected-bit-local-ring-sweeps/PROOF.md", + "sha256": "846c59440cc99e28bae93ad2af99525bc769de29368080071b8427141215b4f7", + "git_blob": "4330de85dd9862ed15d84ab917887d249753df99", + "bytes": 16491 + }, + { + "pr": 2195, + "commit": "3a1cf78a1ba6322129e42d80c50d21765524d612", + "source_path": "research/selected-bit-local-ring-sweeps/verify.py", + "path": "sources/pr2195/verify.py", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3a1cf78a1ba6322129e42d80c50d21765524d612/research/selected-bit-local-ring-sweeps/verify.py", + "sha256": "c0b17516fc772d297fddbc5d779d704e5512ecb1405374aaeaf4a17ce69b429e", + "git_blob": "7f4629851064be3a9b5c84ca9be02ae85415b035", + "bytes": 3904 + }, + { + "pr": 2234, + "commit": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f", + "source_path": "research/selected-bit-recursive-closure/PROOF.md", + "path": "sources/pr2234/PROOF.md", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/d047ef86fbc5b1614d3d8e2b8d3441413beab73f/research/selected-bit-recursive-closure/PROOF.md", + "sha256": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344", + "git_blob": "6c410cab5713979214a45835091fbeb9ee9b8531", + "bytes": 23425 + }, + { + "pr": 2234, + "commit": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f", + "source_path": "research/selected-bit-recursive-closure/NOTICE.md", + "path": "sources/pr2234/NOTICE.md", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/d047ef86fbc5b1614d3d8e2b8d3441413beab73f/research/selected-bit-recursive-closure/NOTICE.md", + "sha256": "c144e34c24470ca53df77527b9687ae9b345a4d88a506d839312ca26584cfe79", + "git_blob": "a5ccfbecbd225d4b63d9ce85edb2fac90f37147c", + "bytes": 3546 + }, + { + "pr": 2195, + "commit": "3a1cf78a1ba6322129e42d80c50d21765524d612", + "source_path": "research/selected-bit-local-ring-sweeps/owner_packets.py", + "path": "sources/pr2195/owner_packets.py", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/3a1cf78a1ba6322129e42d80c50d21765524d612/research/selected-bit-local-ring-sweeps/owner_packets.py", + "sha256": "8d49d9830cb482324668219e9065440760dded8ac5f68865bf4c965fd4076d34", + "git_blob": "70d5fcc0c89028bc2c2f4eb8cf8336ba15fa6cad", + "bytes": 10091 + }, + { + "pr": 2234, + "commit": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f", + "source_path": "research/selected-bit-recursive-closure/recursive_plan.py", + "path": "sources/pr2234/recursive_plan.py", + "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/d047ef86fbc5b1614d3d8e2b8d3441413beab73f/research/selected-bit-recursive-closure/recursive_plan.py", + "sha256": "49a6bbc8b942064a58e646585efb44c2c6b3ca1abc8d1e49193d9b8a3c708b74", + "git_blob": "4396434ed4d8013862fdc6889e8e5e5d3061654c", + "bytes": 6715 + } +] diff --git a/research/selected-live-row-divisor/README.md b/research/selected-live-row-divisor/README.md new file mode 100644 index 0000000000..a0303f03eb --- /dev/null +++ b/research/selected-live-row-divisor/README.md @@ -0,0 +1,235 @@ +# Exact compatibility of live-row and physical-slot reserves + +This is an independently checked **corollary of Jose Manuel's PR2195/PR2234 +live/work separation**, with an explicit row codec and a written all-depth +proof. It is not a new separation mechanism or an unconditional supplier. +PR2195 already calls its least-common-multiple layout an overreserve. + +For the same fixed complete live-packet format, replace the sufficient divisor + +``` +K_lcm = lcm(28416,28425) * |GL64(F_q)| * q^(4096(w-1)) +``` + +by + +``` +B = 28416 * |GL64(F_q)| * q^(4096(w-1)). +``` + +At coarse depth D, the reserve changes from `K_lcm^D` to `B^D`, a factor +`9475^D`. This is a row-divisibility reduction. **All private/selector work, +COPY/ERASE operations, occupied volume and parking charges remain required.** +The nine physical work slots are not turned into live input or deleted. +The per-volume paid profile, selected invoice and kappa are unchanged. + +The new format need not satisfy a consumer's old P-based divisor. The exact +acceptance gate is `9475^D | t` for incoming live-format stock `t B^D`. +Consequently **the old reserve remains minimal when both fixed formats are +required**. Using the smaller reserve requires a caller admitting the complete +live-packet contract below. The +literal historical `row_layout` test still asserts the old constants and is +retained unchanged. This package does not substitute its codec into a complete +selected recursive machine. + +## Source binding and exact delta + +Scientific base: `0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2`, priority revision 4. +Selected record SHA256: +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. + +- [PR2195](https://github.com/CrocSwap/integer-mult-bounds/pull/2195), head + `3a1cf78a1ba6322129e42d80c50d21765524d612`, PROOF section 5 and + `owner_packets.py:151`: `W=28416`, `P=W+9=28425`, private work outside the + row split, packet volume `V/(WN)`, and the old surplus quotient `9475`. +- [PR2234](https://github.com/CrocSwap/integer-mult-bounds/pull/2234), head + `d047ef86fbc5b1614d3d8e2b8d3441413beab73f`, PROOF sections 5-8: + recursive complete-row contract, four work buffers, depth and parking bill. + `recursive_plan.py` is retained as inert evidence of the macroplan boundary. + +The six copied files and their Git blobs/SHA256s are in `PREDECESSORS.json`. +The primary checker authenticates its manifest and every byte before use; +it never imports or executes predecessor code. The source audit covers these +named files, not every linked implementation. Source2195 explicitly retained +P-divisibility as compatibility, without identifying P-slot input with scratch. +Our delta is the replacement codec, its exact full-depth implication, controls, +and independent review of the resulting interface boundary. + +PR2084/2120 supplied conditional parent-stock coefficients; PR2324/2343 supplied +cutoffs for their stipulated reserves. Their results are neither recomputed nor +changed. This package does not identify new selected fourteen-stage constants. + +## Conditional full-depth theorem + +For integers `W,N,H>=1`, set `B=WNH`. A complete live packet has coordinate +range `[W] x [N] x [H]`; `[a]` means the integers from 0 through a-1. +Fix an integer maximum active depth `D>=0` and multiplicity `t>=1`. +Assume the following contracts, independently of a P-based row format: + +1. A parent can interpret the fixed source word on `[W] x [N] x [H] x [U]` + for every positive integer U. All original rows carry arbitrary live payload. + Private, source, target and route copies are additional paid work. No + arbitrary live coordinate is cleared to supply that work. +2. Routes and descriptors preserve unused U and exposed ancestors. A child's + existence, requested width and coefficients may depend on ancestors but do + not select or inspect its fresh row fields. Each child receives its complete + fresh range at every fixed ancestor value, including every parent high value. +3. A child with depth bound `D'<=D-1` restores its row and complete spectators + pointwise, closes its local work and returns its heads. Leaves accept every + positive integer row multiplicity; width zero is identity. The source's + chronological, endpoint, parking and uniform primitive contracts are retained. + +Then `t B^D` rows are sufficient for the entire depth-D live-row construction. +The row codec is a bijection + +``` +[t B^D] <-> ([W] x [N] x [H])^D x [t]. +``` + +**Proof.** At D=0 the row range is `[t]` and no packet is exposed. At D>=1, +ordinary Euclidean division gives + +``` +[t B^D] <-> [W] x [N] x [H] x [t B^(D-1)]. +``` + +For every fixed family, low class and high value, the last coordinate is the +same complete range. For a child of depth D', it equals +`[t' B^D']`, with `t'=t B^(D-1-D')` a positive integer. Apply the induction +hypothesis to that child. It restores the row and all exposed fields, so the +next sibling reuses the same range; reserves do not multiply across sequential +calls. Inverse decoding restores the parent's row exactly. Iterating division +gives the displayed codec. Constant-weight descriptor resets do not reset the +consumed row depth or discard an exposed field. This proves the conditional +all-depth implication. It does not establish the physical premises. + +**Fixed-format minimum.** A range that is the product of D complete independent +W,N,H layers and a nonempty integer leftover has cardinality `t B^D`. Hence +`B^D` is its least positive cardinality. This is only a minimum in the stated +product format. It is not a lower bound for adaptive, correlated, variable-depth +or otherwise changed row encodings, nor for arbitrary reversible algorithms. + +**Exact two-format gate.** For any additional integer `P>=1`, + +``` +(PNH)^D | t(WNH)^D <=> (P/gcd(P,W))^D | t. +``` + +Cancel `(NH)^D`, write `P=ga`, `W=gb` with `g=gcd(P,W)` and coprime a,b, +and cancel `g^D`. The question is `a^D | t b^D`; Euclid's lemma makes this +equivalent to `a^D | t`. At D=0 both sides hold for every positive t. +Since every live-format cardinality is `t B^D`, its smallest positive value +also accepted by the fixed physical format is + +``` +lcm((WNH)^D,(PNH)^D) = (lcm(W,P)NH)^D = K_lcm^D. +``` + +For the selected constants, `g=3`, `a=9475`, `b=9472`. An unchanged +depth-D physical-format consumer therefore accepts `t B^D` exactly when +`9475^D | t`; in particular t=1 fails at every positive depth. This is the +full depth-D divisor, not just one PNH factor at a deeper depth. The old +reserve is an overreserve relative to the live-only format and is minimal +for the two-format cardinality promise. This gate establishes no paid +adapter, joint ownership or physical implementation. + +**Selected depth.** The source recurrence is `D(n)=0` below 64 and +`D(n)=1+D(42 floor(n/64))` otherwise. The map `42 floor(n/64)` is monotone +and strictly below n at internal nodes. Strong induction therefore proves D +monotone. For every allowed rank `1<=r<=42`, and for fallback widths at most +`floor(n/64)`, child depth is at most `D(n)-1`. Thus the theorem applies at +every finite n under the retained caller contracts. No finite depth census +is being extrapolated to prove this fact. + +For `N=|GL64(F_q)|`, `H=q^(4096(w-1))`, every fixed eligible odd prime q and +integer w>=1 gives the stated B. The high matrix fibers remain present. Since +`284162^80`, the predecessor +per-level upper envelope `log_q B<4096w+1<=4097w` still holds. No sharper +coefficient, fit cutoff or moment is claimed. + +## Padding, arbitrary payload and paid work + +For a genuine row range Q>=S, where S=B^D, pad to +`R=ceil(Q/S)S`. Then `Q<=R=0`. The changing +format consists of a complete original row interval of cardinality `t B^D`. +Every original row carries arbitrary live payload; no original row is assumed +zero. At an active node the format consumes one independently complete +`[W] x [N] x [H]` layer. Children may require any depth `D'<=D-1`. + +Assume the completed operations have these boundary contracts: + +1. Packet primitives accept arbitrary complete unused ranges of the stated + size, and leaves accept every positive row multiplicity. A call accepts + all payload values, including correlated dirty values. This is an explicit + changed-interface hypothesis: an old API promising only `K^D` multiples + does not automatically satisfy it for the smaller reserve. +2. Current-header routes fix the unused row coordinate. Generated descriptors + read only exposed ancestors, not the child's fresh family, matrix or + leftover coordinates. +3. A child acts on the entire packet with old high coordinates as complete + spectators; it restores the row and spectator coordinates pointwise. +4. Private copies, selectors and other work are allocated separately, with + their full source shapes, preparation, scans, parking, cleanup and return + costs. They are not relabelled arbitrary input rows to be zeroed. + +At `D=0`, the leftover row interval has cardinality `t` and no fresh layer is +needed. At `D>=1`, mixed-radix decoding gives the exact bijection + + [t B^D] = [W] x [N] x [H] x [t B^(D-1)]. + +For a child of depth `D'<=D-1`, write + + U=t B^(D-1) = (t B^(D-1-D')) B^D'. + +The first factor is a positive integer, so the child receives an admissible +complete range with multiplicity `t B^(D-1-D')`. For every fixed old high +coordinate, this is the identical whole range `[U]`. Old high values remain +complete spectators of the one child call; they are not a separate loop of +child invocations. Induct on the remaining depth. The route and restoration +hypotheses preserve the complete range after each call, so sequential reuse +is permitted. After `k` active levels, the unused cardinality is exactly +`t B^(D-k)`, with no compatibility-factor residue. + +This proves sufficiency at every finite depth. It supplies fresh cardinality +only; all completed-child, causality, ownership and work contracts remain +hypotheses. It is a modification of the source's format, not an invocation of +a theorem whose declared input still requires the larger divisor. + +For the source's width function, `D(n)=0` below 64 and +`D(n)=1+D(42 floor(n/64))` otherwise. Its argument is strictly smaller than +`n`; induction makes `D` well-defined and monotone. For an active parent, +`n'<=42 floor(n/64)` implies `D(n')<=D(n)-1`. The same inequality applies to +positive fallback widths at most `floor(n/64)`. This supplies the depth +hypothesis above without claiming anything about a different recurrence. + +For minimality, suppose a positive reserve `S` itself has the fixed complete +format of `D` independent `W,N,H` layers and a nonempty integral leftover +range `[u]`. Cardinalities force `S=B^D u`; therefore `B^D` divides `S` and +`S>=B^D`. The displayed construction attains equality with `u=1`. The same +conclusion applies to a reserve promised to work for every multiplicity, +because that promise includes `t=1`. + +This does not prove minimality among compressed, reused, correlated, adaptive +or non-Cartesian layouts. A promise of only a shorter actual execution path +need not consume `D` layers. For one specially chosen multiplicity `t`, its +factors might supply some required stock; uniformity over all positive `t` +must not be dropped from the reserve interpretation. + +## Volume, costs and the physical format + +A complete fixed-family/low packet includes every high and unused coordinate. +If `c` is the payload volume per original row, then + + V=c W N H U, v=c H U=V/(WN). + +The separate four-buffer boundary and source parking expression therefore +retain their forms at the actual volume: + + occupied <= V+4v, + parking <= 5V+19v+9(W+4)-2, + +excluding the child and retaining all separately stated control and dispatch +charges. This algebra does not verify that the source's machine implements +those bounds, or evaluate a selected numerical invoice. It does not erase +the work bill or assert a numerical runtime saving at a different `V`. + +For `W=28416` and `P=28425`, `gcd(W,P)=3` and + + lcm(W,P)=269241600, + lcm(W,P)/W=9475, + lcm(W,P)/P=9472. + +Consequently the historical stock is `K^D=9475^D B^D`. At depth one and +`t=1`, `PNH` cannot divide `B=WNH`, since cancellation would require `P|W`. +This remains true for the actual positive selected `N,H`; no small-field +approximation is involved in that cancellation. The exact condition for an +unchanged depth-`D` physical format is stronger and can be characterized fully. + +### Exact acceptance by an unchanged physical format + +For any positive `W,P,N,H,t` and integer `D>=0`, + + (P N H)^D divides t (W N H)^D + if and only if + (P/gcd(P,W))^D divides t. + +To prove this, cancel the common positive factor `(NH)^D` from the first +divisibility statement. Set `g=gcd(P,W)`, `a=P/g`, and `b=W/g`, so that +`gcd(a,b)=1`. Cancelling `g^D` leaves `a^D | t b^D`. The powers `a^D` and +`b^D` are coprime, so Euclid's lemma gives `a^D | t`. The converse follows +by multiplication. At `D=0` both sides say `1|t`. + +Every cardinality compatible with both fixed complete formats must be a +positive multiple of `B^D`. The equivalence proves that its least possible +multiplicity is `(P/g)^D`; hence its least positive cardinality is exactly + + lcm((W N H)^D, (P N H)^D) + = (lcm(W,P) N H)^D + = K^D. + +Thus the historical reserve is minimal for simultaneous cardinality +compatibility with both fixed depth-`D` formats. Calling it an overreserve +is relative to the changed live-only format, not to that two-format promise. +The smaller reserve is usable only when the physical-format consumer is +removed or its additional premise is proved unnecessary, or when the incoming +multiplicity independently passes the exact gate above. + +For the selected constants, `b=9472` and `a=9475` are coprime. Therefore an +unchanged depth-`D` physical consumer accepts `t B^D` exactly when +`9475^D | t`. In particular `t=1` fails at every positive depth. The statement +concerns the full depth-`D` physical power; accidental divisibility by only +one `PNH` factor at a larger depth would not establish that contract. +This acceptance gate is a cardinality condition, not a proof of an adapter, +simultaneous layout ownership, charged work, or a completed physical caller. + +For an arbitrary incoming cardinality `R>=S=B^D`, rounding upward to +`ceil(R/S) S` is less than `2R`. Removing padding is valid once the completed +endpoint restores every row coordinate and performs the desired action +within each row. Intermediate permutations may mix genuine and padded rows; +premature restriction can destroy genuine payload. Pointwise restoration is +a sufficient condition. Merely preserving a multiset of row values does not +establish it. + +## Independent finite evidence + +Reproduce from the repository root: + +```sh +python3 -I -O -B research/selected-live-row-divisor/independent.py +``` + +Normal and optimized runs passed under Python 3.14.6; the first optimized run +took approximately 1.1 seconds. The +checker uses Python's Cartesian-product enumeration as an oracle independently +of its integer encoding and decoding routines. Its complete finite domains are: + +* `W,N,H in {1,2,3}`, `D in {0,1,2,3}`, `t in {1,2}`: 216 formats, + 148,929 rows and 585,945 exposed-prefix/unused-suffix checks; 648 complete + old-high/child-depth domains and 162 volume/parking identities. +* Six fully enumerated payload fixtures `(W,N,H,D,t)`: + `(2,3,2,2,1)`, `(2,2,3,3,1)`, `(3,2,2,2,2)`, `(1,3,2,3,1)`, + `(2,1,3,3,1)`, `(3,2,1,3,2)`. They contain 24,192 distinct formal input + symbols, including an extra complete spectator and two binary data + coordinates. Literal suffix cycles, data interchange and inverse cycles + give 69,120 pointwise endpoint comparisons at 30 complete child boundaries. + Equality on distinct symbols is an exact permutation identity, hence it + allows every substitution of correlated Boolean payload values. +* Widths `0..4096`: 169,386 positive rank-child checks and 129,088 fallback + checks. These are finite checks using the source recurrence directly, not + an independently derived depth algorithm. The Cartesian-product and + distinct-symbol tests provide the independent layout/endpoint coverage. +* 116 complete padding cases for stocks `{1,2,3,4,6,8,12,18}` and each + `R` from `S` through `3S`, plus 108 finite base/depth cardinality cases. +* 18,000 exact acceptance equivalences for `W,P in {1,...,12}`, + `D in {0,...,4}`, `t in {1,...,25}`, using `N=2,H=3` in the direct + full-power divisor. A direct ascending search, independent of the lcm + formula, establishes all 720 least common reserves in that domain. + At the actual selected `W,P`, depths `0..8` test acceptance of `t=9475^D` + and rejection of the positive `t=9475^D-1` boundaries. The depth-zero + latter value is `t=0`, explicitly outside the positive-multiplicity domain; + it is not counted as a failed divisibility case. + +Eleven controls distinguish: omitting high stock at the first level; omitting +it only in descendants despite a successful root decode; absent physical-slot +divisibility in a small model and at the selected depth-one constants; COPY +pollution from arbitrary dirty private input; noninjective clearing of that +input; row-multiset preservation without pointwise restoration; spectator +drift; removal of padding before restoration; applying the factor-two bound +without `R>=S`; and allowing a child the unconsumed parent depth. + +The payload fixture is a generic complete-call probe, not the selected scalar +word, GL64 cover, weighted residual or physical tape machine. The finite tests +do not establish every-parameter claims; the written arguments above do. +Neither is a formal-kernel proof. + +## Open obligations + +The parent package owns exact predecessor-file authentication, selected-record +status and publication. Separate machine/circuit review would be needed to +replace the stock in an actual caller, check all generated descriptor paths +and separately allocated work, and retain pointwise restoration at every +recursive boundary. No physical `P`-slot contract, selected finite invoice, +ordinary-supplier implementation, multiplication exponent or new kappa is +certified by this review. + +This file and the independent checker are Apache-2.0, with substantial OpenAI +Codex assistance; predecessor attribution and source-specific licenses remain +with the inherited materials. diff --git a/research/selected-live-row-divisor/SOURCES.json b/research/selected-live-row-divisor/SOURCES.json new file mode 100644 index 0000000000..392737aa2a --- /dev/null +++ b/research/selected-live-row-divisor/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + } + ] +} diff --git a/research/selected-live-row-divisor/TASK.json b/research/selected-live-row-divisor/TASK.json new file mode 100644 index 0000000000..b244f5e655 --- /dev/null +++ b/research/selected-live-row-divisor/TASK.json @@ -0,0 +1,139 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #1956/#1965/#1990 in the batch review and the stock-audit source boundary. Its actual selected coefficient remains uncomputed.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one of the fourteen recorded stages, pin its producer, and derive the parent reserve and depth coefficient. Stop with a precise source-level missing lemma if that coefficient cannot yet be bounded; do not rerun the already checked headroom arithmetic as a new result.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990" + ] + }, + "scope_status": "changed", + "actual_scope": "Conditional minimum divisor and exact physical-format compatibility gate for PR2195/PR2234 complete live packets with separately paid private work.", + "scope_change_reason": "The live overlap already covers first-stage coefficient and cutoff arithmetic. This follows the explicit pending caller layout: replace its compatibility overreserve only under a complete live-packet API, preserving every work and child contract. It is a corollary with a new codec and independent review, not a selected fourteen-stage stock identification.", + "bottleneck_link": "Makes the precise row-format acceptance gate inspectable for the pending selected BIT caller; prevents confusing fewer divisible live rows with free private memory or automatic old-format compatibility.", + "budget_minutes": 60, + "stop_rule": "Stop after this conditional layout/compatibility lemma and exact controls. No new cutoff, profile, root, global compiler or selected-frontier work; final quarter reserved for verification and preservation.", + "outcome": "completed", + "evidence": "Written all-depth conditional proof; explicit row codec; independent Cartesian and symbolic-payload implementation; source-bound finite receipts and public-CLI semantic, source, receipt and guard-removal controls.", + "author": "Ross Richardson", + "ai_assistance": "Substantial OpenAI Codex assistance, including an independent math-recursive-interfaces specialist; no independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can a complete selected caller instantiate arbitrary-U live packets with this codec?", + "why_it_matters": "A divisor theorem does not implement fresh fields, pointwise restoration or physical workspace.", + "first_step": "Connect one whole selected residual and recursive child to the PR2405 field schema, preserving the exact row codec and work bill.", + "blocked_by": "Complete global family/owner interpreter and primitive contracts remain outside this package." + }, + { + "question": "Does a target consumer actually require the P-based format?", + "why_it_matters": "The new reserve generally fails that interface; removing compatibility is a substantive model choice.", + "first_step": "Trace the exact row-decoder consumer and use the divisibility iff before replacing its reserve.", + "blocked_by": "No full downstream integration or paid format adapter is supplied." + } + ], + "assignment_seed": "fa7b3b7319d7ee637aa8bada2a148fdd", + "selected_method": "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope.", + "scope_key": "f5c32b23bcd01d2e356d/separated-work-live-row-divisor", + "session_start_utc": "2026-10-15T08:24:45Z", + "construction_cutoff_utc": "2026-10-15T09:09:45Z", + "predecessors": [ + { + "pr": 2195, + "author": "Jose Manuel (jmbarrancoml)", + "head": "3a1cf78a1ba6322129e42d80c50d21765524d612", + "credit": "Live/work separation and explicitly sufficient lcm overreserve; whole-packet contract." + }, + { + "pr": 2234, + "author": "Jose Manuel (jmbarrancoml)", + "head": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f", + "credit": "Recursive caller, row depth, separately paid buffers and parking." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2179#discussioncomment-18944653", + "expiry_utc": "2026-10-15T10:33:00Z", + "entry_coverage": { + "open_prs": { + "fetched_at": "2026-10-15T08:26:00.031527+00:00", + "complete_pagination": true, + "records": 619 + }, + "discussions": { + "fetched_at": "2026-10-15T08:29:11.930954+00:00", + "complete_pagination": true, + "records": 1149 + } + }, + "limitations": "Open PR titles/bodies, Discussion bodies/comments/replies, local READMEs and ledger; no arbitrary diff or unpublished-work coverage; no novelty guarantee.", + "submission_coverage": { + "open_prs": { + "fetched_at": "2026-10-15T08:48:44.952225+00:00", + "complete_pagination": true, + "records": 621 + }, + "discussions": { + "fetched_at": "2026-10-15T08:51:51.717297+00:00", + "complete_pagination": true, + "records": 1153 + } + }, + "submission_local_records": 1536, + "submission_warnings": [], + "focused_terms": [ + "9475", + "live-row divisor", + "physical-slot", + "row-format", + "2195", + "2234" + ], + "submission_assessment": "Named predecessors and cutoff/parameter/leaf follow-ups retained; source heads unchanged. New PR2416/2418 and Discussion2417 concern other models. Active Discussion2319 arithmetic-lowering work is separate. No claim of novelty or unsearched-code coverage." + }, + "upstream_checkpoint": { + "checked_at_utc": "2026-10-15T08:48:27.987998+00:00", + "commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "selected_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "guidance_unchanged": true + } +} diff --git a/research/selected-live-row-divisor/VERIFY.json b/research/selected-live-row-divisor/VERIFY.json new file mode 100644 index 0000000000..aeb474cb6f --- /dev/null +++ b/research/selected-live-row-divisor/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 90, + "checks": "Exact source pins, codec, child ranges, unchanged work bill and conditional-format controls" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 90, + "checks": "Independent Cartesian layers and symbolic arbitrary-payload/row/padding checks" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/test_package.py" + ], + "timeout_seconds": 90, + "checks": "Normal and optimized public-CLI source/receipt controls, read-only relocation and actual guard removal" + } + ] +} diff --git a/research/selected-live-row-divisor/independent.py b/research/selected-live-row-divisor/independent.py new file mode 100644 index 0000000000..173f329c48 --- /dev/null +++ b/research/selected-live-row-divisor/independent.py @@ -0,0 +1,357 @@ +#!/usr/bin/env python3 +"""Independent finite audit of the conditional complete live-row format. + +Standard library only. This file does not import the primary checker or its +artifacts. Cartesian products supply the oracle for all mixed-radix rows; +distinct formal payload symbols test permutations without sampling bit values. +This is not an execution of the selected BIT word or its recursive machine. +""" + +from collections import Counter +from itertools import product +from math import gcd, prod +import json + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def encode(digits, radices): + require(len(digits) == len(radices), "wrong number of digits") + value = 0 + for digit, radix in zip(digits, radices): + require(0 <= digit < radix, "digit outside complete range") + value = radix * value + digit + return value + + +def decode(value, radices): + require(0 <= value < prod(radices), "row outside complete range") + digits = [] + for radix in reversed(radices): + value, digit = divmod(value, radix) + digits.append(digit) + require(value == 0, "unconsumed row quotient") + return tuple(reversed(digits)) + + +def complete_rows(): + counts = Counter() + for w, low, high in product(range(1, 4), repeat=3): + base = w * low * high + for depth in range(4): + for multiplicity in (1, 2): + radices = (w, low, high) * depth + (multiplicity,) + row_count = multiplicity * base ** depth + counts["formats"] += 1 + seen = set() + for ordinal, digits in enumerate(product(*(range(r) for r in radices))): + # The Cartesian enumeration does not use either radix routine. + require(encode(digits, radices) == ordinal, "Cartesian encoding") + require(decode(ordinal, radices) == digits, "Cartesian decoding") + seen.add(ordinal) + counts["rows"] += 1 + for consumed in range(depth + 1): + quotient = multiplicity * base ** (depth - consumed) + prefix = digits[:3 * consumed] + suffix = digits[3 * consumed:] + require(encode(suffix, radices[3 * consumed:]) == ordinal % quotient, + "unused suffix is not the complete row remainder") + require(encode(prefix, radices[:3 * consumed]) == ordinal // quotient, + "exposed ancestors do not form the quotient") + counts["prefix_suffix_checks"] += 1 + require(seen == set(range(row_count)), "missing or duplicated row") + if depth: + unused = multiplicity * base ** (depth - 1) + for child_depth in range(depth): + child_stock = base ** child_depth + child_multiplicity, rem = divmod(unused, child_stock) + require(rem == 0 and child_multiplicity > 0, "incomplete child stock") + child_radices = (w, low, high) * child_depth + (child_multiplicity,) + require(prod(child_radices) == unused, "child volume mismatch") + # Every old high value sees the same complete child row set. + child_domain = tuple(product(*(range(r) for r in child_radices))) + for old_high in range(high): + require(len(child_domain) == unused, "high-dependent child size") + require({encode(c, child_radices) for c in child_domain} == set(range(unused)), + "child lacks a complete independent layer") + counts["high_child_domains"] += 1 + # These are the unchanged source formulas, at actual volume. + volume = 8 * row_count + packet = 8 * high * unused + require(packet * w * low == volume, "wrong live packet denominator") + role_slots = w + 4 + require(5 * (volume + 4 * packet) - packet + 9 * role_slots - 2 + == 5 * volume + 19 * packet + 9 * role_slots - 2, + "unequal-buffer parking identity") + counts["volume_parking_checks"] += 1 + return dict(counts) + + +def symbolic_payload(row_count): + # A symbol is a distinct formal input coordinate, not a sampled bit. + return {(r, s, x, y): ("input", r, s, x, y) + for r in range(row_count) for s in range(2) + for x in range(2) for y in range(2)} + + +def permute_payload(state, row_action, swap_data=False, flip_spectator=False): + output = {} + for (row, spectator, x, y), symbol in state.items(): + new_row = row_action[row] + new_spectator = 1 - spectator if flip_spectator else spectator + a, b = (y, x) if swap_data else (x, y) + key = (new_row, new_spectator, a, b) + require(key not in output, "noninjective payload permutation") + output[key] = symbol + return output + + +def cyclic_suffix_route(row_count, suffix_count): + require(row_count % suffix_count == 0, "partial suffix group") + route = {} + for start in range(0, row_count, suffix_count): + # Enumerate a concrete cycle and its edges, independently of radix decode. + cycle = list(range(start, start + suffix_count)) + destinations = cycle[1:] + cycle[:1] + route.update(zip(cycle, destinations)) + return route + + +def restored_payloads(): + fixtures = ((2, 3, 2, 2, 1), (2, 2, 3, 3, 1), + (3, 2, 2, 2, 2), (1, 3, 2, 3, 1), + (2, 1, 3, 3, 1), (3, 2, 1, 3, 2)) + counts = Counter() + for w, low, high, depth, multiplicity in fixtures: + base = w * low * high + rows = multiplicity * base ** depth + original = symbolic_payload(rows) + identity = dict(enumerate(range(rows))) + expected = permute_payload(original, identity, swap_data=True) + counts["fixtures"] += 1 + counts["distinct_initial_symbols"] += len(original) + for consumed in range(1, depth + 1): + unused = multiplicity * base ** (depth - consumed) + route = cyclic_suffix_route(rows, unused) + inverse = {destination: source for source, destination in route.items()} + for source, destination in route.items(): + require(source // unused == destination // unused, + "child touched an exposed ancestor including old high") + moved = permute_payload(original, route) + acted = permute_payload(moved, identity, swap_data=True) + returned = permute_payload(acted, inverse) + require(returned == expected, "row or spectator was not restored pointwise") + for child_depth in range(depth - consumed + 1): + require(unused % (base ** child_depth) == 0, "child depth exceeds suffix") + counts["complete_child_boundaries"] += 1 + counts["symbolic_endpoint_checks"] += len(original) + return dict(counts) + + +def depth_of(width): + depth = 0 + while width >= 64: + width = 42 * (width // 64) + depth += 1 + return depth + + +def width_depths(): + counts = Counter() + previous = 0 + for width in range(4097): + depth = depth_of(width) + require(depth >= previous, "nonmonotone depth") + previous = depth + counts["widths"] += 1 + if width < 64: + require(depth == 0, "incorrect leaf depth") + continue + atom = width // 64 + for rank in range(1, 43): + child = rank * atom + require(0 < child < width and depth_of(child) <= depth - 1, + "rank child depth contract") + counts["rank_children"] += 1 + for child in range(1, atom + 1): + require(depth_of(child) <= depth - 1, "fallback child depth contract") + counts["fallback_children"] += 1 + return dict(counts) + + +def padding_restriction(): + counts = Counter() + for stock in (1, 2, 3, 4, 6, 8, 12, 18): + for genuine_rows in range(stock, 3 * stock + 1): + padded_rows = ((genuine_rows + stock - 1) // stock) * stock + require(padded_rows % stock == 0, "padding did not supply full stock") + require(genuine_rows <= padded_rows < 2 * genuine_rows, "padding factor") + original = symbolic_payload(padded_rows) + route = cyclic_suffix_route(padded_rows, padded_rows) + inverse = {v: k for k, v in route.items()} + identity = dict(enumerate(range(padded_rows))) + actual = permute_payload(original, route) + actual = permute_payload(actual, identity, swap_data=True) + actual = permute_payload(actual, inverse) + expected = permute_payload(original, identity, swap_data=True) + restricted = {k: v for k, v in actual.items() if k[0] < genuine_rows} + require(restricted == {k: v for k, v in expected.items() if k[0] < genuine_rows}, + "padding restriction after completed endpoint") + counts["complete_padding_cases"] += 1 + return dict(counts) + + +def minimality_census(): + counts = Counter() + for base in range(1, 28): + for depth in range(4): + stock = base ** depth + # A positive integer leftover is necessary in the fixed full-product + # format. This finite census is separate from the written proof. + first = next(s for s in range(1, stock + 1) if s % stock == 0) + require(first == stock, "fixed-format least positive cardinality") + counts["base_depth_pairs"] += 1 + return dict(counts) + + +def two_format_compatibility(): + """Direct divisibility oracle for the unchanged complete P-slot format.""" + counts = Counter() + # Nontrivial low and high factors are present in the direct divisor. The + # written cancellation proves that their particular positive values do not + # affect the exact gate; this finite census uses N=2 and H=3. + low, high = 2, 3 + for live, physical in product(range(1, 13), repeat=2): + common = gcd(live, physical) + numerator, denominator = live // common, physical // common + require(gcd(numerator, denominator) == 1, "uncancelled compatibility fraction") + for depth in range(5): + live_stock = (live * low * high) ** depth + physical_stock = (physical * low * high) ** depth + gate = denominator ** depth + for multiplicity in range(1, 26): + direct = (multiplicity * live_stock) % physical_stock == 0 + cancelled = (multiplicity * live ** depth) % (physical ** depth) == 0 + proposed_gate = multiplicity % gate == 0 + require(direct == cancelled == proposed_gate, "incorrect exact acceptance gate") + counts["iff_cases"] += 1 + # Search directly among live-format cardinalities; any common + # reserve must be one of these. No lcm formula supplies the oracle. + first = None + for multiplicity in range(1, gate + 1): + counts["minimum_search_candidates"] += 1 + if (multiplicity * live_stock) % physical_stock == 0: + first = multiplicity + break + require(first == gate, "historical common reserve not minimal") + common_stock = ((live * physical // common) * low * high) ** depth + require(first * live_stock == common_stock, "wrong common-reserve cardinality") + counts["minimum_common_reserves"] += 1 + + live, physical = 28416, 28425 + common = gcd(live, physical) + require((live // common, physical // common) == (9472, 9475), + "selected compatibility fraction") + require(gcd(9472, 9475) == 1, "selected compatibility fraction not reduced") + for depth in range(9): + gate = 9475 ** depth + # Actual selected W and P; the arbitrary positive N,H have cancelled. + require((gate * live ** depth) % (physical ** depth) == 0, + "selected boundary must satisfy physical format") + counts["selected_accepted_boundaries"] += 1 + below = gate - 1 + if below > 0: + require((below * live ** depth) % (physical ** depth) != 0, + "selected just-below boundary unexpectedly accepted") + counts["selected_rejected_positive_boundaries"] += 1 + else: + # D=0 gives t=0 here. Divisibility of zero is true, but a zero + # multiplicity is outside the nonempty complete-row contract. + require(depth == 0 and below == 0, "unexpected boundary-domain case") + counts["selected_zero_multiplicity_outside_domain"] += 1 + return dict(counts) + + +def defect_controls(): + controls = {} + # Removing H can fail at the first level or only after a successful root split. + controls["omitted_high_first_layer"] = (2 * 3) % (2 * 3 * 5) != 0 + wrong_rows = (2 * 3) ** 2 + actual_base = 2 * 3 * 2 + controls["omitted_high_descendant"] = ( + wrong_rows % actual_base == 0 and (wrong_rows // actual_base) % actual_base != 0) + + # The historical physical-slot interpretation is an additional condition. + w, physical, low, high = 2, 11, 3, 2 + controls["physical_slot_divisor_not_automatic"] = (w * low * high) % (physical * low * high) != 0 + selected_w, selected_p = 28416, 28425 + selected_lcm = selected_w * selected_p // gcd(selected_w, selected_p) + require((selected_lcm, selected_lcm // selected_w, selected_lcm // selected_p) + == (269241600, 9475, 9472), "selected compatibility constants") + controls["selected_depth_one_physical_incompatibility"] = selected_w % selected_p != 0 + + # An XOR copy into zero work is sound; the same word on dirty work is not. + source, target, dirt = (frozenset((name,)) for name in ("source", "target", "dirt")) + work = frozenset() + work ^= source + correct_target = target ^ work + work ^= source + require(correct_target == target ^ source and not work, "allocated zero copy") + work = dirt ^ source + polluted_target = target ^ work + restored_dirty_work = work ^ source + controls["dirty_private_copy_pollution"] = ( + polluted_target != correct_target and restored_dirty_work == dirt) + reset_images = {value: 0 for value in (0, 1)} + controls["arbitrary_private_zeroing_noninjective"] = len(set(reset_images.values())) < len(reset_images) + + rows = 64 + original = symbolic_payload(rows) + identity = dict(enumerate(range(rows))) + expected = permute_payload(original, identity, swap_data=True) + missing_return = permute_payload(original, cyclic_suffix_route(rows, 8), swap_data=True) + controls["row_multiset_does_not_imply_pointwise_restoration"] = ( + Counter(missing_return.values()) == Counter(expected.values()) and missing_return != expected) + spectator_drift = permute_payload(original, identity, swap_data=True, flip_spectator=True) + controls["spectator_multiset_does_not_imply_restoration"] = ( + Counter(spectator_drift.values()) == Counter(expected.values()) and spectator_drift != expected) + + # Five real rows are padded to eight. A completed row drift would let a + # padded formal value replace a genuine one when the padded tail is dropped. + genuine, padded = 5, 8 + original = symbolic_payload(padded) + missing_return = permute_payload(original, cyclic_suffix_route(padded, padded), swap_data=True) + expected = permute_payload(original, dict(enumerate(range(padded))), swap_data=True) + controls["padding_removed_before_row_restoration"] = ( + {k: v for k, v in missing_return.items() if k[0] < genuine} + != {k: v for k, v in expected.items() if k[0] < genuine}) + controls["padding_factor_requires_at_least_one_stock"] = 4 >= 2 * 1 + + # A child asking for its parent's depth fails already at multiplicity one. + controls["child_depth_not_strictly_consumed"] = (12 ** 2 // 12) % (12 ** 2) != 0 + require(all(controls.values()), "a defect control did not distinguish its mutant") + return controls + + +def run(): + return { + "claim": "conditional_complete_live_row_format_only", + "complete_rows": complete_rows(), + "symbolic_payloads": restored_payloads(), + "width_depths": width_depths(), + "padding": padding_restriction(), + "minimality": minimality_census(), + "two_format_compatibility": two_format_compatibility(), + "negative_controls": defect_controls(), + "selected_execution": False, + "formal_kernel_proof": False, + "new_kappa": False, + } + + +if __name__ == "__main__": + print(json.dumps(run(), sort_keys=True, indent=2)) + print("PASS_SELECTED_LIVE_ROW_DIVISOR_INDEPENDENT no_new_kappa") diff --git a/research/selected-live-row-divisor/sources/pr2195/PROOF.md b/research/selected-live-row-divisor/sources/pr2195/PROOF.md new file mode 100644 index 0000000000..4330de85dd --- /dev/null +++ b/research/selected-live-row-divisor/sources/pr2195/PROOF.md @@ -0,0 +1,301 @@ +# Selected BIT calls on complete local-ring packets + +We prove an exact-stream integration statement for the selected PR589 word and +an explicit sufficient row layout. We assume completed address callees with +the spectator, restoration and work contracts below. We do not prove their +recursive implementation cost or admit a new exponent. + +## Domain and conclusion + +Fix an odd prime q, w >= 1, R = Z/q^w and m = 64. A payload is an arbitrary +Boolean function of two complete address blocks and complete spectators. +We compute payload XOR over F2; we use R only for addresses. At a given +recursive node, fix a diagonal unit matrix A whose entries depend on exposed +ancestor fields, but not on this node's family, cover coordinates or unused +descendant row field. We may fix each ancestor tuple separately in the proof. + +Use the pinned 288 call descriptors and both literal local programs, the +fixed data charts rho, and the helper completions in section 3. For each low +cover class, execute the whole local word on its complete high packet before +advancing to the next low class. Use fresh private work and the literal +transported-source ERASE guards. Assume that address callees act on the whole +specified packet, preserve its complete spectators, restore row coordinates +and close their work before returning. + +Under these hypotheses we obtain the selected local endpoints and chronological +hosting identity over GL64(R), on arbitrary correlated dirty payloads. After +the global bridges, idle remainders and terminal stream exchange, we obtain +the full weighted reversed interchange on each live family. We also give a +restricted-fibre XOR procedure and a compatible row divisor for these calls. +We retain their stated scan, route and workspace charges. + +We reuse alephnan's PR1627 literal replay and chronological proof. Eumemic +already gave a whole-owner GL local-ring argument in PR490. Our contribution +binds that domain to the selected literal word, distinguishes point owners +from complete-packet owners, supplies a selected live-row layout, and gives +physical restricted-fibre and wrong-geometry controls. We make no novelty +claim for generic conjugation or the common-label induction. + +## 1. Split projectors over R + +For a projector P on the head block and the fixed reversal C on the tail, +write + + D_C(P) = [[I-P, P C], [C P, I-C P C]]. + +We need P^2=P, without a symmetry requirement. Multiplication gives +D_C(P)^2=I. For nested projectors PQ=QP=P, multiplication gives +D_C(P) D_C(Q)=D_C(Q-P). For disjoint commuting projectors, it gives +D_C(P) D_C(Q)=D_C(P+Q). Conjugate by diag(A,I) to obtain the weighted maps. +For a variable g in GL64(R), conjugate P by g P g^-1. Use the inverse of g; +its transpose generally differs. + +PR1627 reconstructs the 636 rational frame projectors from the selected root +lines, and checks exact idempotence, nesting and dyadic final entries. These +identities hold in Z[1/2], so we specialize them to R. For a rank-r rational +idempotent, the characteristic polynomial equals T^(m-r)(T-1)^r in Z[1/2]. +After reduction modulo q, diagonalizability of an idempotent gives rank r. +We do not infer rank from the trace modulo q. + +Choose r independent columns of P and m-r independent columns of I-P modulo +q. Lift those same columns to R and concatenate them into T. The determinant +of T is a unit because its reduction is invertible. The equations +PT=T diag(I_r,0) then give P=T diag(I_r,0) T^-1. This proves split rank r +over R, including q dividing r. We apply the argument to frame projectors, +their nested differences and the ambient stage embeddings. + +For completeness, write P=B V with V B=I_r. Then + + D_C(P)-I = [-B; C B] [V, -V C]. + +The first factor has left inverse [-V,0], and the second has right inverse +[B;0]. Thus the address residual has split rank r. Unit conjugation preserves +this factorization and rank. + +We check 636 frames and 531 distinct residuals over Z/9, Z/25, Z/49 and +Z/27: 4,668 exact image/kernel bases, including 760 positive ranks divisible +by q. These finite checks audit the specialization argument; the argument +above covers arbitrary odd q and w. + +## 2. The selected local word and its rank-seven guards + +For the common invocation d, give each logical role the address label + + Gamma = Q_A Q_d D_C(P_frame + E_s) Q_d^-1 Q_A^-1, + Q_A = diag(A,I), Q_d = diag(d,C d C). + +For the reflected orientation replace the local P_frame by I_8-P_frame. +The exterior E_s occupies the first s seven-coordinate blocks. A MOVE from +label Gamma_a to Gamma_b uses Gamma_a Gamma_b^-1. An ADD between equal +labels performs XOR at the common address. COPY creates a private copy with +the relative transport. Equality of the decoded temporary and source implies + + f_temp = f_source composed with Gamma_source Gamma_temp^-1, + +which is the physical ERASE guard. Bijectivity equates zero decoded and zero +physical payload. Apply induction to the literal chronological events, using +the owner separation from section 3 to exclude indirect writes to a source. + +The imported PR1627 replay propagates all 661 initial Boolean columns through +both 27,234-event programs, checks centre immutability and the nine literal +COPY/ERASE episodes per orientation, and returns x'=x, y'=y+x, h'=h in local +role order. Arbitrary substitutions for those columns allow correlated +payloads. Each event acts separately at each high cover coordinate after +owner alignment, so the same induction applies to a complete high packet. + +The source copies frames 510 through 518 to frame 0. Their relative swap has +rank seven in both orientations; the common E_s cancels. We check weighted +transport for the actual frame pairs and twelve ambient 64-dimensional COPY +cases, including charts that mix local and exterior axes. We reuse PR1627's +literal guard checks rather than treating a rank number as an ERASE proof. + +## 3. Complete owner packets and chronological sweeps + +Let F_d0 = {d0 + q G : G in [q^(w-1)]^(64*64)} for a fixed invertible low +matrix d0. A matrix over R is invertible exactly when its reduction is. +For a fixed unit chart sigma, right multiplication is a bijection + + F_d0 sigma^-1 = F_(d0 sigma_bar^-1). + +The bijection includes the carries in the chosen low/high representation. +At one low invocation, two helpers in the same family therefore have +disjoint complete packets precisely when their owner low classes differ. + +For port p let A_p be the retained dyadic orthogonal family chart. For a +hosted support S of size eight, start from D={0,...,7}. Pair the sorted sets +D\S and S\D and exchange each pair of axes, obtaining pi_S. If S meets D, +set sigma_S=A_p pi_S; otherwise set sigma_S=pi_S. This is the support +completion used in PR2157. It has image A_p E_S on the local block, since +A_p is the identity on exterior axes. Its full basis order need not match +PR1627's completion: the full local endpoint depends on this image projector. + +Within a selected call, the supports of two helpers in the same family are +disjoint. Their images remain nonzero disjoint subspaces modulo each odd q, +because A_p is invertible there. Hence their chart reductions differ. Left +multiplication by d0 preserves that difference, proving complete-packet +separation. The 222 data families are distinct and outside the helper +families. The private family lies outside the live inventory. + +We check the prescribed images of 124 completion types and the supports of +181,056 same-family pairs across 288 calls. The selected word includes +11,072 same-family ADDs across these calls. For example, stage 0, replica 0, +event 19422 adds role 244 into role 243 in family 451, on supports 9..16 and +1..8. A whole-family XOR would act on more than the specified owned packet. + +Finish the whole word for a low class before the next class. Distinct low +invocations may reuse a physical packet through different roles. The local +endpoint theorem accepts its current arbitrary dirty value, so this reuse +does not require fresh or independent inputs. We reduce complete calls to +their endpoints before commuting any hosted residuals. + +For each fixed slot, d -> d sigma^-1 permutes the full GL64(R) cover. Thus +one full sweep places that slot's residual once on each physical class. +For a fixed family and physical g, the images g A_p E_S A_p^-1 g^-1 of +disjoint supports are commuting disjoint idempotents. PR1627 checks the +selected untouched intervals between a slot's host stage and its nominated +idle child. Its chronological argument therefore applies in these charts: +move the completed slot endpoints inside those intervals, then multiply +them with the exact remainder to recover each full idle child. + +We also replay the global eight-role Boolean schedule, including its eighteen +bridge shears and terminal pair exchange. It returns the identity on decoded +data. The terminal exchange moves frame labels with stream values. On an +original source family the entry projector is the port line P and the final +projector is I-P; on the other family the endpoints are 0 and I. Their +relative operators give the full F_A. We check the 111 weighted ambient +source endpoints and the 888 data-chart boundary cases over Z/9 and Z/25. +For f-atom blocks, tensor these identities with I_f and retain the specified +tail reversal convention. We do not charge a new full-tail pass for a +coordinate convention, or assert that an actual required pass would be free. + +## 4. Restricted-fibre XOR and its cost + +The stream model in `upstream/build/sections/02-streams.tex`, lines 24-26, +60-96 and 98-118, permits fixed selectors, split/merge passes and work +copies, with charges for scans, counters, rewinds and erasure. At fixed q +there are finitely many low classes. Use the following procedure for a +same-family ADD on two distinct owned low packets: + +1. Scan the family and copy the target and source packets to work streams. +2. Align both complete high fibres to d=g sigma and XOR them there. +3. Invert the target alignment. Scan the original family and replace only + its target packet, copying the other packets unchanged. +4. Erase the fresh work copies and reset their heads. + +Keep the original source intact. Its work copy needs no inverse route before +erasure. With packet volume V_f and whole-family volume V_F, charge + + C_select(q) V_F + T_target(V_f,w) + T_source(V_f,w) + + T_target_return(V_f,w) + C_XOR V_f. + +There are three route actions. An invocation over every low class multiplies +the finite q-dependent constant; it does not introduce a loop of scans over +the growing high-cardinality set. The fixed-route lowering in PR2157 can +implement each route under its completed ordinary-callee and preparation +contracts. Its cost must enter the selected numerical invoice before use in +an admitted bound. PR490 likewise retained a separate B_GL allowance. + +Our physical fixture executes this procedure on the full GL2(Z/9) family: +3,888 rows, three unused classes per row, seventeen payload bits per class. +It performs two full-family scans and two ordered high shifts on 198,288 +bits. The target and return charts are identity in this fixture; the source +chart is [[1,1],[0,1]]. It needs no ordinary callee. The independent oracle +uses full-ring matrix multiplication, and we compare the whole payload, +including the 47 unowned low-class packets. Omitting a carry changes the +payload. The meter counts payload reads, writes, head movement and erasure; +it does not measure Python controller arithmetic or certify all selected +64-dimensional routes. + +## 5. An explicit live-row layout compatible with the physical count + +The selected emitter counts W=28,416 live families and P=W+9=28,425 physical +slots. Its private COPY register starts at zero; the copied-centres lemma +uses a work stream with the same logical volume as its source. We must +allocate and charge that work separately. We cannot clear arbitrary input +rows merely by assigning them a private-slot label. + +Keep w fixed down the coarse recursion. Set N=|GL64(F_q)|, +H=q^(4096(w-1)), and + + M=lcm(W,P)=269241600, K=M N H, + D(n)=0 for n<64; D(n)=1+D(42 floor(n/64)) otherwise, + S(n,w)=K^D(n). + +At an internal node take a row count R_rows=t S(n,w). Decode its complete +range as + + [W] x [N] x [H] x [U], + U=R_rows/(W N H)=t * 9475 * K^(D(n)-1). + +All original rows carry live payload. Allocate the private and selector work +streams outside this coordinate split, with the complete packet shape of +their sources. A fixed family and low class has exact logical volume +V/(W N), since we retain all H high coordinates and all U unused rows. + +For a child of width r floor(n/64), 1<=r<=42, monotonicity of D gives +D_child<=D(n)-1. Fallback children of width at most floor(n/64) obey the +same inequality. Thus K^D_child divides U. For each fixed parent high +matrix, the child receives an identical complete fresh row range inside U; +parent high coordinates and inactive atoms become complete spectators. +After k active levels the unused count is t * 9475^k * K^(D(n)-k). +The compatibility factor remains complete unused stock. + +This induction requires routes to fix U and generated child descriptors +to read exposed ancestors rather than fresh child roles. It also requires +the child to restore its row field pointwise. At leaves we use the completed +ordinary contract, whose own workspace obligations remain separate. We +prove sufficient coarse row stock, not a full allocation of recursive work +tapes. The retained depth-first parking procedure in `04-swap.tex`, lines +222-242, is a starting point for that allocation and its scan bill. + +Since M/P=9472, S is also divisible by the P-based packet power. This is +an explicit alternative layout with an overreserve. We do not identify its +live rows with arbitrary P-slot input rows or claim that divisibility alone +discharges PR2084's physical interpretation premise. + +For the eligible prime domain q>2^80, M=S without divisibility, the outer wrapper may pad its row range to +ceil(R_rows/S) S<2 R_rows. It may remove that padding only after the completed +parent restores its full row coordinate. We have not supplied the outer +borrow, finite-cutoff or time admission here. + +The executable layout test enumerates a complete small model with W=2, +P=3, q=3 and GL1 high/low fields: 1,296 original rows, 324 rows in a selected +low packet, and unused count 108 containing the child divisor 36. We check +exact coverage and decoding, child independence from the parent high field, +and rejection of P as the live-volume denominator. This is a layout test, +not a small simulation of the full selected recursive algorithm. + +## 6. Controls and limits + +For the selected port-eight root r=(0,1,1,0,1,0,0,1), take g=I+3E_12 over +Z/9, with zero-based indices. The wrong transpose conjugate g P g^T agrees +with g P g^-1 modulo 3 but fails idempotence: entry (1,1) of its defect is 6. +The corresponding partial swap fails involution with defect 3 at (1,1). + +An orthogonal projection onto each transformed range does not repair this. +Let u=g r and v=g^-T r. The projectors uu^T/(u^T u) and I-vv^T/(v^T v) +have split ranks 1 and 7, agree with the correct pair modulo 3, and each +defines an involution. Their product still differs from the full swap: +head entries (1,4) and (4,1) have defects 6 and 3. We need the complementary +oblique projectors uv^T/4 and I-uv^T/4. + +For a separate weak-owner countermodel over GL2(Z/9), take sigma_0=I and +sigma_1=I+3E_01. The 81 owner pairs differ at each fixed d, but both image +packets are the same high fibre. The alias permutation has 27 three-cycles. +A simultaneous snapshot XOR has Boolean rank 54; the serial fixed-d XORs +have rank 81. On an all-one payload they leave zero and 27 ones respectively. +This refutes point-owner injection as a sufficient high-batching argument; +the selected low-separated completions pass the stronger condition. + +We leave completed weighted child implementations, their recursive scratch +allocation, bad-class integration, a selected finite routing invoice and +the outer analytic transfer as obligations. We prove neither an unconditional +integer-multiplication theorem nor a change to the selected kappa. We prepared +this written proof and executable certificate with substantial OpenAI Codex +assistance; no independent human or proof-assistant verification is claimed. diff --git a/research/selected-live-row-divisor/sources/pr2195/owner_packets.py b/research/selected-live-row-divisor/sources/pr2195/owner_packets.py new file mode 100644 index 0000000000..70d5fcc0c8 --- /dev/null +++ b/research/selected-live-row-divisor/sources/pr2195/owner_packets.py @@ -0,0 +1,187 @@ +"""Selected low-packet separation, global scalar schedule and live-row layout.""" +from collections import Counter,defaultdict +from fractions import Fraction as F +from itertools import combinations,product +from math import lcm +from ring_algebra import need,eye,reduce_matrix,chart,conjugate,weighted_swap,multiply,difference + + +def pending(event): + a,b=event["source_level"],event["target_level"] + return list(range(1 if a==-1 else 8+7*a,8+7*b)) + + +def completion(axes,port): + """PR2157's support completion; the full basis order is immaterial.""" + perm=list(range(64));domain=set(range(8));support=set(axes) + for i,j in zip(sorted(domain-support),sorted(support-domain)):perm[i],perm[j]=j,i + u=[tuple([F(port["q"][i],2)]+list(map(F,port["complement_columns"][i]))) for i in range(8)] + def a_column(j): + if j<8:return tuple(u[i][j] if i<8 else F(0) for i in range(64)) + return tuple(F(i==j) for i in range(64)) + local=bool(domain&support) + actual=[a_column(perm[i]) if local else tuple(F(k==perm[i]) for k in range(64)) for i in range(8)] + reference=[a_column(j) for j in axes] + need(sorted(actual)==sorted(reference),"actual completion has the prescribed image basis") + need(all(sum(x*y for x,y in zip(a,b))==int(i==j) + for i,a in enumerate(actual) for j,b in enumerate(actual)),"unit orthogonal image basis") + need(all(x.denominator&(x.denominator-1)==0 for col in actual for x in col),"dyadic completion") + return tuple(perm),local + + +def owner_certificate(template,geometry): + children={e["idx"]:e for e in template["schedule"] if e["kind"]=="idle"} + pairs=occurrences=same_family_adds=0;types=set();sizes=Counter();first_add=None + for call in template["calls"]: + byfamily=defaultdict(list);owners=call["owners"] + datafamilies={f for f,_ in owners[:222]} + need(len(datafamilies)==222,"distinct live data families") + role_support={} + for role,(family,route) in enumerate(owners[222:],222): + need(route[0]=="hosted" and family not in datafamilies,"hosted family outside the active pair") + _,child,offset,width=route + axes=pending(children[child])[offset:offset+width] + need(len(axes)==width==8,"whole helper block") + port=family%111;key=(tuple(axes),port if min(axes)<8 else None) + if key not in types:completion(axes,geometry["ports"][port]);types.add(key) + byfamily[family].append((role,tuple(axes),child));role_support[role]=axes + occurrences+=1 + for family,roles in byfamily.items(): + sizes[len(roles)]+=1 + for a,b in combinations(roles,2): + need(set(a[1]).isdisjoint(b[1]),"separation witness for complete low packets") + pairs+=1 + for position,event in enumerate(template["local_programs"][call["orientation"]]): + if event[0]!=1:continue + target,source=event[1:3] + if target<222 or source<222 or target>=661 or source>=661:continue + if owners[target][0]==owners[source][0]: + same_family_adds+=1 + if first_add is None: + first_add={"stage":call["stage"],"replica":call["replica"],"position":position, + "target_role":target,"source_role":source,"family":owners[target][0], + "target_support":role_support[target],"source_support":role_support[source]} + need((occurrences,pairs,len(types),same_family_adds)==(126432,181056,124,11072),"selected owner inventory") + need(first_add["position"]==19422 and first_add["family"]==451,"selected same-family ADD") + return {"calls":len(template["calls"]),"helper_occurrences":occurrences, + "same_family_pairs":pairs,"completion_types":len(types), + "group_sizes":dict(sorted(sizes.items())),"same_family_ADDs":same_family_adds, + "first_same_family_ADD":first_add,"private_family":template["live"]} + + +def global_scalar(schedule,skip=-1): + values=[1<=64:n=42*(n//64);d+=1 + return d + + +def encode(family,low,high,unused,low_count,high_count,unused_count): + return ((family*low_count+low)*high_count+high)*unused_count+unused + + +def decode(row,low_count,high_count,unused_count): + row,unused=divmod(row,unused_count);row,high=divmod(row,high_count) + family,low=divmod(row,low_count) + return family,low,high,unused + + +def row_layout(template): + live=template["live"];physical=live+template["private_centre_reserve"] + compatible=lcm(live,physical);slack=compatible//live + need((live,physical,compatible,slack)==(28416,28425,269241600,9475),"live/work compatibility count") + need(compatible<2**80,"same logarithmic per-level envelope for eligible q") + depth_checks=0 + for n in (0,1,63,64,65,127,128,1024,4096,10**6,10**9): + if n<64:need(depth(n)==0,"leaf reserve");continue + for rank in range(1,43): + need(depth(rank*(n//64))<=depth(n)-1,"child compatible reserve divides unused quotient") + depth_checks+=1 + # Exhaustive small complete-row model of the same mixed-radix layout. + # W=2, P=3, q=3, GL1 low classes=2, high cardinality=3, depth=2. + w,p,low_count,high_count=2,3,2,3 + packet=lcm(w,p)*low_count*high_count;rows=packet**2 + unused_count=rows//(w*low_count*high_count) + seen=set() + for fields in product(range(w),range(low_count),range(high_count),range(unused_count)): + row=encode(*fields,low_count,high_count,unused_count) + need(decode(row,low_count,high_count,unused_count)==fields,"exact row coordinate round trip") + seen.add(row) + need(seen==set(range(rows)),"every original live row belongs to the layout") + batch=[encode(1,1,h,u,low_count,high_count,unused_count) + for h,u in product(range(high_count),range(unused_count))] + need(len(batch)*w*low_count==rows,"logical child volume denominator") + need(len(batch)*p*low_count!=rows,"physical inventory is not the live denominator") + need(unused_count%packet==0,"child reserve remains complete") + for h in range(high_count): + child_rows=[u%packet for u in range(unused_count)] + need(Counter(child_rows)==Counter({r:unused_count//packet for r in range(packet)}), + "fresh child row coverage independent of parent high coordinate") + return {"live_families":live,"private_inventory":physical-live,"compatible_low_factor":compatible, + "unused_compatibility_factor":slack,"physical_divisibility_factor":compatible//physical, + "depth_checks":depth_checks,"toy_rows":rows,"toy_batch_rows":len(batch), + "toy_child_reserve":packet,"toy_unused_quotient":unused_count, + "volume_denominator_control":"REJECT_PHYSICAL_INVENTORY_SUBSTITUTION", + "scope":"Explicit alternative packet layout; no numerical routing invoice or completed recursive scratch allocation."} diff --git a/research/selected-live-row-divisor/sources/pr2195/verify.py b/research/selected-live-row-divisor/sources/pr2195/verify.py new file mode 100644 index 0000000000..7f46298510 --- /dev/null +++ b/research/selected-live-row-divisor/sources/pr2195/verify.py @@ -0,0 +1,77 @@ +"""Selected PR589 local-ring packet integration; reuse the pinned PR1627 audit.""" +import argparse +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import sys + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +sys.path.insert(0,str(HERE)) +from ring_algebra import need,ring_certificate +from fibre_streams import alias_control,physical_fibre_check +from owner_packets import owner_certificate,global_endpoint,data_chart_boundaries,row_layout + +PREDECESSOR="research/pr589-five-helper-hosting/" + + +def canonical(value):return json.dumps(value,sort_keys=True,separators=(",",":")) + + +def inputs(): + manifest=json.loads((HERE/"SOURCES.json").read_text()) + for item in manifest["files"]: + if item["usage"]=="input": + raw=(ROOT/item["path"]).read_bytes() + need(sha256(raw).hexdigest()==item["sha256"],"source pin: "+item["path"]) + spec=importlib.util.spec_from_file_location("pr1627_retained",ROOT/(PREDECESSOR+"verify.py")) + module=importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def build_result(): + old=inputs() + inherited=old.run() + receipt=json.loads((ROOT/(PREDECESSOR+"RESULT.json")).read_text()) + need(json.loads(json.dumps(inherited))==receipt,"fresh predecessor receipt") + word,template,geometry=old.read(old.WORD),old.read(old.HOST),old.read(old.GEO) + need(template["m"]==64 and max(map(int,inherited["profile"]))==42,"selected coarse width and maximum child rank") + frame_rows=[old.projection([word["lines"][i] for i in f]) for f in word["frames"]] + projectors=[p for p,_ in frame_rows];dims=[r for _,r in frame_rows] + rings=ring_certificate(projectors,dims,template["local_programs"],word) + basis=rings.pop("basis_choices") + rings["basis_choice_sha256"]=sha256(canonical(basis).encode()).hexdigest() + bad=dict(template);bad_call=dict(template["calls"][0]) + bad_call["owners"]=list(bad_call["owners"]) + bad_call["owners"][244]=bad_call["owners"][243] + bad["calls"]=[bad_call]+template["calls"][1:] + try:owner_certificate(bad,geometry) + except ValueError as error: + need(str(error)=="separation witness for complete low packets","specific aliased-owner rejection") + else:raise ValueError("aliased selected owners accepted") + return {"status":"PASS_SELECTED_LOCAL_RING_SWEEPS", + "inherited_PR1627":{"status":inherited["status"],"receipt_sha256":sha256(canonical(receipt).encode()).hexdigest(), + "local":inherited["local"],"rank_mass":inherited["rank_mass"], + "rank_deficit":inherited["rank_deficit"], + "credit":"alephnan; the existing finite-field whole-call proof and literal replay are reused, not claimed as new."}, + "local_ring":rings,"owner_packets":owner_certificate(template,geometry), + "selected_owner_mutation":"REJECT_EQUAL_SUPPORT_PACKET_ALIAS", + "data_chart_boundaries":data_chart_boundaries(geometry), + "global_endpoint":global_endpoint(template,word,projectors), + "packet_alias_control":alias_control(),"restricted_fibre_XOR":physical_fibre_check(), + "compatible_row_layout":row_layout(template), + "scope":"Selected local-ring exact-stream integration and explicit live-row layout, conditional on completed address callees and the stated work/stock contracts; no finite-invoice admission or new exponent."} + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit",action="store_true",help="Print a fresh receipt without comparing the saved RESULT.json.") + args=parser.parse_args();result=build_result() + if not args.emit: + need(json.loads(canonical(result))==json.loads((HERE/"RESULT.json").read_text()),"saved receipt equality") + print(json.dumps(result,indent=2)) + + +if __name__=="__main__":main() diff --git a/research/selected-live-row-divisor/sources/pr2234/NOTICE.md b/research/selected-live-row-divisor/sources/pr2234/NOTICE.md new file mode 100644 index 0000000000..a5ccfbecbd --- /dev/null +++ b/research/selected-live-row-divisor/sources/pr2234/NOTICE.md @@ -0,0 +1,54 @@ +# Attribution and source scope + +Jose Manuel (`jmbarrancoml`) prepared this contribution with substantial +OpenAI Codex assistance in mathematical analysis, code, tests and writing. +We use the repository's Apache-2.0 license and retain source notices in the +eight unchanged vendored Python files. `SOURCES.json` records their original +paths, commits and SHA256 values; we checked byte equality against those +Git objects before publication. + +We credit the following predecessors: + +* OpenAI's retained framework and Douglas Colkitt: the stream, ordinary + interchange, row-volume and tape contracts, with their source notices. +* DreamingOfClouds: selected PR589 tuning, on eumemic's PR555 base word. + The lineage includes Dugongue's PR541/548 and rohanarun's PR542. +* alephnan: PR1627, retained as `research/pr589-five-helper-hosting`, for the + literal word, whole-call dirty-helper cancellation and chronological proof. +* eumemic: PR490's whole-owner GL local-ring argument. +* The source527 contributors: retained normal forms, weighted leaf + factorization and ordinary borrowing method, with the existing notices. +* commdata2338: PR2160 selected good normal form, PR2188 mixed descriptor + grammar, and PR1379 unequal-buffer parking boundary. We vendor PR2188's + `descriptor.py` unchanged at `77bb4e8cfe3e8c89f6e281eaf948454ee487796a`. +* RossRichardson: PR2159 full-ring fallback topology, covariance and charge, + at `9022b980917b7a9dd0bf1e9cb8012a16ea30293b`. +* Jose Manuel: PR2157 fixed dyadic routes (`eb1bf93950e9b14f7fadca7892866e9f29a26ad3`), + PR2171 controlled streams (`416aac58960660edced905dc7d914c126d357290`), + PR2195 GL packet integration (`3a1cf78a1ba6322129e42d80c50d21765524d612`), + and PR2207 fallback continuation (`149d55d90d3c0877ed3d78e1deca8eb2f72e0d00`). +* The authors of the retained `moment.py` and `base_two_moment.py` engines: + we reuse their rational arithmetic at one coarse point, with input pins. +* 1337isnot1337: adjacent PR2212 route inventory, at + `cd37bdf943876f81a60522e13cf838a464ed3104`; we do not reproduce that census. + +The new work binds the remaining actual residual labels, gives causal symbolic +field references and completed leaf/header bases, and composes the weighted +caller by strong induction. We derive the resulting ordinary-interchange +saving with the elementary base. We claim neither a new generic weighted +factorization nor a new generic parking lemma. + +The retained `physical_stream.py` contains an explicit weighted-child test +oracle and `qadic_streams.py` contains an ordinary test oracle. We retain +those files unchanged for their sequential primitives and arithmetic. The +new completed leaf/header paths never call those oracles; the replay replaces +them with rejecting functions. Their presence does not implement recursive +children. PROOF.md supplies that separate construction. + +The pending predecessor PRs remain subject to review. We have not merged or +closed them. The repository's selected result remains unchanged. + +For the exact written premises, see the pinned +[PR2195 packet proof](https://github.com/CrocSwap/integer-mult-bounds/blob/3a1cf78a1ba6322129e42d80c50d21765524d612/research/selected-bit-local-ring-sweeps/PROOF.md), +[PR2171 adapter proof](https://github.com/CrocSwap/integer-mult-bounds/blob/416aac58960660edced905dc7d914c126d357290/research/selected-bit-controlled-streams/PROOF.md) +and [PR2207 fallback proof](https://github.com/CrocSwap/integer-mult-bounds/blob/149d55d90d3c0877ed3d78e1deca8eb2f72e0d00/research/selected-bit-fallback-streams/PROOF.md). diff --git a/research/selected-live-row-divisor/sources/pr2234/PROOF.md b/research/selected-live-row-divisor/sources/pr2234/PROOF.md new file mode 100644 index 0000000000..6c410cab57 --- /dev/null +++ b/research/selected-live-row-divisor/sources/pr2234/PROOF.md @@ -0,0 +1,433 @@ +# Recursive closure of the selected BIT interchange + +We give a written construction on a fixed number of finite-alphabet multitape +streams. We retain the sequential stream model of `02-streams.tex`: complete +address ranges, arbitrary Boolean payload, charged scans, counters, rewinds and +scratch erasure. We prove an ordinary binary chunk-interchange bound + + O(V E^(1-a)), a = 169711/100000000 = 0.00169711, + +for two complete E-bit address chunks and arbitrary complete spectators, where +V counts payload bits. The machine restores spectators and clears its work. +We fix one odd prime q>2^80 throughout; constants and the fixed tape count may +depend on q and the selected word. We make no practical runtime claim. + +We supply a mathematical algorithm and finite interface checks. We have not +translated the entire recursive machine into transition tables or a proof +assistant. Reviewers must assess the composition argument below. The selected +finite certificate and the multiplication theorem have further interfaces, +including the complex supplier and analytic transfer; we leave their status +unchanged. + +## 1. Sources and the recursive contract + +We use DreamingOfClouds' selected PR589 word, building on eumemic's PR555 word, +and alephnan's PR1627 literal/chronological proof. We reuse the GL local-ring +packet integration of PR2195, the good adapters of PR2171, the fallback word +of PR2159/PR2207, and commdata2338's PR2188 weight grammar. Source527 already +gives the weighted factorization and outer borrowing method. PR1379 supplies +the unequal-buffer parking boundary. `SOURCES.json` pins the executable inputs; +`NOTICE.md` identifies the pending source commits and mathematical reuse. + +Fix an original radix-q width e, c=17/10000, and w=ceil(e^c). Put B=q^w and +R=Z/B. We keep w fixed throughout one coarse recursion. Let C_n reverse n +atom positions. For a diagonal unit vector A, we construct + + F_A(H,D) = (A C_n D, C_n A^-1 H). + +We quantify over any two ordered complete n-atom chunks, with arbitrary +complete preceding, intervening and following fields. This includes two +subchunks of one former bank, which we need for fallback reversals. We allow +arbitrary correlated dirty payload values. + +We generate A from a constant unit by the Good and FallbackPair expressions +below. A may read earlier frozen matrix fields; it may not read this node's +fresh family, matrix or unused stock. A unit child starts a new constant +expression but retains its global generation depth. We bound that depth by +the original root width, including after such a reset. + +At return we require the specified address permutation on I/O, pointwise +restoration of row and spectator coordinates, empty local work and restored +head positions. For a parking top h, we visit no cell below h-1 and write no +cell below h. We require a time bound uniform in parked contents and h. + +## 2. Actual residuals and full-ring preparation + +PR1627 reconstructs 636 rational frame projectors and proves the nesting +identities used by both selected literal programs. Their entries lie in +Z[1/2]. For an idempotent P0 of rational rank r, its characteristic polynomial +is T^(64-r)(T-1)^r. Reduction modulo an odd q preserves this identity and +idempotent diagonalizability, hence rank r, including when q divides r. + +Choose independent image columns of P0 and kernel columns of I-P0 modulo q. +Their lifts form a unit matrix B0 over R and satisfy + + P0 = B0 diag(I_r,0) B0^-1. + +We compute this identity in control arithmetic. We do not move payload through +B0. For the actual owner chart sigma and raw physical header g, the provider +passes g sigma B0 to the retained coordinate normalizer. It therefore computes +exactly P=g sigma P0 sigma^-1 g^-1. + +For MOVE, we use the positive nested frame difference and the actual owner +sigma. The common stage projector cancels. The reflected orientation gives +the same positive residual. For COPY, we first copy and align the source +packet to d=g sigma. Its private header is d and its projector label is P0; +we set its additional chart to I. Applying sigma again would change the +operator. ERASE retains the literal transported-source equality guard. + +For an idle remainder, we subtract the actual hosted slots from its pending +axes and use the fixed family chart. We skip the zero remainder. The provider +binds 28,278 canonical requests and 32 replicas, giving + + H_1=381024, H_2=400416, H_3=22752, H_4=26880, + H_5=29376, H_6=17376, H_7=26784, H_42=288. + +We obtain 541 distinct base labels and 1,235 assembled charts. The finite +checks verify image/kernel bases over Z/9 and Z/25 for each label, and 120 +full 128-coordinate operators from selected MOVE, COPY and idle requests. +These cases supplement the identities; they do not enumerate GL64(R). + +## 3. One schedule per complete low packet + +Write g=g0+qG with g0 in GL64(F_q) and G in [q^(w-1)]^4096. For a fixed +request, call g0 good when the first r northeast pivots of PC are units. +Equivalently, require the leading k principal minors of P to be nonzero +modulo q for 1<=k<=r. Unit tests depend only on g0. The full coefficients +still depend on G. + +For each k, multiply its minor by det(g)^k to obtain a polynomial of degree +at most 64k in the entries of g. Conjugating the fixed split rank-r projector +to diag(I_r,0) gives a nonzero witness. The union of these zero sets has +fraction at most 64r(r+1)/(2q) in all matrices. Since + + |GL64(F_q)|/q^4096 = product_(i=1)^64 (1-q^-i) > 1/2, + +the bad fraction for this request is at most 2*64^3/q<10^-16. We use this +bound separately for each paid edge. We do not require one matrix to be good +for every label or multiply the bound by the number of labels. + +On a good packet, unweighted northeast elimination gives unit-lower matrices +L,R0 and a pivot vector delta. Split rank and a unit rank-r minor force the +remaining Schur block to vanish over R itself. We retain q-multiples in the +arithmetic; reduction modulo q alone would not establish that conclusion. +The normal-form factorization in source527/PR2171 uses ordered head, tail +and cross ADDs, one weighted child, and the inverse adapters. For n=64f, + + A_child[k f+j] = A[k f+j] delta_k, 0<=k=1. Recompute on split and merge rather than retaining +an array indexed by the high fibre. Ripple counters have amortized linear +movement cost; initialize them once per scan and do not reread unrelated +spectator counters per fibre. Fixed low tables and finite labels depend on +q, not e. Thus these scans have the stated uniform bounds. For independently +chosen n,w,d, retain the preparation quotient instead of this absorption. + +The selected word has fixed length. Good and bad bodies use O(n) ordered +atom passes; header routes use O(Vw) each; selections, XORs, erasure and +parking use O(V) each. We include their finite q-dependent multiplicities +in a constant C. The local nonrecursive charge is C V(n+w), including the +remainder leaf. This is an asymptotic accounting, not an explicit optimized +finite invoice for the selected multiplier. PR2212 prices the separate +same-family route inventory and leaves further whole-invocation charges. + +Normalize by logical volume and bound the worst generated call by T(n,w). +For positive widths below 64, T<=Cw. The bad fraction is at most epsilon=10^-16 +for each request, and each fallback has at most 32*64^2 children of width at +most f=floor(n/64). We may overcount good calls on bad classes, obtaining + + T(n,w) <= sum_r (H_r/W) T(r f,w) + + epsilon F/W * max_(1<=j<=f) T(j,w) + C(n+w), + F=32*64^2*sum_r H_r=118606528512. + +We prove a monotone upper bound, so the maximum causes no extra factor. +Define mu_t=(sum H_r(r/64)^t + epsilon F(1/64)^t)/W. The two retained outward +rational engines independently give + + mu_1 = 2874298095721977/2890625000000000 < 199/200, + mu_(1-c) < 9999/10000. + +Induct on n and use f<=n/64. Increasing C to cover the leaf constants gives + + T(n,w) <= 200 C n + 10000 C n^(1-c) w. + +Indeed the first term leaves at least Cn after the recursive linear mass, +and the second leaves at least C n^(1-c)w>=Cw. We treat n=0 separately. +The resulting constants are independent of ancestor contents, stack top, +row multiplicity and original e. + +## 8. Internal borrowing and binary interchange + +Choose the sufficient stock S=K(w)^D(e) from the original width e, before +choosing a body width. Since M=64: + n=42*(n//64) + result+=1 + return result + + +@dataclass(frozen=True) +class Child: + kind: str + first: int + second: int + expression: object + + +@dataclass(frozen=True) +class ResidualPlan: + branch: str + parent_size: int + frozen_field: object + children: tuple + operations: tuple + + +def residual_plan(expression,request,low_matrix,catalogue): + """Freeze only the parent field's specification; values stay on I/O.""" + n=expression.size;f=n//64;q=expression.q + need(f>=1,"internal residual node") + raw=RawHeader(q,1,low_matrix,tuple((0,)*64 for _ in range(64)),request.header_space) + header=GeneralHeader(raw,request,catalogue) + p=d.projector(header.read(Arithmetic(q)),header.axes,q) + specification=FieldSpecification(q,expression.width,request,low_matrix) + try: + d.good_pivots(p,request.base.rank,q) + good=True + except ValueError: + good=False + if good: + child=expression.append("good",request,low_matrix,expression.depth) + # Coordinates refer to the core: first 64f head, last 64f tail. + children=(Child("good",0,128*f-child.size,child),) + operations=tuple(schedule(64,request.base.rank,1)) + branch="good" + else: + program=compile_program(d.elimination(d.residual(p,q),q)) + children=[] + for op in program: + if op.kind!="swap": + continue + i,k=op.target,op.source + same=(i<64)==(k<64) + def reversal(): + if f//2: + children.append(Child("orientation",k*f,(k+1)*f-f//2, + expression.unit_child(f//2))) + if same: + reversal() + if op.coefficient.kind=="pair": + child=expression.append("pair",request,low_matrix,expression.depth, + field=i,reverse=i>=64) + else: + need(op.coefficient.kind=="unit","fallback child grammar") + child=expression.unit_child(f) + children.append(Child(op.coefficient.kind,i*f,k*f,child)) + if same: + reversal() + operations=tuple((op.kind,op.target,op.source,op.coefficient.kind, + op.coefficient.reduction_index) for op in program) + children=tuple(children);branch="fallback" + need(len(children)<=32*64**2,"retained fallback allowance") + for child in children: + size=child.expression.size + need(0= minimum, "invalid integer domain") + + +@dataclass(frozen=True) +class Packet: + live: int + low: int + high: int + + def __post_init__(self): + for x in (self.live, self.low, self.high): + integer(x, 1) + + @property + def size(self): + return self.live * self.low * self.high + + def split(self, row, rows): + integer(rows, 1) + integer(row) + need(row < rows and rows % self.size == 0, "incomplete live packet") + unused = rows // self.size + prefix, quotient = divmod(row, unused) + prefix, high = divmod(prefix, self.high) + family, low = divmod(prefix, self.low) + return family, low, high, quotient + + def join(self, fields, rows): + integer(rows, 1) + need(rows % self.size == 0, "incomplete live packet") + radices = (self.live, self.low, self.high, rows // self.size) + need(len(fields) == 4, "wrong field count") + value = 0 + for x, radix in zip(fields, radices): + integer(x) + need(x < radix, "field outside its complete range") + value = value * radix + x + return value + + +def path_split(packet, row, depth, multiplicity): + integer(depth) + integer(multiplicity, 1) + integer(row) + need(row < multiplicity * packet.size**depth, "path row outside range") + fields = [] + for remaining in range(depth, 0, -1): + a, b, c, row = packet.split(row, multiplicity * packet.size**remaining) + fields.append((a, b, c)) + return tuple(fields), row + + +def path_join(packet, fields, tail, multiplicity): + integer(tail) + need(tail < multiplicity, "tail outside multiplicity") + row = tail + for level, triple in enumerate(reversed(fields), 1): + row = packet.join((*triple, row), multiplicity * packet.size**level) + return row + + +def depth(n): + integer(n) + answer = 0 + while n >= 64: + n = 42 * (n // 64) + answer += 1 + return answer + + +def validate_path_table(packet, d, t, table): + triples = list(product(range(packet.live), range(packet.low), range(packet.high))) + expected = set(product(product(triples, repeat=d), range(t))) + need(len(table) == t * packet.size**d, "lost arbitrary input row") + need(set(table) == expected, "incomplete or aliased descendant fibers") + for row, fields in enumerate(table): + need(path_join(packet, *fields, t) == row, "ancestor/row coordinate changed") + + +def layout_checks(): + rows_seen = cases = child_checks = 0 + for spec in ((2, 2, 1), (2, 2, 3), (3, 4, 1), (2, 6, 2)): + p = Packet(*spec) + for d in range(4): + for t in (1, 2): + count = t * p.size**d + table = [path_split(p, row, d, t) for row in range(count)] + validate_path_table(p, d, t, table) + rows_seen += count + cases += 1 + if d: + unused = count // p.size + for child_depth in range(d): + divisor = p.size**child_depth + need(unused % divisor == 0, "child reserve does not divide quotient") + expected = Counter({r: unused // divisor for r in range(divisor)}) + for ancestor in product(range(p.live), range(p.low), range(p.high)): + got = Counter(p.split(p.join((*ancestor, u), count), count)[3] % divisor + for u in range(unused)) + need(got == expected, "fresh child range depends on ancestor") + child_checks += 1 + p = Packet(2, 2, 1) + incompatible = [d for d in range(1, 9) if p.size**d % (3*p.low*p.high)**d] + need(incompatible == list(range(1, 9)), "old physical-format gate silently retained") + return dict(cases=cases, rows=rows_seen, child_fiber_checks=child_checks, + incompatible_physical_depths=incompatible) + + +def depth_checks(): + checks = 0 + for n in range(64, 10001): + for rank in range(1, 43): + need(depth(rank*(n//64)) < depth(n), "selected child consumes too many levels") + checks += 1 + for child in (n//64, (n//64)//2): + need(depth(child) < depth(n), "fallback depth mismatch") + checks += 1 + threshold = 64 + thresholds = [] + for d in range(1, 65): + need(depth(threshold) == d and depth(threshold-1) == d-1, + "inverse threshold boundary") + thresholds.append(threshold) + threshold = 64*((threshold+41)//42) + return dict(widths=10001, all_child_checks=checks, threshold_pairs=len(thresholds), + final_threshold=thresholds[-1]) + + +def compatibility_checks(): + cases = common_reserves = selected_boundaries = 0 + # Rational reduction supplies a second route to the required multiplicity. + for W, P, d, t, NH in product(range(1, 10), range(1, 14), range(7), + range(1, 31), (1, 6, 15)): + required = (Fraction(W, P)**d).denominator + need(((t*(W*NH)**d) % (P*NH)**d == 0) == (t % required == 0), + 'two-format acceptance mismatch') + cases += 1 + if t == 1: + need(lcm((W*NH)**d, (P*NH)**d) == (lcm(W, P)*NH)**d, + 'common fixed-format minimum mismatch') + common_reserves += 1 + W, P, NH = 28416, 28425, 6 + for d in range(13): + required = (Fraction(W, P)**d).denominator + need(required == 9475**d, 'selected compatibility factor changed') + for t in sorted({1, max(1, required-1), required, 2*required}): + need(((t*(W*NH)**d) % (P*NH)**d == 0) == (t % required == 0), + 'selected compatibility boundary') + selected_boundaries += 1 + return dict(exact_equivalences=cases, common_reserve_identities=common_reserves, + selected_depths=13, selected_boundaries=selected_boundaries, + required_selected_multiplicity='9475^D') + + +def wrapper(row, h, d, modulus): + # PR2234 ordinary wrapper, with an abstract row-uniform F_I on one atom. + d = (d-h) % modulus + h, d = d, h + d = (d+h) % modulus + h, d = d, h + d = (h-d) % modulus + return row, h, d + + +def restricted_payload(rows, genuine, radix, row_permutation=None): + """Push distinct arbitrary symbols through the completed abstract endpoint.""" + source = {(r, h, d): ((r, h, d) if r < genuine else None) + for r, h, d in product(range(rows), range(radix), range(radix))} + output = {} + for (r, h, d), value in source.items(): + rr, hh, dd = wrapper(r, h, d, radix) + rr = rr if row_permutation is None else row_permutation[rr] + output[rr, hh, dd] = value + return {key: value for key, value in output.items() if key[0] < genuine} + + +def padding_and_work_checks(): + cases = symbols = 0 + for reserve in (1, 4, 12, 16, 144): + for genuine in sorted({reserve, reserve+1, 2*reserve-1, 2*reserve+1}): + rows = ((genuine+reserve-1)//reserve)*reserve + need(genuine <= rows < 2*genuine and rows % reserve == 0, "padding bound") + for radix in (2, 3, 5): + got = restricted_payload(rows, genuine, radix) + want = {(r, h, d): (r, d, h) + for r, h, d in product(range(genuine), range(radix), range(radix))} + need(got == want, "completed endpoint does not preserve genuine rows") + cases += 1 + symbols += len(want) + dirty_source, dirty_target = frozenset({'s'}), frozenset({'t'}) + private = frozenset() + private ^= dirty_source + dirty_target ^= private + private ^= dirty_source + need(dirty_source == frozenset({'s'}) and dirty_target == frozenset({'s', 't'}) + and not private, "private copy/use/erase endpoint") + W, P = 28416, 28425 + bills = [] + for N in (1, 2, 48): + V = 7*W*N + v = Fraction(V, W*N) + occupied = V+4*v + B0 = W+4 + parked = 5*occupied-v+9*B0-2 + need(parked == 5*V+19*v+9*B0-2, "parking bill was undercharged") + need(P-W == 9 and B0 == 28420, "physical inventory changed") + bills.append(dict(low_classes=N, logical_volume=V, packet_volume=int(v), + occupied=int(occupied), parking=int(parked))) + return dict(padding_cases=cases, distinct_payload_symbols=symbols, work_bills=bills) + + +def controls(): + rejected = [] + def rejects(name, action): + try: + action() + except (ValueError, TypeError): + rejected.append(name) + else: + raise ValueError('accepted defect: '+name) + p = Packet(2, 2, 3) + valid = [path_split(p, r, 2, 1) for r in range(p.size**2)] + rejects('omit_high_fibers', lambda: validate_path_table(p, 2, 1, valid[:16])) + rejects('short_reserve', lambda: p.split(0, p.size**2-1)) + alias = list(valid); alias[-1] = alias[0] + rejects('alias_one_dirty_row', lambda: validate_path_table(p, 2, 1, alias)) + swapped = list(valid); swapped[0], swapped[1] = swapped[1], swapped[0] + rejects('multiset_only_row_restoration', lambda: validate_path_table(p, 2, 1, swapped)) + rows, genuine, radix = 8, 5, 2 + perm = list(range(rows)); perm[0], perm[7] = perm[7], perm[0] + rejects('padded_row_leaks_into_genuine', lambda: need( + restricted_payload(rows, genuine, radix, perm) == + restricted_payload(rows, genuine, radix), 'dummy leakage')) + rejects('physical_live_denominator', lambda: need(Fraction(28416, 28425) == 1, + 'P is not live W')) + rejects('drop_physical_compatibility_factor', lambda: need( + (28416*6)**2 % (28425*6)**2 == 0, 'missing 9475^D multiplicity')) + rejects('private_starts_dirty', lambda: need(not (frozenset({'u'}) ^ + frozenset({'s'}) ^ frozenset({'s'})), 'private not erased')) + rejects('erase_arbitrary_input_for_scratch', lambda: need(frozenset() == + frozenset({'u'}), 'arbitrary input lost')) + rejects('omit_work_buffers', lambda: need(5*100-1+9*28420-2 == + 5*(100+4)-1+9*28420-2, 'four buffers remain paid')) + rejects('nonpositive_packet', lambda: Packet(0, 2, 3)) + rejects('boolean_cardinality', lambda: Packet(True, 2, 3)) + return rejected + + +def source_checks(): + raw = (HERE/'PREDECESSORS.json').read_bytes() + need(hashlib.sha256(raw).hexdigest() == PREDECESSOR_PIN, 'predecessor manifest changed') + manifest = json.loads(raw) + need(len(manifest) == 6, 'incomplete predecessor inventory') + for item in manifest: + data = (HERE/item['path']).read_bytes() + need(len(data) == item['bytes'], 'source size mismatch') + need(hashlib.sha256(data).hexdigest() == item['sha256'], 'source SHA256 mismatch') + need(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + == item['git_blob'], 'source Git blob mismatch') + proof = (HERE/'sources/pr2195/PROOF.md').read_text() + caller = (HERE/'sources/pr2234/PROOF.md').read_text() + need('W=28,416 live families and P=W+9=28,425' in proof, 'live/work source binding') + need('explicit alternative layout with an overreserve' in proof, 'predecessor scope binding') + need('5V+19v+9B0-2' in caller, 'parking source binding') + need('Allocate private and selector copies as work, not arbitrary input rows' in caller, + 'separate work source binding') + return {'predecessor_files': len(manifest), 'executed_predecessor_code': False} + + +def certificate(): + return {'status':'PASS_SELECTED_LIVE_ROW_DIVISOR', 'scope':'conditional fixed-format theorem; no_new_kappa', + 'selected': {'live':28416, 'physical':28425, 'private_inventory':9, + 'old_lcm':lcm(28416,28425), 'removed_factor_per_depth':lcm(28416,28425)//28416, + 'new_packet':'28416*|GL64(F_q)|*q^(4096*(w-1))'}, + 'sources':source_checks(), 'layouts':layout_checks(), 'depth':depth_checks(), + 'compatibility':compatibility_checks(), + 'padding_and_work':padding_and_work_checks(), 'rejected_controls':controls()} + + +def canonical(x): + return json.dumps(x, sort_keys=True, separators=(',', ':'), ensure_ascii=True) + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument('--write-receipt', type=Path) + args = ap.parse_args() + result = certificate() + if args.write_receipt: + with args.write_receipt.open('x') as stream: + stream.write(json.dumps(result, indent=2)+'\n') + else: + need(canonical(result) == canonical(json.loads((HERE/'RESULT.json').read_text())), + 'stored receipt differs from exact replay') + print(json.dumps(result, indent=2)) + print('PASS_SELECTED_LIVE_ROW_DIVISOR factor=9475^D no_new_kappa') + + +if __name__ == '__main__': + main()