diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 582e416aaf..4541cfa0e8 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -5,6 +5,25 @@ Start with the [selected record](../certificates/selected-result.json). Its `reproduce`, `review`, `source_manifest` and `validation` fields identify the replay command, scoped assessment, source bindings and integration evidence. +The selected checkpoint is #4359, documented in +[the proof review](research/pr-intake-evidence/pr4359/PROOF-REVIEW.md), +[the source manifest](../certificates/frontier4359-source.json) and +[the validation receipt](research/pr-intake-evidence/pr4359/VALIDATION.json). +The public cold replay is `make frontier4359-verify`; the configured +[frontier4359 workflow](../.github/workflows/frontier4359.yml) executes it +on Ubuntu 24.04 with Python 3.12 and the pinned requirements. Consult +[the integration receipt](research/pr-intake-evidence/pr4359/INTEGRATION.json) +and [workflow runs](https://github.com/CrocSwap/integer-mult-bounds/actions/workflows/frontier4359.yml) +for dated evidence and exact tested heads. + +`make selected-record-check` checks metadata and source/proof hashes. The +finite replay and changed-interface review retain the native/physical, +analytic, precision, fixed-tape and recovery hypotheses in the selected +record; they are not a full formal multiplication theorem. The winning +uniform templates are algorithm-defined and are not materialized. + +## Historical checkpoint through #1094 + At this checkpoint, the selected composition is #589 with #1094, documented in [the review](research/community-batch1099-review.md), [the source manifest](../research/community-frontier1094-audit/SELECTED-SOURCE.json) diff --git a/docs/research/current-status.md b/docs/research/current-status.md index 62a8cbb097..043a8cd78a 100644 --- a/docs/research/current-status.md +++ b/docs/research/current-status.md @@ -1,12 +1,14 @@ # Current reviewed status -Selected conditional κ: **0.0023 = 23/10000**, zxv’s #4359 productive-helper construction, using Jacob Alan Sussman’s mixed-target recursion and the credited cumulative native/outer lineage. +Selected conditional κ: **0.0023** = 23/10000, zxv’s #4359 productive-helper construction, using Jacob Alan Sussman’s mixed-target recursion and the credited cumulative native/outer lineage. [Selected record](../../certificates/selected-result.json) · [Proof review](pr-intake-evidence/pr4359/PROOF-REVIEW.md) · [Integration receipt](pr-intake-evidence/pr4359/INTEGRATION.json) · [Contributors](community-productive4359-contributors.md). Cold replay: `make frontier4359-verify`. The fresh 23-stage replay and 59 normalized artifacts pass; the changed interfaces have an AI-assisted proof review under retained analytic/native/fixed-tape hypotheses. Winning uniform templates are not materialized. This is not a complete formal or independent human verification. #4404 independently checks a narrower arithmetic/flow scope. -## Historical selected status through #1094 +The sections below are a historical snapshot; consult the selected record above for present status. + +## Historical checkpoint through #1094 Historical selected conditional κ: **0.001672660197076918**, Rohan Arun's #1094 on Jeremy Kothe's #1087 packing and the cumulative k8/slot/T16 construction. The bit supplier remains #589 on #555. diff --git a/research/direct-mixed-flow/.gitattributes b/research/direct-mixed-flow/.gitattributes new file mode 100644 index 0000000000..2435bfdf63 --- /dev/null +++ b/research/direct-mixed-flow/.gitattributes @@ -0,0 +1 @@ +vendor/** -text -whitespace diff --git a/research/direct-mixed-flow/README.md b/research/direct-mixed-flow/README.md new file mode 100644 index 0000000000..3be00f754b --- /dev/null +++ b/research/direct-mixed-flow/README.md @@ -0,0 +1,496 @@ +# Direct mixed flow and explicit compiler size: a partial research checkpoint + +**Publication authorized by the user on October 21, 2026.** This is a partial +compiler/resource checkpoint; the direct exponent gate remains open. + +The target is a structural successor to +[PR4433](https://github.com/CrocSwap/integer-mult-bounds/pull/4433): remove the +tensor/padding step needed by overlapping ranks and control the complete +finite compiler's size. The user requested a significance target twice the +previous contribution. That is an ambitious scope target, not a numerical +measurement or a claim that it has been achieved. + +Two results are established under the source native-word hypotheses: + +1. A **finite chronological integer flow** works when paid ranks overlap + target ranks, provided `max paid < ambient`. It retains and pays every + unmatched job as an exit. All recursive ranks decrease. This gives a + finite uniform compiler, **without a proved near-root saving**. +2. Choosing **nested divisible widths** gives `B_N <= exp(O(N log N))`. + Exact rank-one accounting also bounds raw instances, owned centers, + routing slots and the source finite-constant envelopes. This batching + choice preserves the normalized leaf cost and therefore applies to the + already supported PR4433 supplier. + +The main exponent target remains open. Exact compilation at rank 1,000 on +the raw p7 profile fails the desired saving. That finite failure is not an +asymptotic obstruction, and it does not invalidate PR4433's separated recipe. +No new κ, selected frontier, native admission or physical runtime is claimed. + +## 1. Source boundary and decision + +The starting point is Jacob Alan Sussman's multinomial lockstep construction, +retained by PR4359. Its separated proof requires `r_max < k_min` so every +parent output is consumed. PR4416 and PR4433 instead repair the raw p7 +overlap by chronological products, paid completion and splitting. + +Retain the four native hypotheses of +[FINITE-PRECOMPILATION.md](vendor/FINITE-PRECOMPILATION.md): a correct +all-column arbitrary-input word, disjoint splitting with complete spectators, +permitted and priced whole-job adapters, and finite-program closure with +owned initialization/erasure. Equal rank alone does not supply an adapter. +Changed finite combinatorics do not independently admit those hypotheses. + +**Continue, with two separate gates.** The finite-flow gate is now proved and +checked. The exponent gate requires a new uniform estimate on the complete +complement-plus-exit recurrence. Do not expand a search solely because a +moment root is favorable. The size theorem is useful independently, since +the predecessor leaves productive width and owned-instance counts implicit. + +| Obligation | Evidence / remaining work | +| --- | --- | +| Integer matching with overlapping ranks | Proved below; literal and merged replays agree | +| Chronological return and strictly smaller exits | Proved under `r_max < m`; no cross-round matching | +| Source complements and full uniform output | Source integer-batch induction, with nested divisible widths | +| Direct near-root saving | **Open**; rank 1,000 fails; no global conclusion | +| Productive width, rank-one leaves, raw instances, owned centers | Explicit bounds below, with exact finite controls | +| Routing slots, encoded records and source finite-constant envelopes | Counted below in the stated grammar; physical implementations retain their own tariffs | +| Native all-column, physical, analytic, precision and recovery premises | Inherited; no full replay or new admission | + +## 2. Partially matched integer lockstep flow + +Let positive integer target multiplicities be W_k, chronological paid rounds +have ranks r_j, and let + +``` +2 <= k_min <= m=max(k), 1 <= r_max < m. +``` + +The paid word may have `r_max >= k_min`. At a fixed integer top rank n>=m, +put + +``` +c(a) = product_k k^a_k, +u(a) = multinomial(|a|;a) product_k W_k^a_k, +R(rho) = {a : m*rho*c(a) <= n}, +G = floor(log_(k_min)(floor(n/m))). +``` + +For every paid-round path s of length d<=G with multiplier rho_s, instantiate +u(a) units at column rho_s*c(a), for every point a in R(rho_s) of degree +G−d. This is the source class construction. For a parent class with +multiplier rho, its rank-r round supplies u(b) jobs at point b when b is +present. The child demand at that point is + +``` +D(b) = sum over eligible (b−e_k) of W_k*u(b−e_k). +``` + +The complete Pascal sum is u(b). Therefore: + +- If the parent point b exists, `0 <= D(b) <= u(b)`. Route D(b) of the + **whole** issued jobs to the child. Complete the remaining u(b)−D(b) + jobs as paid exits, at their actual rank `e=r*rho*c(b)`. +- If the parent point is absent, supply the child demand with new distinct + top input arrays. These are source jobs, not copies of issued data. +- At depth G, every point has degree zero; all paid jobs are exits. + +No fractional jobs, cloned productive inputs or uncharged discarded requests +are introduced. Within each point, choose a fixed enumeration of parent +jobs and target slots and match their first D(b) elements. The rest have +explicit endpoints and remain on their actual owners. + +### Sources and exits + +At the root, every demanded point has degree G+1, so it is outside R(1). +Its rank s is in `(n/m,n]`. A non-root source has no parent point, hence +`m*rho_parent*c(b)>n`; its rank is `r*rho_parent*c(b)>r*n/m>=n/m`. +Its eligible child target ensures s<=n. Thus every source is a positive +job in `(n/m,n]`. + +Every exit belongs to an actual parent unit, so + +``` +e <= r_max*n/m < n. +``` + +This holds for the new premature exits as well as leaf exits. A premature +exit has at least one omitted Pascal term, with +`m*r*rho*c(b)/k > n`; consequently `e > k_min*n/m`. These are large exits +near the upper boundary. They cannot be assigned the old bound +`r_max*(n/m)^theta` with theta<1. That lost estimate is the exponent issue. + +### Chronology and arbitrary inputs + +Run all scalar steps of a class in their specified order. At paid position +j, issue that position for every unit, partition its whole issued jobs into +matched and unmatched slots, finish all unmatched exits and the entire child +class, restore adapters, and only then resume position j+1. The child takes +incoming jobs from this one parent round plus its new top sources. It never +waits for a later round of a suspended parent. The finite class depth is G; +all complement and exit calls have rank below n, so their uniform programs +are already available by strong induction. + +Distinct slots in one class have distinct physical fields. Routing fewer +parent slots than the original full-Pascal construction preserves this +property. Arbitrary-input native correctness permits correlated values, +including current owned-center contents; it does not permit field aliasing +or extra productive credit. Each unit has its own owned identities and +retains them until its word clears them. These requirements are unchanged. + +### Exact potential and count identities + +Let S_s and E_e be integer source and exit inventories, U the unit count, +and Qcol the sum of the units' positive integer column multiplicities. +Cancellation of matched jobs gives, exactly at rank one, + +``` +sum_s S_s*s − sum_e E_e*e = Delta * Qcol, +Delta = sum_k W_k*k − sum_j r_j. +``` + +At any real exponent t, the corresponding identity is + +``` +sum_s S_s*s^t − sum_e E_e*e^t + = (T_t−P_t) * sum_units column^t. +``` + +Thus a favorable raw t-moment survives as a superpotential. It does **not** +by itself pay the source complements. Writing W=sum W_k and P=number of +paid rounds, complete untruncated layer counts give + +``` +U <= sum_(d=0..G) P^d W^(G−d) <= (W+P+1)^(G+1), +S := sum_s S_s <= W*U, +sum_e E_e <= P*U. +``` + +The source package's separated case is unchanged: no premature exits occur. +The verifier compares it with the byte-identical predecessor literal replay. + +## 3. Nested divisible widths and complete count bounds + +Use the ordinary base B_n=1, P_n=n below m, with B_0=1 and P_0=0. For n>=m +choose the replication factor and productive width + +``` +a_n = B_(n−1), B_n = a_n*S_n. +``` + +Every earlier width B_e divides B_(n−1), by induction. Therefore every +source-complement batch and exit batch is an integer number of smaller +uniform programs. This is a concrete choice within the source compiler's +existing denominator-clearing freedom; no optimum is claimed. Its previous +option to use an LCM is retained as predecessor context. + +As in the source compiler, each of the a_n*S_n original arrays first gets +its disjoint complementary job, then its one source job through the flow. +All exits are completed by smaller uniform programs. The result is a full +rank-n transform on every original array. Owned storage is excluded from B_n. + +The normalized leaf count satisfies the **same exact recurrence** for any +valid replication choice: + +``` +L(n) = (1/S_n) * [sum_s S_s L(n−s) + sum_e E_e L(e)]. +``` + +Changing the replication factors changes width and total counts equally. +It does not spend supplier saving or alter any outer parameter. + +For a fixed final N and h=G(N), all n<=N satisfy + +``` +S_n <= C_N := W*(W+P+1)^(h+1), +B_N = product_(n=m..N) S_n <= C_N^N. +``` + +Since h=O(log N), **log B_N=O(N log N)** for a fixed mixed rule. Repeatedly +multiplying all previous widths is unnecessary. This bounds one explicit +realization; the original compiler did not require that inefficient choice. + +If Delta>0, telescope rank-one mass over the fully expanded uniform program: + +``` +B_N*N − P_N = Delta * Qcol_N, +U_N <= Qcol_N <= B_N*N/Delta. +``` + +All raw columns are positive integers, which gives the middle inequality. +Thus paid leaves and raw instances have the same `exp(O(N log N))` bound. +With one owned center per raw unit, the center count is at most U_N. A rule +with O_local distinct owned banks per invocation instead gets O_local*U_N. +Extra router scratch must be counted separately. + +### Routing and word description + +Count one routing slot for every source, every exit, every unit target slot +and every unit paid position. At one flow its count is at most +`2*(W+P)*U`. The same bound telescopes over all recursive calls, because +each call contributes its own local unit instances. Exact compilation checks +this identity alongside widths and leaves. + +In the macro grammar that records a whole-job adapter, inverse adapter or +whole-field move as one record, a slot can be handled with at most sixteen +records: up to two whole-job conjugations and their inverses, park/load/ +return/reorder moves, and explicit scratch initialization and erasure. +Allocate separate owned scratch for those moves when needed; no zero-cost +routing or free copying is assumed. Let A bound the fixed unit's complete +nonrecursive record count, owned operations and scalar coefficient heights. +The final weighted record allowance satisfies the conservative bound + +``` +R_bar <= A*U_N + 32*(W+P)*U_N + P_N + <= (A+32*(W+P)+1)*B_N*N, for Delta>=1. +``` + +R_bar bounds both the macro count and the sum of scalar-height and native +record allowances. Every owned bank has an explicit initialization record, +so total allocated owned banks can also be bounded by R_bar; the sharper +raw-center bound remains separate. This is a **description/record bound**, +not a new tariff for executing a +general matrix or permutation. A Gaussian monomial adapter's dense binary +address matrix and quadratic phase have O(N^2) descriptor bits. Explicit role indices add O(log B_N) +bits. Thus an encoding of this finite word still has +`exp(O(N log N))` bits for a fixed unit and its finite coefficient alphabet. +If physical expansion of one adapter needs F(N) native records, multiply +the routing term by its actual F(N). That physical implementation, coefficient +heights and tape costs remain separately priced native obligations. They +are not set to zero by the macro bound. + +## 4. Applying the size result to PR4433 + +The new nested widths may be used in the separated compiler of PR4433. +Its normalized L(n), ambient N, uniform saving and outer ledger remain +unchanged. Therefore this application does not need the still-open direct +exponent lemma. + +With `v=150`, `H=349300000000`, `N=2^H`, the completed mixed rule has + +``` +W = 7688^150 < 2^1950, +P <= 131115^150 + 7688^150*15^150 < 2^2701, +W+P+1 < 2^2702. +``` + +The bound on P counts every original and completion call by its positive +rank mass; splitting preserves that mass. Since k_min>=2, h<=H. Set + +``` +D = 1950 + 2702*(H+1) = 943808600004652. +``` + +There is consequently a realization of the same proposed conditional +κ=0.00268647 supplier satisfying + +``` +B_N < 2^(D * 2^H), +P_N < B_N * 2^H. +``` + +More finely, after expanding every product, padding, split and compiler call +back to the raw p7 word, that word has surplus 608. Product/completion/split +boundaries cancel, so + +``` +B_N*N − P_N = 608 * sum_raw_p7_instances column, +U_raw <= (B_N*N − P_N)/608. +``` + +This is also an explicit bound on raw p7 center banks under the safe +one-center-per-instance allocation. These are large upper bounds, not +emitted words, smallest widths or practical precision estimates. They replace +one implicit part of the source finite-constant prescription. The native +adapter bodies, analytic transfer and physical costs retain their original +conditions; a closed bound for the source's finite-constant prescription is +given next, without a new physical runtime or exact-recovery threshold. + +### A closed envelope for the source finite constants + +The exported THREE-base native word has exactly 22,633 records in each +orientation. Source-bound counting retains all 15 copies, the literal p7 +controller, scalar allowance 2,490,856, every productive/paid/contact/helper/ +idle slot, and all routing and owned operations. A raw macro allowance is + +``` +A_raw = 15*8*(decompressed native JSON bytes) + + 8*(literal controller JSON bytes) + + 32*(2490856 + all declared slots + 15*22633) < 2^40. +``` + +The payload-bit terms overcount the coefficient literals and full local +descriptors, including both orientations. The 32-per-slot term overcounts +whole-job normalizers and inverses, field movements, initialization and +erasure. It is a bound on the declared source word in this grammar, not +independent verification of its functional correctness or physical tariffs. + +For the chronological v-fold product, its number of raw p7 invocations is + +``` +U_v = sum_(i=0..v−1) 7688^(v−1−i)*55998^i < 2^2392. +``` + +At every product level retain the whole-job matching wrappers. A conservative +product allowance is + +``` +A_product <= (2^40 + 32*v*(7688+55998+1))*U_v + 32*v*55998^v. +``` + +Add 32 records for every final paid call, completion role and original paid +position. Counting paid calls by their rank mass gives + +``` +A_completed <= A_product + + 32*(131115^v + 7688^v*15^v + 7688^v + 55998^v). +``` + +A dense local binary map/quadratic phase and role index fit in +`64*(121^v)^2` bits per such record. The verifier checks the integer bound +`A_completed * 64*(121^v)^2 < 2^5000`. Thus **A=2^5000** is a valid weighted +record/description allowance for this fixed completed unit. It includes all +source coefficients and owned operations, with a large deliberate overcount. +No instruction list of the completed product is emitted. + +Since `A+32*(W+P)+1 < 2^5001`, use the envelope + +``` +R_bar < 2^(D*2^H + H + 5001). +``` + +Apply the existing source finite-constant prescription to the **newly expanded +word**. With Z=B_N+owned banks, G its scalar coefficient envelope, and P_N +its rank-one leaves, we have `Z<=2*R_bar`, `G<=8*R_bar`, `P_N<=R_bar` and +`N<=R_bar`. Therefore + +``` +E = 64*(Z+N+P_N+G+1)^3 + < 2^(3*D*2^H + 3*H + 15021), +B_constant = P_N+E, +C0 = 32*N*B_constant^2 + < 2^(6*D*2^H + 7*H + 30049) + < 2^(8*D*2^H). +``` + +The last comparison uses `2^H>=H+1` and an exact polynomial integer check +on D and H. These are explicit, very loose upper bounds for the inherited +semantic precision/stock constants, conditional on that source prescription +and its admitted native record implementations. The exact numerical outer +input threshold, prime exclusions and physical tape costs remain separate. + +## 5. Exact finite checks and the open exponent gate + +The verifier uses no floating-point acceptance tests. It checks: + +- Nine literal/merged flows at ranks 20, 40 and 80: a separated control, + strict overlap `{2:1,5:1} <- {1:2,4:1}`, and Sussman's open equality + example `{2:4,3:1} <- {1:6,2:2}`. Every whole input and exit agrees. +- The separated control agrees with the unchanged Sussman literal replay. +- Complete nested-width compilations through rank 100 on both overlap + examples, checking every recursive batch, routing count and rank identity. +- Raw p7 through rank 1,000: **880 exact nonbase compilations**. B_1000 has + 17,504 bits; the saved receipt binds all large computed integers by their + unsigned big-endian hashes, avoiding enormous decimal dumps. +- Removing premature exits violates mass conservation. Removing batch + replication fails integer divisibility. Allowing a paid rank equal to + the ambient rank is rejected because strict rank descent is unavailable. + +For raw p7 at rank 1,000, exact arithmetic gives + +``` +L(1000) > 990 > 1000^(1−0.00268647). +``` + +The second comparison is elementary and exact: `ln(2)>2/3` from its first +atanh term and `1000>2^9` give `ln(1000)>6`. Then +`1000^κ > 1+6κ > 100/99`. No log approximation is used in this rejection. +This checks one finite failure and keeps it distinct from the infinite-rank +question. + +The missing lemma is a uniform bound on the **whole** recurrence. For some +fixed p and sufficiently large n, one would need, for example, + +``` +sum_e E_e e^t (1+log2(e))^p + + sum_s S_s (n−s)^t (1+log2(n−s))^p + <= S_n n^t (1+log2(n))^p, +``` + +with zero-rank terms defined separately and a correctly funded base range. +The premature exits have rank proportional to n. Their logarithmic factors +cannot use the old fixed theta<1 power contraction. A raw moment advantage +alone does not prove this inequality. + +Exploratory `approximate_leaves` in flow.py evaluates the recurrence in +floating point and is deliberately excluded from verification. A bounded +run through 20,000 ranks found saving about 0.000827 for the default height; +varying the height did not approach 0.00268647 there. This is local search +evidence, not a lower bound or a reason to enlarge the same scan. A better +boundary estimate or a changed flow is the next research obligation. + +## 6. Reproduction and provenance + +Python 3.12, standard library only: + +```sh +python3.12 -B research/direct-mixed-flow/verify.py +python3.12 -B scripts/research_package.py --package research/direct-mixed-flow --check-only +python3.12 -B scripts/research_package.py --package research/direct-mixed-flow +``` + +Use `verify.py --out /absolute/new/result.json` for a fresh receipt. +[RESULT.json](RESULT.json) contains exact flows, integer compilation hashes, +symbolic size bounds and negative controls. `flow.py` is the new algorithm; +the verifier independently compares its merged and literal traversal outputs. +Those are two internal implementations, not an independent mathematical review. + +Canonical base is `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority revision +7. SOURCES.json pins orientation metadata. VENDOR.json separately binds eleven +unchanged exports by commit, full path, Git blob and SHA256. Their bytes and +notices are preserved; direct replay needs no foreign Git objects. The source +theorem and earlier finite compiler remain attributed hypotheses, not new work. + +Local validation used Python 3.12.8 on macOS arm64. The registered replay, +metadata/pin check and committed-byte preflight passed. A separate Git-free +copy passed with `python3.12 -I -O -B verify.py`; changed-native-source and +changed-receipt controls both rejected. Replay uses exact integer arithmetic +and source hashes, with no network or foreign Git objects. The repository is +shallow, so a full source-history preflight was not attempted. No Lean, Docker, +full native/all-column admission, physical adapter expansion or historical +suite was run. Independent mathematical acceptance remains open. + +The overlap refresh at 18:48 UTC covered 538 open PR bodies and 3,280 +discussion/comment records, with complete reported pagination. Specific +searches for direct overlapping-rank compilers, Pascal matching and nested +widths found no matching public item in that scope; this is not a novelty +certificate. Existing PR4433 supplies the fixed-rank application, and the +source theorem explicitly leaves the unseparated exponent open. No Discussion +claim or PR has been posted for this partial checkpoint. + +## Open next questions + +1. **Close or refute the direct exponent gate for this capped flow.** Start + with a proved bound on premature-exit potential relative to the actual + complement capacity. This decides whether the flow can replace the + tensor/padding layer. A larger rank scan is not a uniform proof. +2. **Independently admit the physical expansions and precision prescription.** + Audit the conservative A allowance against the actual native caller and + bind every adapter's physical implementation, row movements and recovery + exclusions. The encoded constants above use the inherited semantics; + description size is not a physical execution tariff. +3. **Tighten the constructive width.** The nested product is an explicit + upper bound, not an optimized LCM. A useful next step would control prime + valuations of the actual source counts; another arbitrary batching choice + would not by itself establish a smaller physical supplier. + +Prepared by zxv with substantial OpenAI Codex assistance in research, code +and writing. No subagents or independent human mathematical review were +used. New material is Apache-2.0. The integer lockstep/Pascal construction +and original open unseparated question are Jacob Alan Sussman's work, retained +at upstream `wht-power-saving-lean` commit +`563b4e6e913625637f36ba7869bf5fcd0dd4975a`; its LICENSE and NOTICE are included. +PR4359 supplies the native finite-precompilation bridge and p7 predecessor +lineage. PR4416's p7 product/padding is @1337isnot1337's work. PR4433 supplies +the unchanged sufficient rank. Their original contributor credit remains +in the authenticated exports. diff --git a/research/direct-mixed-flow/RESULT.json b/research/direct-mixed-flow/RESULT.json new file mode 100644 index 0000000000..e657f58b5a --- /dev/null +++ b/research/direct-mixed-flow/RESULT.json @@ -0,0 +1,505 @@ +{ + "direct_exponent_theorem_established": false, + "exact_p7_direct_compilation": { + "column_mass": { + "bits": 17497, + "unsigned_big_endian_sha256": "0f2b521412ca3f565d734c244b1cf42b8c7d49ef1e61af197ec97b2605078a3c" + }, + "leaves_per_array": { + "lower": "24890741110487842821/25000000000000000", + "upper": "995629644419513712841/1000000000000000000" + }, + "n": 1000, + "nested_batch_checks": 880, + "paid_above_99_percent_linear": true, + "paid_rank_one_leaves": { + "bits": 17514, + "unsigned_big_endian_sha256": "1f28a559d21f0df473b67fef0c37eb57144955250234a44c998bd837d1e8f3d6" + }, + "productive_width": { + "bits": 17504, + "unsigned_big_endian_sha256": "49727d4435d62a4a84b79cf2451d374a5bb98234cbe460ec0b0ef3da77c8c9e6" + }, + "rank_one_surplus": 608, + "raw_instances": { + "bits": 17497, + "unsigned_big_endian_sha256": "0f5ce7310a89be0835b71681538c3e2e57134d2690ff663b8bc1cd10938b9c7f" + }, + "routing_slots": { + "bits": 17514, + "unsigned_big_endian_sha256": "98bde80b4a7bc886645e82f3b9e730545da94beddcbec4e98ce88e1c44a39242" + }, + "source_count_upper": 31182789153672, + "target_failure": { + "kappa": "268647/100000000", + "proved": "L(1000) > 990 > 1000^(1-kappa)", + "scope": "This particular finite rank fails; no asymptotic impossibility claim." + }, + "width_exponent_envelope": 45000 + }, + "exact_toy_compilations": [ + { + "column_mass": { + "bits": 438, + "unsigned_big_endian_sha256": "f469278cd8f6190ffe6a1ae190299a8d183d1675d4280087d107e5d7016aee25" + }, + "leaves_per_array": { + "lower": "63955485748643768733/1000000000000000000", + "upper": "31977742874321884367/500000000000000000" + }, + "n": 100, + "nested_batch_checks": 96, + "paid_above_99_percent_linear": false, + "paid_rank_one_leaves": { + "bits": 439, + "unsigned_big_endian_sha256": "7df4f5875466fa21b225c2b60317e60536fdededbe8473d18fe5fb3fb057bb6f" + }, + "productive_width": { + "bits": 433, + "unsigned_big_endian_sha256": "35f12bcc6000b703565e2f120e8077641f744909e8ec163921775b2b0c139254" + }, + "rank_one_surplus": 1, + "raw_instances": { + "bits": 436, + "unsigned_big_endian_sha256": "12b6d174870cd23fd40ad1f4ff56df629ed813fabbbfcf143a914bfdd875609d" + }, + "routing_slots": { + "bits": 439, + "unsigned_big_endian_sha256": "4034ff94efe1f1ab70575b300eebbd2469e9065861c4f2570a59256c47170f74" + }, + "source_count_upper": 15552, + "width_exponent_envelope": 1400 + }, + { + "column_mass": { + "bits": 1007, + "unsigned_big_endian_sha256": "f04dcf1684cd1a5f5708102f230375fb43cd08135626ac91b22478876e21c63e" + }, + "leaves_per_array": { + "lower": "65003740439870989333/1000000000000000000", + "upper": "32501870219935494667/500000000000000000" + }, + "n": 100, + "nested_batch_checks": 98, + "paid_above_99_percent_linear": false, + "paid_rank_one_leaves": { + "bits": 1008, + "unsigned_big_endian_sha256": "1302eac01cf514d2855c821612c64c9d38a6c9ff55f12115f72bf34a9906b9d5" + }, + "productive_width": { + "bits": 1002, + "unsigned_big_endian_sha256": "398043f007044ec4c1ba14eda89bf66b48733ce7a22bb855a3bc17a4665b5952" + }, + "rank_one_surplus": 1, + "raw_instances": { + "bits": 1006, + "unsigned_big_endian_sha256": "ebd327c71dde99fefa5afb70ef8ad5b207723935abb8bed0473a95d67e73fbe7" + }, + "routing_slots": { + "bits": 1010, + "unsigned_big_endian_sha256": "23f8f6398dbe8fe43a321ff79a6c52edfee5c4de97ff2852a6cdcc6c127e7cd7" + }, + "source_count_upper": 37647680, + "width_exponent_envelope": 2600 + } + ], + "existing_supplier_size_bounds": { + "D": 943808600004652, + "H": 349300000000, + "N": "2^349300000000", + "compiled_record_upper": "R < 2^(D*2^H + H + 5001)", + "completed_unit_description_upper": "2^5000", + "kappa": "268647/100000000", + "owned_p7_center_bound": "one per raw instance; <= B_N * 2^H / 608", + "paid_leaf_bound": "P_N < B_N * 2^H", + "physical_scope": "Encoded whole-job adapter/move records. Their permitted physical implementation and tariffs remain inherited, separately priced premises.", + "raw_macro_allowance_upper": "2^40", + "raw_macro_and_payload_allowance": 319592968, + "raw_native_record_counts": { + "backward": 22633, + "forward": 22633 + }, + "raw_p7_instance_bound": "U_raw <= (B_N * 2^H - P_N)/608", + "routing_macro_record_bound": "R <= (A + 32*(W+P) + 1) * B_N * N; A < 2^5000", + "routing_slot_bound": "slots <= 2*(W+P)*V, V completed-unit instances", + "source_C0_upper": "C0 < 2^(8*D*2^H)", + "source_precision_E_upper": "E < 2^(3*D*2^H + 3*H + 15021)", + "width_bound": "B_N < 2^(D * 2^H)", + "winning_uniform_word_materialized": false + }, + "finite_flows": [ + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 18, + "exits": { + "1": 16, + "2": 16, + "4": 4 + }, + "height": 1, + "matched_jobs": 18, + "minimum_source": 9, + "n": 20, + "rank_one_surplus": 2, + "source_count": 9, + "sources": { + "12": 4, + "16": 1, + "9": 4 + }, + "unit_count_upper": 9, + "units": 9 + }, + "literal_classes": 7, + "paid": { + "1": 4, + "2": 2 + }, + "rule": "separated-control", + "targets": { + "3": 2, + "4": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 180, + "exits": { + "1": 64, + "2": 96, + "4": 48, + "8": 8 + }, + "height": 2, + "matched_jobs": 132, + "minimum_source": 12, + "n": 40, + "rank_one_surplus": 2, + "source_count": 42, + "sources": { + "12": 16, + "16": 4, + "24": 8, + "27": 8, + "32": 2, + "36": 4 + }, + "unit_count_upper": 63, + "units": 58 + }, + "literal_classes": 43, + "paid": { + "1": 4, + "2": 2 + }, + "rule": "separated-control", + "targets": { + "3": 2, + "4": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 244, + "exits": { + "1": 64, + "2": 96, + "4": 48, + "8": 8 + }, + "height": 2, + "matched_jobs": 162, + "minimum_source": 27, + "n": 80, + "rank_one_surplus": 2, + "source_count": 27, + "sources": { + "27": 8, + "36": 12, + "48": 6, + "64": 1 + }, + "unit_count_upper": 63, + "units": 63 + }, + "literal_classes": 43, + "paid": { + "1": 4, + "2": 2 + }, + "rule": "separated-control", + "targets": { + "3": 2, + "4": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": { + "16": 1 + }, + "column_mass": 28, + "exits": { + "1": 8, + "16": 5, + "4": 12 + }, + "height": 2, + "matched_jobs": 8, + "minimum_source": 5, + "n": 20, + "rank_one_surplus": 1, + "source_count": 14, + "sources": { + "10": 2, + "20": 5, + "5": 4, + "8": 3 + }, + "unit_count_upper": 19, + "units": 11 + }, + "literal_classes": 13, + "paid": { + "1": 2, + "4": 1 + }, + "rule": "strict-overlap", + "targets": { + "2": 1, + "5": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": { + "32": 5 + }, + "column_mass": 132, + "exits": { + "1": 16, + "16": 12, + "32": 5, + "4": 32 + }, + "height": 3, + "matched_jobs": 40, + "minimum_source": 10, + "n": 40, + "rank_one_surplus": 1, + "source_count": 30, + "sources": { + "10": 8, + "16": 3, + "20": 10, + "25": 4, + "40": 5 + }, + "unit_count_upper": 65, + "units": 35 + }, + "literal_classes": 40, + "paid": { + "1": 2, + "4": 1 + }, + "rule": "strict-overlap", + "targets": { + "2": 1, + "5": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": { + "40": 4, + "64": 5 + }, + "column_mass": 872, + "exits": { + "1": 32, + "16": 80, + "4": 80, + "40": 4, + "64": 29 + }, + "height": 4, + "matched_jobs": 132, + "minimum_source": 20, + "n": 80, + "rank_one_surplus": 1, + "source_count": 106, + "sources": { + "20": 36, + "25": 8, + "32": 15, + "40": 10, + "50": 8, + "80": 29 + }, + "unit_count_upper": 211, + "units": 119 + }, + "literal_classes": 121, + "paid": { + "1": 2, + "4": 1 + }, + "rule": "strict-overlap", + "targets": { + "2": 1, + "5": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 322, + "exits": { + "1": 216, + "2": 216, + "4": 72, + "8": 8 + }, + "height": 2, + "matched_jobs": 512, + "minimum_source": 8, + "n": 20, + "rank_one_surplus": 1, + "source_count": 128, + "sources": { + "12": 48, + "18": 10, + "8": 64, + "9": 6 + }, + "unit_count_upper": 129, + "units": 128 + }, + "literal_classes": 73, + "paid": { + "1": 6, + "2": 2 + }, + "rule": "source-open-equality", + "targets": { + "2": 4, + "3": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 4362, + "exits": { + "1": 1296, + "16": 16, + "2": 1728, + "4": 864, + "8": 192 + }, + "height": 3, + "matched_jobs": 5040, + "minimum_source": 16, + "n": 40, + "rank_one_surplus": 1, + "source_count": 670, + "sources": { + "16": 256, + "18": 84, + "24": 256, + "27": 6, + "36": 68 + }, + "unit_count_upper": 1157, + "units": 1142 + }, + "literal_classes": 585, + "paid": { + "1": 6, + "2": 2 + }, + "rule": "source-open-equality", + "targets": { + "2": 4, + "3": 1 + } + }, + { + "flow": { + "all_sources_above_n_over_m": true, + "boundary_exits": {}, + "column_mass": 55372, + "exits": { + "1": 7776, + "16": 480, + "2": 12960, + "32": 32, + "4": 8640, + "8": 2880 + }, + "height": 4, + "matched_jobs": 45088, + "minimum_source": 27, + "n": 80, + "rank_one_surplus": 1, + "source_count": 3572, + "sources": { + "27": 36, + "32": 1024, + "36": 744, + "48": 1280, + "54": 96, + "72": 392 + }, + "unit_count_upper": 9881, + "units": 9732 + }, + "literal_classes": 4681, + "paid": { + "1": 6, + "2": 2 + }, + "rule": "source-open-equality", + "targets": { + "2": 4, + "3": 1 + } + } + ], + "new_code_sha256": { + "flow.py": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a", + "verify.py": "9ae067eadf17ff9d97737805eb642a69375a5ff2ddb08988fef59aa0771f9b7c" + }, + "rejected_mutations": [ + "whole integer subprogram batches", + "finite direct-flow rank contract" + ], + "schema": "partial-direct-mixed-flow-and-finite-size/1", + "scope": "New finite matching/scheduling and batching/size bounds. The direct near-root exponent is open. Existing conditional endpoint and native/physical hypotheses remain inherited; no new kappa.", + "source_sha256": { + "research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8", + "research/direct-mixed-flow/vendor/P7-FACTOR.json": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598", + "research/direct-mixed-flow/vendor/SUSSMAN-LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "research/direct-mixed-flow/vendor/SUSSMAN-NOTICE": "8289a4ba75efe5da7bd2e389b951155ff74b3bf49b38ace0906a1e5205c7cd6e", + "research/direct-mixed-flow/vendor/THREE-base-FULL-IDENTITY-NATIVE.json.gz": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39", + "research/direct-mixed-flow/vendor/higher-moment-README.md": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d", + "research/direct-mixed-flow/vendor/higher-moment-RESULT.json": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156", + "research/direct-mixed-flow/vendor/p7-NATIVE.md": "26bf9312cdb496b1113c9ddd8aa0fa922ed9e480005703212942af358394183d", + "research/direct-mixed-flow/vendor/p7-RESULT.json": "9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab", + "research/direct-mixed-flow/vendor/theorem-1g.md": "c4a96c55c2509ff36e8bc6bddaaf6a8b1a34a5d794e4e09ac5214c82b51510e6", + "research/direct-mixed-flow/vendor/tree_flow.py": "750782f6d1cc0a9fff8a768899f3f4c62a7efdf0696d8b5a5d640b1836f5ab72" + }, + "status": "PASS_PARTIAL_DIRECT_FLOW_AND_SIZE_BOUNDS" +} diff --git a/research/direct-mixed-flow/SOURCES.json b/research/direct-mixed-flow/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/direct-mixed-flow/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/direct-mixed-flow/TASK.json b/research/direct-mixed-flow/TASK.json new file mode 100644 index 0000000000..e232fd2674 --- /dev/null +++ b/research/direct-mixed-flow/TASK.json @@ -0,0 +1,148 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Can the #4088 four-provider dispatch satisfy the complete ordinary/outer admission contract?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/scatter-boundary-decision/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4088 Scope and Open next questions: local words, native receipts and literal fill do not include a rerun of the mixed four-provider ordinary/outer engine. #3801 is the newer scatter-boundary decision; do not restart #2977 as if untouched.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Pin the provider registry, four native source closures and dispatch. Make a bounded acceptance coverage map or one registry adapter preserving every inherited admission predicate and rejection control (including an omitted fourth provider). Record remaining ordinary/outer obligations and a resource estimate before heavy execution. Stop at unresolved source/caller dependencies; no selected-result promotion from a local pass.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "One provider-registry, dispatch, native-closure or admission-predicate obligation; separate branches must name distinct coverage." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug.", + "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary.", + "Running another root enclosure instead of validating dispatch or weakening an inherited predicate to make mixed admission pass." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting", + "2977", + "scatter export", + "duplicate index", + "parity semantics", + "4088", + "3801", + "staged544-mixed-fourth-entry", + "scatter-boundary-decision" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Target a direct chronological integer compiler for overlapping paid/productive ranks, without tensor power or paid padding, and explicit width/word/owned-storage bounds.", + "scope_change_reason": "User requests the next contribution target twice the significance of the higher-moment strictification. Raise the target from quantitative bounds inside that mechanism to removing its separation layer and controlling the full finite word. This is an ambitious target, not a claimed numerical significance measurement.", + "bottleneck_link": "Raw p7 has paid rank 48 above productive minimum 5. Existing compiler proofs require strict separation and the winning words lack explicit productive-width bounds. Partial matching may retain all unmatched jobs as priced exits; nested widths may avoid repeated products of batching denominators.", + "budget_minutes": 60, + "stop_rule": "First prove exact whole-integer matching, chronological return, top sources and smaller exits. Then test whether the complete recurrence supports the desired exponent. Do not infer exponent admission from moment balance. If it fails, preserve the first counterexample or missing lemma and the explicit-size result; no broader census or new kappa claim.", + "outcome": "partial", + "evidence": "README.md proves the finite partial-matching compiler, nested exp(O(N log N)) widths, raw/owned/routing bounds and closed encoded precision envelopes for the existing PR4433 supplier. RESULT.json checks source record counts and all integer inequalities, nine literal/merged flows, two overlap compilations through rank 100, and 880 p7 nonbase compilations through rank 1000. Direct near-root exponent remains open.", + "author": "zxv, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; no subagents.", + "open_questions": [ + { + "question": "Does the capped, partially matched direct flow close the target-saving induction?", + "why_it_matters": "A finite acyclic flow is insufficient if its boundary exits consume all complement capacity.", + "first_step": "Reconstruct every unmatched whole job and evaluate the complete complement-plus-exit recurrence on the source first examples and p7.", + "blocked_by": "No uniform boundary-exit bound or direct exponent proof yet." + }, + { + "question": "Do the complete encoded resource and precision envelopes survive independent native/physical admission?", + "why_it_matters": "The closed numerical envelopes depend on the source finite-record semantics and do not independently establish their physical tariffs or recovery threshold.", + "first_step": "Audit the raw/whole-job record allowance against the caller, then separately bind physical adapters, movement and recovery exclusions.", + "blocked_by": "Inherited native/physical/analytic premises remain outside this mathematical count proof." + } + ], + "publication_policy": "User explicitly authorized posting this PR on October 21, 2026. Subsequent research remains local for user review before submission; no Discussion posting is authorized by this checkpoint.", + "significance_target": { + "relative_to": "PR4433 higher-moment strictification", + "requested_multiplier": 2, + "meaning": "Structural removal of tensor/padding plus full finite-program size control; aspirational scope, not a numerical guarantee." + }, + "upstream_checkpoint": { + "commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "priority_revision": 7, + "checked_at_utc": "2026-10-21T18:47:25Z" + }, + "scope_decision": "Continue toward the direct exponent gate; retain a separate complete count/batching theorem that already applies to PR4433. No further scan expansion without a new boundary estimate.", + "overlap": { + "checked_at_utc": "2026-10-21T18:48:25Z", + "open_prs": 538, + "discussion_records": 3280, + "complete_pagination": true, + "terms": [ + "direct mixed compiler", + "overlapping ranks", + "Pascal matching", + "nested widths", + "batch denominators", + "unmatched jobs" + ], + "specific_matches": "No matching public scope found; the later search matches this local task itself. This is not proof of novelty.", + "limits": "Open bodies, discussions and local notes; no arbitrary remote code-diff or remote closed-body search." + }, + "scope_deliverables": { + "finite_direct_compiler": "proved under inherited native/adapter hypotheses; max paid < ambient, no near-root saving yet", + "full_finite_size_bounds": "proved in declared encoded native-record grammar; explicit bounds for the existing PR4433 supplier", + "direct_near_root_exponent": "open; requires a uniform boundary-exit/complement estimate", + "scientific_significance_target": "in progress; not claimed achieved" + }, + "validation": { + "python": "3.12.8", + "platform": "macOS arm64", + "registered_replay": "pass", + "metadata_and_pins": "pass", + "committed_bytes": "pass", + "git_free_optimized": "pass", + "changed_native_source": "rejected", + "changed_receipt": "rejected", + "unrun": [ + "full source history (shallow checkout)", + "independent mathematical review", + "native all-column/physical/analytic/recovery admission", + "Lean", + "Docker", + "historical suites" + ] + } +} diff --git a/research/direct-mixed-flow/VENDOR.json b/research/direct-mixed-flow/VENDOR.json new file mode 100644 index 0000000000..d95b1124e8 --- /dev/null +++ b/research/direct-mixed-flow/VENDOR.json @@ -0,0 +1,82 @@ +{ + "schema": "byte-identical-source-exports/1", + "files": [ + { + "commit": "da637c87c89482bc4c86be36bd0071b3d400dbed", + "original_path": "research/kappa-rebuild/architecture/sources/Sussman-563b4e6/research/record-track/proofs/theorem-1g.md", + "path": "research/direct-mixed-flow/vendor/theorem-1g.md", + "git_blob": "36d2399f3538c34e4b1567a15b4a5dfe77ffc7ad", + "sha256": "c4a96c55c2509ff36e8bc6bddaaf6a8b1a34a5d794e4e09ac5214c82b51510e6" + }, + { + "commit": "da637c87c89482bc4c86be36bd0071b3d400dbed", + "original_path": "research/kappa-rebuild/architecture/sources/Sussman-563b4e6/research/record-track/programs/theorem-1g/tree_flow.py", + "path": "research/direct-mixed-flow/vendor/tree_flow.py", + "git_blob": "31a9c1ae4d116b12e8db7d8e06f723f10425068d", + "sha256": "750782f6d1cc0a9fff8a768899f3f4c62a7efdf0696d8b5a5d640b1836f5ab72" + }, + { + "commit": "da637c87c89482bc4c86be36bd0071b3d400dbed", + "original_path": "research/kappa-rebuild/architecture/sources/Sussman-563b4e6/LICENSE", + "path": "research/direct-mixed-flow/vendor/SUSSMAN-LICENSE", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "commit": "da637c87c89482bc4c86be36bd0071b3d400dbed", + "original_path": "research/kappa-rebuild/architecture/sources/Sussman-563b4e6/NOTICE", + "path": "research/direct-mixed-flow/vendor/SUSSMAN-NOTICE", + "git_blob": "0b06967886fab2628afc0b881c884161bbf5e430", + "sha256": "8289a4ba75efe5da7bd2e389b951155ff74b3bf49b38ace0906a1e5205c7cd6e" + }, + { + "commit": "da637c87c89482bc4c86be36bd0071b3d400dbed", + "original_path": "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md", + "path": "research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md", + "git_blob": "4badb40f0919c515823cb07e44c6470d4d6469ca", + "sha256": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8" + }, + { + "commit": "b84060c9c", + "original_path": "research/higher-moment-strictification/README.md", + "path": "research/direct-mixed-flow/vendor/higher-moment-README.md", + "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3", + "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d" + }, + { + "commit": "b84060c9c", + "original_path": "research/higher-moment-strictification/RESULT.json", + "path": "research/direct-mixed-flow/vendor/higher-moment-RESULT.json", + "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a", + "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156" + }, + { + "commit": "e9058860b5c850760fdf970e796a96aefcdb1d98", + "original_path": "research/pr4359-p7-padding/RESULT.json", + "path": "research/direct-mixed-flow/vendor/p7-RESULT.json", + "git_blob": "ebb30a9b3b94fb159a316350f7da57bde4a30c25", + "sha256": "9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab" + }, + { + "commit": "da637c87c89482bc4c86be36bd0071b3d400dbed", + "original_path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "path": "research/direct-mixed-flow/vendor/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39" + }, + { + "commit": "e9058860b5c850760fdf970e796a96aefcdb1d98", + "original_path": "research/pr4359-p7-padding/P7-FACTOR.json", + "path": "research/direct-mixed-flow/vendor/P7-FACTOR.json", + "git_blob": "04c7ef620e760cc8f1764bbf0ccd7f32c6a5bd86", + "sha256": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598" + }, + { + "commit": "e9058860b5c850760fdf970e796a96aefcdb1d98", + "original_path": "research/pr4359-p7-padding/NATIVE.md", + "path": "research/direct-mixed-flow/vendor/p7-NATIVE.md", + "git_blob": "394d9a03c165336d1cfbcd41921c93741042393b", + "sha256": "26bf9312cdb496b1113c9ddd8aa0fa922ed9e480005703212942af358394183d" + } + ] +} diff --git a/research/direct-mixed-flow/VERIFY.json b/research/direct-mixed-flow/VERIFY.json new file mode 100644 index 0000000000..de075b7c20 --- /dev/null +++ b/research/direct-mixed-flow/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/direct-mixed-flow/vendor/theorem-1g.md", + "research/direct-mixed-flow/vendor/tree_flow.py", + "research/direct-mixed-flow/vendor/SUSSMAN-LICENSE", + "research/direct-mixed-flow/vendor/SUSSMAN-NOTICE", + "research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md", + "research/direct-mixed-flow/vendor/higher-moment-README.md", + "research/direct-mixed-flow/vendor/higher-moment-RESULT.json", + "research/direct-mixed-flow/vendor/p7-RESULT.json", + "research/direct-mixed-flow/vendor/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/direct-mixed-flow/vendor/P7-FACTOR.json", + "research/direct-mixed-flow/vendor/p7-NATIVE.md", + "research/direct-mixed-flow/VENDOR.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact partially matched flows, nested widths and global resource counts; source-bound finite-word/precision envelopes; rank-1000 direct-target rejection. No direct exponent theorem." + } + ] +} diff --git a/research/direct-mixed-flow/flow.py b/research/direct-mixed-flow/flow.py new file mode 100644 index 0000000000..07175cd6e1 --- /dev/null +++ b/research/direct-mixed-flow/flow.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +"""Capped whole-integer lockstep flow, retaining unmatched jobs as paid exits. + +Generalizes Jacob Alan Sussman's separated multinomial construction. +zxv with substantial OpenAI Codex assistance. Apache-2.0. +This is a finite flow, not a theorem that it attains the mixed-root saving. +""" +from collections import Counter +from functools import lru_cache +from math import comb, prod + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +class Flow: + def __init__(self, targets, paid, n, extra_height=0, height_base=None): + self.T, self.P, self.n = dict(targets), dict(paid), n + self.K = tuple(sorted(targets)) + self.m, self.kmin, self.rmax = max(targets), min(targets), max(paid) + need(2 <= self.kmin <= self.m and self.rmax < self.m <= n, + 'finite direct-flow rank contract') + need(all(isinstance(v, int) and v > 0 for x in (targets, paid) + for v in x.values()), 'positive integer inventories') + self.cap = n//self.m + self.height_base = self.kmin if height_base is None else height_base + need(isinstance(self.height_base, int) and self.height_base >= 2, 'integer height base') + self.G, least = 0, 1 + while least*self.height_base <= self.cap: + self.G += 1 + least *= self.height_base + need(isinstance(extra_height, int) and extra_height >= 0, 'nonnegative extra height') + self.G += extra_height + self.zero = (0,)*len(self.K) + + @lru_cache(None) + def column(self, a): + return prod(k**v for k, v in zip(self.K, a)) + + @lru_cache(None) + def points(self, height, cap): + """(a, u(a)) at fixed degree; exact multinomial integer weights.""" + result = {} + + def visit(i, remaining, c, weight, a): + if i == len(self.K): + if remaining == 0 and c <= cap: + result[a] = weight + return + k, w = self.K[i], self.T[self.K[i]] + for count in range(remaining+1): + new_c = c*k**count + if new_c > cap: + break + visit(i+1, remaining-count, new_c, + weight*comb(remaining, count)*w**count, a+(count,)) + + if cap >= 1: + visit(0, height, 1, 1, ()) + return result + + @lru_cache(None) + def units(self, depth, rho): + return self.points(self.G-depth, self.cap//rho) + + @lru_cache(None) + def demand(self, depth, rho): + result = Counter() + for a, count in self.units(depth, rho).items(): + for i, k in enumerate(self.K): + b = list(a) + b[i] += 1 + result[tuple(b)] += count*self.T[k] + return result + + def merged(self): + sources, exits, boundary = Counter(), Counter(), Counter() + units = columns = 0 + matched = 0 + path_counts = Counter({1:1}) + for b, count in self.demand(0, 1).items(): + sources[self.column(b)] += count + for depth in range(self.G+1): + following = Counter() + for rho, paths in path_counts.items(): + batch = self.units(depth, rho) + units += paths*sum(batch.values()) + columns += paths*sum(count*rho*self.column(a) for a, count in batch.items()) + for rank, repetitions in self.P.items(): + new_rho = rho*rank + copies = paths*repetitions + if depth == self.G: + need(set(batch) <= {self.zero}, 'leaf degree zero') + exits[new_rho] += copies*batch.get(self.zero, 0) + continue + child = self.demand(depth+1, new_rho) + if new_rho <= self.cap: + following[new_rho] += copies + for b in set(batch) | set(child): + supply, demand = batch.get(b, 0), child.get(b, 0) + e = new_rho*self.column(b) + consumed = min(supply, demand) + matched += copies*consumed + if supply > demand: + exits[e] += copies*(supply-demand) + boundary[e] += copies*(supply-demand) + elif demand > supply: + need(supply == 0, 'Pascal demand cannot exceed present supply') + sources[e] += copies*(demand-supply) + path_counts = following + sources, exits, boundary = +sources, +exits, +boundary + need(sources and all(1 <= s <= self.n for s in sources), + 'all sources are positive and fit parent') + if self.height_base <= self.kmin: + need(all(self.n < self.m*s for s in sources), 'default top source bound') + need(all(1 <= e < self.n and self.m*e <= self.rmax*self.n for e in exits), + 'all paid exits strictly smaller than parent') + need(all(self.m*e > self.kmin*self.n for e in boundary), + 'premature exits have a failed boundary term') + mass = lambda h: sum(k*v for k, v in h.items()) + surplus = mass(self.T)-mass(self.P) + need(mass(sources)-mass(exits) == surplus*columns, + 'exact rank-one telescoping identity') + W, P = sum(self.T.values()), sum(self.P.values()) + bound = sum(P**d*W**(self.G-d) for d in range(self.G+1)) + need(units <= bound and sum(sources.values()) <= W*units, + 'full integer unit/source count bounds') + return {'n': self.n, 'height': self.G, 'sources': sources, 'exits': exits, + 'boundary_exits': boundary, 'units': units, 'column_mass': columns, + 'source_count': sum(sources.values()), 'matched_jobs': matched, + 'minimum_source': min(sources), 'all_sources_above_n_over_m': + all(self.n < self.m*s for s in sources), + 'rank_one_surplus': surplus, 'unit_count_upper': bound} + + def literal(self, paid_word, class_limit=200000): + """Every round returns before the next; no merging of round paths.""" + need(Counter(paid_word) == Counter(self.P), 'literal paid word matches invoice') + sources, exits = Counter(), Counter() + classes = 0 + + def process(depth, rho, incoming): + nonlocal classes + classes += 1 + need(classes <= class_limit, 'literal replay class limit') + wanted = self.demand(depth, rho) + need(all(v <= wanted.get(b, 0) for b, v in incoming.items()), + 'all incoming whole jobs fit child slots') + for b, count in wanted.items(): + missing = count-incoming.get(b, 0) + if missing: + sources[rho*self.column(b)] += missing + batch = self.units(depth, rho) + for rank in paid_word: + new_rho = rho*rank + if depth == self.G: + for a, count in batch.items(): + exits[new_rho*self.column(a)] += count + continue + child = self.demand(depth+1, new_rho) + passed = Counter() + for b, count in batch.items(): + consumed = min(count, child.get(b, 0)) + if consumed: + passed[b] = consumed + if count > consumed: + exits[new_rho*self.column(b)] += count-consumed + # All unconsumed exits and this entire child return at this + # paid position, before any later parent round is issued. + process(depth+1, new_rho, passed) + + process(0, 1, Counter()) + return {'sources': +sources, 'exits': +exits, 'classes': classes} + + +def approximate_leaves(targets, paid, maximum, checkpoints, extra_height=0, height_base=None): + """Exploratory floating point recurrence; never an acceptance certificate.""" + m = max(targets) + leaves = list(map(float, range(maximum+1))) + saved = {} + previous_cap = None + for n in range(m, maximum+1): + cap = n//m + if cap != previous_cap: + recipe = Flow(targets, paid, n, extra_height, height_base).merged() + source, exit = recipe['sources'], recipe['exits'] + count = recipe['source_count'] + exit_charge = sum(v*leaves[e] for e, v in exit.items()) + previous_cap = cap + leaves[n] = (sum(v*leaves[n-s] for s, v in source.items())+exit_charge)/count + if n in checkpoints: + from math import log + saved[n] = {'leaves_approx': leaves[n], + 'effective_saving_approx': 1-log(leaves[n])/log(n), + 'source_types': len(source), 'exit_types': len(exit), + 'boundary_exit_types': len(recipe['boundary_exits'])} + return saved diff --git a/research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md b/research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md new file mode 100644 index 0000000000..4badb40f09 --- /dev/null +++ b/research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md @@ -0,0 +1,313 @@ +# Finite precompilation of a mixed-target rule + +Status: constructive bridge under the precise native hypotheses below, +independently audited in `../transfer-audit/AUDIT.md`. This is a written +argument, not a formal proof or a completed integer-multiplication admission. +The companion finite scheduler checks actual integer flow and ordering. +The original immediate-normalization BIT interface failed hypothesis 3. +`../bit/DELAYED-COVER-BRIDGE.md` supplies the distinct delayed-cover +implementation, with a finite local-ring check and the native binding in +`../bit/BIT-P3-NATIVE-BINDING.json`. Its fixed rational cover routes are a +costed program schema, not dense coordinate gates in a plain native word. + +Substantial OpenAI assistance. Apache-2.0. The mixed-target asymptotic flow is +Jacob Alan Sussman's Theorem 1G, PR4268, with the detailed proof at commit +`563b4e6e913625637f36ba7869bf5fcd0dd4975a` of +[`wht-power-saving-lean`](https://github.com/jacobalansussman/wht-power-saving-lean). +The source, exact scheduling code and notices are preserved under `sources/`. +The contribution proposed here is clearing the finite flow into a single +uniform native supplier before applying the inherited outer theorem. + +## 1. What needs to be assumed + +Let a job of rank `s` apply a specified tensor operator to `s` selected +coordinate blocks of one array, fixing all other coordinates. A block has +an arbitrary positive tensor multiplicity `f`. A completed rank `s` job +therefore acts on `s*f` axes. All productive inputs are arbitrary. + +Fix one mixed unit with productive targets `W_k` of ranks `k`, a chronological +list of paid child ranks `r_j`, and a finite number of scalar and routing +passes. These assumptions are required, separately from the moment inequality: + +1. **An all-column native word.** At every integer column count `c`, the unit + computes exactly its independent rank `k*c` output jobs. Its paid rounds + are rank `r_j*c` jobs in the stated order. All borrowed data return to the + declared endpoint, and owned storage is explicitly initialized and erased. + Its finite operation count is uniform in `c`. +2. **Disjoint splitting and spectators.** A rank `a+b` job is a rank `a` job + followed by a rank `b` job on disjoint coordinates. The resulting programs + preserve arbitrary complete spectator fields and accept arbitrary data. +3. **Whole-job adapters.** Any job passed between two units has an explicitly + priced, permitted embedding into its destination. For the intended complex + application these are fixed monomial binary address maps and unit quadratic + phases, together with role permutations. The adapters must work at every + tensor multiplicity. Rank equality by itself is insufficient. +4. **Finite-program closure.** A finite composition of these words and + adapters is again a permitted finite supplier. Constantly many owned fields + may be supplied with their full cost and no productive output credit. + The eventual ordinary recursion must have the same arbitrary-input, + restoration, scalar and precision interface as the retained supplier. + +Put `m=max{k:W_k>0}`, `k_min=min{k:W_k>0}`, and +`r_max=max{r_j}`. Require `r_max g*S`, keeps one +external weight throughout the entire finite circuit, and lowers only its +final rank-one leaves. All rational matchers, role routes and their inverses +are fixed before choosing the odd prime and its exclusions. Every route +uses complete equal-multiplicity cover fibers and the retained, costed row +permutation primitive. This gives the same finite DAG argument in the +rational-cover program category. The BIT binding supplies the actual native +projectors; a rank count alone would not provide this implementation. + +## 2. Proposed conclusion + +Suppose the preceding hypotheses hold and the mixed balance has root +`tau` in `(0,1)`: + +``` +sum_j r_j^tau = sum_k W_k k^tau. +``` + +For every `z` with `tau=2`, a fixed number `B_N` of productive arrays, +and only rank-one paid children, whose number `P_N` satisfies + +``` +P_N < B_N * N^z. +``` + +Every productive output is the full rank-`N` job. The construction may have +an enormous finite scalar word, role inventory and owned-storage requirement. +Those quantities affect constants and the eventual input threshold. They are +not omitted and are not credited as extra output jobs. + +If this uniform supplier is admitted under the retained native, precision and +fixed-tape premises, the existing uniform recursion applies directly. A new +dynamic RAM-to-Turing-machine simulation is not being assumed here. + +## 3. The integer lockstep flow at a fixed rank + +This is the part of Theorem 1G used by the compiler. At one fixed top rank +`N`, its units, source jobs and exit jobs have integer multiplicities. +For a multi-index `a` on the target types define + +``` +c(a) = product_k k^(a_k), +u(a) = multinomial(|a|;a) * product_k W_k^(a_k). +``` + +The exact Pascal identity is + +``` +u(b) = sum_{k:b_k>0} W_k*u(b-e_k). +``` + +Let `G` be the largest `|a|` with `m*c(a)<=N`. A class is indexed by a +sequence of paid rounds `s` of length `d<=G`; its dilation is +`rho_s=product r_j`. It contains `u(a)` units at column `rho_s*c(a)` for +each `a` with `|a|=G-d` and `m*rho_s*c(a)<=N`. + +For one parent paid round, the Pascal bijection matches its job copies to +target roles of the child class, at exactly equal integer ranks. Missing +demands are top sources. Separation ensures every parent job is consumed. +The source ranks lie in `(N/m,N]`; only the deepest classes produce exit +jobs, all strictly smaller than `N` once `N` is outside the finite base range. + +Process a class in word order. At round `j`, suspend every unit of that +class, complete the entire child class fed by that round, and only then +advance the parents to round `j+1`. This forbids a unit from requiring both +an earlier and a later round of the same suspended parent. The resulting +dependency graph is finite and acyclic. Its edges carry complete array jobs, +not individual scalar values copied for free. + +These integer quantities exist before normalizing the sources to total +weight one. Let `S_s` be the number of source jobs of rank `s`, let +`S=sum_s S_s`, and let the ordered exit batches be `(e,t)` with `t` jobs +of rank `e` each. This finite integer flow is the compiler input. + +## 4. Clear every batch denominator constructively + +Induct on the integer top rank `N`. For each smaller rank `e` the compiler +has already constructed a uniform program on `B_e` arbitrary arrays, +computing full rank `e` with `P_e` paid rank-one calls. For a sufficiently +small rank use the ordinary sequential program: `B_e=1`, `P_e=e`. + +For the current flow choose an integer `a` divisible by every `B_e` needed +for an exit and every `B_(N-s)` needed for a nonzero source remainder. +The product of those finitely many positive integers is a valid choice; +their least common multiple is a smaller optional choice. Set + +``` +B_N = a*S. +``` + +Assign `a*S_s` of the input arrays to each source rank `s`. On each of those +arrays, first complete its `N-s` complementary coordinates using the +already-compiled smaller uniform program. All such batches are integral +because `a` is divisible by their program widths. This preliminary action +commutes with the intended `s`-coordinate job and fixes its input coordinates. + +Make `a` copies of the integer lockstep flow. Route its source arrays to +their exact input slots using permitted whole-array adapters. At a deepest +exit batch, `a*t` is divisible by `B_e`; replace that batch by copies of +the smaller uniform rank-`e` program. Restore its role ordering and adapters +before resuming the suspended parent class. Execute the finite DAG in the +lockstep order, and finally restore the original source-array ordering. + +Every array has now received its disjoint complementary job and source job, +hence the full rank-`N` transform. No copied scalar input or blank helper is +treated as another independent output. Every original array occurs exactly +once as a source; interior target slots are jobs on those arrays, not new +productive inputs. + +Induction removes all recursive calls: the only remaining paid children +have rank one. Clearing denominators multiplies productive arrays and paid +operations equally, so it preserves the per-array leaf count. In formulas, + +``` +P_N/B_N = (1/S) * [ + sum_s S_s * (P_(N-s)/B_(N-s)) + + sum_(ordered exit batches e,t) t * (P_e/B_e) +]. +``` + +Zero-rank terms vanish. Any plain rank-one exits are the ordinary base +program. Scalar and routing passes have their own analogous nonnegative +count and must be included in the asymptotic cost used to choose `N`. + +This construction uses full integer batches; it does not assume that +fractional pieces of a physical array can be routed at zero cost. Its exact +replication factors can be impractically large, which is acceptable for a +fixed finite supplier existence statement but must be disclosed. + +## 5. Why some fixed N has the required saving + +The independent audit sharpened this step to a direct count of paid leaves. +It does not require a running-time comparison between a RAM flow and native +tapes. Let `L(n)=P_n/B_n`, let `w_s=S_s/S`, and let `x_e` be the exit counts +normalized by the number S of source arrays. The actual integer compiler +satisfies + +``` +L(n) = sum_s w_s L(n-s) + sum_e x_e L(e), +sum_s w_s = 1, +sum_e x_e e^tau = sum_s w_s s^tau. +``` + +The last equality follows by canceling every internal matched job in the +exact tau-potential balance. The source ranks satisfy `n/m0`, concavity gives + +``` +n^z0 - sum_s w_s (n-s)^z0 >= eta * sum_s w_s s^z0. +``` + +Indeed, for `t=s/n` in `[1/m,1]`, +`1-(1-t)^z0 >= z0*t >= eta*t^z0`. For every sufficiently large n the +exit coefficient is less than `eta/2`. Every complement and exit has +smaller rank than n, so strong induction on the exact recurrence proves +`L(n)<=A*n^z0`, with finite A chosen to cover the smaller ranks. Eventually +`L(N).lean, byte-identical to + third-party/openai-math/). + + b. Modified copies of OpenAI's proof files. In each package, the folder + Work/Fourier/ (for example Work/FourierC588MHH/) holds copies + of eleven files of lean/OAI/Computability/FourierTransform/ of + openai/math and of five definitions of its Goal.lean, made the way + section 7 describes, by Shea's script mkchain_c401g5.py or by the + agents' generators that copy its output under a new suffix (for + example community/c588mhh/generators/lean-gen/mk_fourier_h.py). Each + begins with a + comment that names the upstream file and states what was changed. In + c588-repack these are Shea's own copies with the exponent changed. + + c. Files that contain upstream text. The files Challenge.lean under + community/wht-c588/overlay/Work/ and community/wht-c588mhh/overlay/ + Work/ contain the RAM cost model of + lean/ComparatorChallenges/UniformFourier.lean of openai/math, + unchanged, as Work/GCert/Data/ChallengeB2Ge8x.lean does (section 2); + their headers say what differs from that file. + + d. Files adapted from Shea's repository in community/c588mhh/overlay/ + Work/XHost/: + - HDef.lean is a copy of lean/complex588/Work/Bridge401/GNetDef.lean, + HStage.lean of Work/Bridge401/GNetStage.lean, HCert.lean of + Work/Bridge401/GNetCert.lean, HGeom.lean of the instance part of + Work/Bridge401/GGeom.lean, and HEnd.lean is adapted from + Work/Bridge401/End.lean, each with same-run hosting added (the idea + of DaysSky's pull request #442 to CrocSwap/integer-mult-bounds) and + the names changed. In Shea's tree these files are those of Nil + Mamano's submission named above (his SOURCE_MANIFEST.json records + each as taken from submissions/dft/nmamano-dft-record/ at the + verifier commit above), written by his generator gen401.py on the + layouts credited above, with the engine of this repository. + - Frames.lean adapts lemmas of Work/Bank401/Adapt.lean and + Work/Bank401/Frames.lean of the same tree, which come from the same + submission: host_adapt is bank_adapt, host_pad is bank_pad and + slot_frames is bank_frames, each with the new coordinates chosen + inside the pending set of an idle climb. + - HSchedK.lean copies the lemmas about lists of + Work/Bridge401/SchedK.lean of the same tree, and its checker + hostSchedK is modelled on the checker schedK there; HostK.lean is + modelled on the same checker. + The header of each file names its source and says what was changed. + One header is wrong in part: that of HEnd.lean says that Shea's + End.lean was written after a file Work/Bridge377/End.lean of Jacob + Sussman's. No such file of his exists; Shea's End.lean says only that + it follows a file of that name. The header is left as it was compiled + (community/c588mhh/README.txt says so). + The generators that wrote them are under + community/c588mhh/generators/lean-gen/. The same twelve network files + of Work/XHost/, byte-identical, are also in community/u8xmhh/overlay/ + Work/XHost/. + The log community/c588mhh/supporting/L2/skeptic/logs/ + Work_Bank401_Adapt.log is of his file, compiled unchanged; the file + itself is not included. + + e. Programs from Shea's repository. + - Byte-for-byte copies of his files at the commit above, unchanged and + without a notice inside them (the same files are also in + third-party/shea256-fourier-transform-below-nlogn/ at their own + paths): + research/complex-transfer-588-596/experiments/generate_global_lean.py + is copied as tools/community/route/generate_global_lean.py and + tools/community/repack/tools/generate_global_lean.py; + research/complex-transfer-588-596/experiments/bank_reprice.py is + copied as tools/community/repack/tools/shea_bank_reprice.py; + research/complex-transfer-588-596/verification/exact_moment.py is + copied as tools/community/route/exact_moment.py, + tools/community/repack/tools/exact_moment.py, + community/c588mhh/generators/design-tools/exact_moment.py and + community/u8xmhh/generators/design-tools/exact_moment.py. + - route_price.py, in four identical copies (tools/community/route/, + tools/community/repack/tools/, + community/c588mhh/generators/design-tools/ and + community/u8xmhh/generators/design-tools/), contains functions + copied from his bank_reprice.py and generate_global_lean.py (its + header says so), changed to price a local word through his route. + - The generators of tools/community/c588m-gen/ drive or adapt his + scripts in third-party/shea256-fourier-transform-below-nlogn/ + research/; each adapted file says what it changes. + - community/c588-repack/overlay/comparator/fourier.json is his + comparator configuration, unchanged. + + f. Data. The certificate of Kothe's #588 circuit, its bank schedule and + its price, as published in Shea's repository, are in + third-party/shea256-fourier-transform-below-nlogn/lean/complex588/ + artifacts/, unchanged. The packages' certificate and data modules + are derived from them (VERIFY.md, section 11, says how). + + g. Data derived from CrocSwap/integer-mult-bounds at a later state (the + U8 circuit). The certificates of community/u8x and community/u8xm (the + files under their Work/GCert/Data/ whose paths contain U8X), + and the host table and data modules of community/u8xmhh, which are + computed from the certificate of u8xm, are derived from the U8 word of + the repository CrocSwap/integer-mult-bounds + (https://github.com/CrocSwap/integer-mult-bounds), a circuit of that + community: Jeremy Kothe's pull request #869, on his #799 (which + carries Chafik Boukhalfa's frame changes of #741), on icekylinx's + gauge44 construction (#645) and on the earlier work that their + notices name. Only the word's additions and their frames are used: + not the owner maps of #870 (Kothe, with Hao Yan's #858), #890 + (Boukhalfa) and #942 (Jonathan Capalbo), nor DreamingOfClouds' bit + supplier #589. The agents rebuilt the word with that repository's + own program + research/complex-t21-owners/vendor/pr870/construction/barch/ + reproduce_barch.py (recipe U8; #869's builder, in the copy of #870's + package that #890 keeps), in a clone at commit + 407d52ff15b2217b6e22bce44728b4c3907b6515 of its main branch + (13 October 2026). The word they obtained has the canonical sha256 + 24db880b7dab31e6af4eec8a1aba1bbbae29cd50d9a7b77cf0e9b571b3e5ae7c, the + value pinned for it in that repository (the file + LOCAL-PINS-barch-U8.json next to the program). The logs of that run are in + community/base-logs/u8-word/. No program of that repository is + included here, and the word itself is not included: the packages hold + certificates computed from it. + That repository is published under the Apache License, Version 2.0 + (its LICENSE at that commit is the same text as the file LICENSE). + Its NOTICE file at that commit differs from the copy of section 6 (the + state of pull request #193) in one passage, which + third-party/CrocSwap-integer-mult-bounds/at-407d52ff/SOURCE.txt + describes. Complete copies of that NOTICE file and of the notice files + of the folders the program comes from + (research/complex-t21-owners/NOTICE.md and, under its vendor/pr870/, + NOTICE.md, UPSTREAM-NOTICE.md and t16/NOTICE.md), unchanged and at + their paths, are in + third-party/CrocSwap-integer-mult-bounds/at-407d52ff/; they apply to + these data. + + The new files of community/ were made on 2026-10-13 the way section 4 + describes. The credits, with links, are in README.md. + +10. Files added in the fifth revision outside community/ (package/, + scripts/, tools/lever/, tools/lever-hub/, tools/reproduce-search.sh, + tools/compare_results.py, data/, results/, research/, + notes/how-the-lever-was-found.md, notes/open-directions-4.md and the + additions to third-party/). + The packages under package/ (the sixth result, package/u8x0hq, and the + recursion lever, package/leverF, package/leverB, package/leverA, package/lever2979, package/lever) are laid over the same + clone of Ryan Shea's repository as the packages of section 9 (commit + 52394849c7ecf3412d39b925d75fc7fdb98994d8, folder lean/complex588, + Apache License, Version 2.0). His licence and notice files in + third-party/shea256-fourier-transform-below-nlogn/ apply to the material + of his repository that files of these packages copy or adapt; each such + file says so in its first lines, and the packages' README.txt list them. + Shea's tree carries Lean files of Nil Mamano's published Big O Speedrun + submission (bigospeedrun/verifier, Apache License, Version 2.0): the + gauged interface, the nine-stage network, its bank lemmas and checker, + its end theorem and the templates of the Fourier chain. The hosted + networks of these packages (Work/XHost in package/u8x0hq; Work/XHostD, + Work/XHostR and Work/XHostT in the lever packages) are adapted from those + network files, as their first lines say. + + a. Modified copies of OpenAI's statement file. Each file named + UniformFourierChallenge.lean under package/*/overlay/Work/ is a + modified copy of lean/ComparatorChallenges/UniformFourier.lean of + openai/math at the commit above: in package/u8x0hq the folders + FourierU8XM, FourierU8XMHH, FourierU8X0, FourierU8X0HH and + FourierU8X0HQ and their twins ending in Neg (10 files); + in package/leverF the folders FourierL3945F and FourierL3945FNeg (2 files); in package/leverB the folders FourierL3945H and FourierL3945HNeg (2 files); in package/leverA the folders FourierL2979H and FourierL2979HNeg (2 files); in package/lever2979 the folders FourierL2979 and FourierL2979Neg (2 files); in package/lever the folders FourierL3945 and FourierL3945Neg (2 files). Changes: the exponent + 1 - 1/(10^(13:ℕ)) is replaced by the package's exponent (in a folder + whose name ends in Neg, one unit stronger), and the seven names of + section 2 receive the package's suffix. Everything else in these files + is the upstream text, unchanged. Unlike the copies of section 9, these + files carry no comment inside them: they are kept byte for byte as they + were compiled, because scripts/build-and-check.sh derives them again + from third-party/openai-math/ (scripts/derive_challenges.sh) and + compares the two. This section is their notice. + b. Modified copies of OpenAI's proof files. In each package, the folders + Work/Fourier/ hold copies of eleven files of + lean/OAI/Computability/FourierTransform/ of openai/math and of five + definitions of its Goal.lean, made by Shea's script mkchain_c401g5.py + or by the agents' generators that copy its output under a new suffix. + Each begins with a comment that names the upstream file and states + what was changed. + c. The community's files. third-party/CrocSwap-integer-mult-bounds/ + staged544-terminal-gap-fill/ holds unmodified copies of 32 files of the + folder research/staged544-terminal-gap-fill/ of pull request #3945 of + CrocSwap/integer-mult-bounds at its head + 91f81d131252db704f945891da1ea54e29d46b8b (Dugongue's branch): the owner + data (FILL, PROFILE, ORDER, DISPATCH, PLAN, TEMPLATE, the two words and + the files of #3815 that #3945 carries as old-*), README.md, PROOF.md, + RESULT.json, SOURCES.json, LICENSE, NOTICE.md and the native lineage + notices. BLOBS.txt gives the git blob hash of each, as GitHub stores + it. That repository and its contributors' branches are published under + the Apache License, Version 2.0; the NOTICE.md and native notices of + that folder apply to these files and are quoted in substance in (g). + The files of #2979 (research/rank7-joint-endframes/ of the main branch + of CrocSwap/integer-mult-bounds at 20ecf289; Marius-Paul Dumitrean, + with the files of Mason Hale's #2917 and of #2942 that its NOTICE + names) are copied unmodified, 12 of them, into package/lever2979/ + and package/leverA/ under generators/tree/wht45/lever/p-alt/dl/ + main2979/: CLAIM.json, CREDITS.md, PINS.json, ALLOCATION-PINS.json, + the allocation files DISPATCH, FILL, ORDER, PROFILE and PROVIDERS, + and the data files PARENT-base, WORD-base and WORD-extra. + package/leverA/generators/tree/wht45/allheads/aA-data/in/alloc2979H/ + holds unmodified copies of its DISPATCH, ORDER, PROFILE and PROVIDERS + (beside the table with every head kept, FILL.json.gz, see (d)). Both + packages also hold #3945's owner/inputs/PLAN.json.gz and + TEMPLATE.json.gz under generators/tree/wht45/lever/g-heads/dl/pr3945/. + The generators check every one of these copies against its sha256 + (generators/tree.sha256) before they run; the same licence and the + notices of #2979 (for PLAN and TEMPLATE, of #3945) apply to them. + Both packages also hold generators/tree/wht43/bound-check/k-word/ + tools/build_tri_869.py, an unmodified copy of the community's word + builder construction/barch/build_tri.py (the same bytes as + research/complex-t21-owners/vendor/pr870/construction/barch/ + build_tri.py of its main branch, whose notices section 9, item g, + names); the generators do not run it. + More unmodified copies of the same folder of #3945 are in package/leverF/ + and package/leverB/, under generators/tree/wht45/lever/g-heads/dl/pr3945/ + owner/: 21 of the files above, and #3945's build_fill.py, check_gain.py + and verify.py (git blob hashes equal to GitHub's at 91f81d13); the same + licence and notices apply to them. + d. Data derived from the community's files. data/native/ holds the + canonical native words of #3945's two words (and of #3815's), the + output of #3945's own program native/run_native.py, run unchanged by + the agents. data/gcert/, data/residuals-*.json and data/t74ctl/ are + the agents' conversion of those words, and of the earlier T74 words, + into this project's certificate format (tools/lever/lower_b.py and + t74_control.py); data/t74ctl/inputs/ holds the community's T74 + inputs repackaged in the layout of #3945's package (TEMPLATE.json.gz + unmodified, and ORDER.json with the same content as the community's + T74 order). The Lean data of the lever packages (the words, the + dispatch, the tables of hosts) is generated from such conversions and + from the community's files by the generators in each package. The + tables with every head kept (the folders fill/ of the packages on + every head kept, where shipped) were made by the community's own + allocation programs (on #2979, its fill17.py and double.py; on #3945, + the hall_lp.py and build_fill.py of #3815 and #3945's offset step), + run with one added condition; each package's fill/ README says how, + and which of those programs it copies, with their notices. + e. Programs that re-implement or adapt the community's code: + - tools/lever/pricer.py re-implements (does not import) the community's + moment engine and kappa assembly (research/native-complex-moment552/ + engines/moment.py and outer.py, research/gauge44-frames-x/code/ + assemble.py). The package "native complex moment" is by Rohan Arun + with OpenAI Codex assistance, on Dugongue's #552, eumemic's #543 and + #558, and icekylinx's complex-cover notes; its outer assembly is + eumemic's, after icekylinx's #144 and Zhihao Chen's #23, with the + balanced prefix of the RaD project (hipotures). + - tools/lever/heads_fill.py and g0_staged.py re-implement the window + and family semantics of #3945's owner/verify.py (they do not import + it). + - tools/lever/lower_b.py extends this project's own lowering program + to the community's borrowed-helper words; the meaning of a warp + follows the community's native code (bw_transport.py, bw_emit.py of + #3945's native/vendor), which was read, not copied. + f. Scripts. scripts/apply-overlay.sh, build-and-check.sh and + run-comparator.sh are adapted from this project's community/scripts/; + scripts/base/, cc-jail/, bos/ and lever-run/ are the agents' scripts + as run. Those in bos/ and lever-run/ package a proof in the layout of + the entries of bigospeedrun/verifier and run that verifier's three + phases; the verifier's own code is not included, except its function + strip_comments (scripts/verifier.py of bigospeedrun/verifier, Apache + License, Version 2.0), whose logic scripts/bos/fspb_submission.py and + scripts/lever-run/isk_submission.py copy, as the line that defines it + says; the same function is in community/scripts/bos/mb_submission.py, + community/u8xmhh/scripts-as-run/build/fsb_submission.py and + package/leverF/logs/fc-engine/C3/scripts/isk_submission.py. + g. Credit for the circuits of the lever. + #3945, as its NOTICE.md and native lineage notices ask that the credit + be kept: + - #3945 (Dugongue, with substantial OpenAI Codex assistance, including + three parallel Codex agents): the terminal-width construction (26 + protected helper terminals from width 4 to width 5, with scalar and + native frames refitted), the idle-gap absorption proof, the + source-guarded recipe, the independent finite checks and the + integration. + - dataisfire, #3734: the staged544 supplier and its full source closure. + - zxv, #3682: the staged pair; #3638: the earlier T360 allocation. + - Ross Richardson, #3605: the staged entrance, cleanup and residual + checks (helpers 644 and 660 from width 8 to 7). + - Erwan Secousses / ChaloupeMusic, #3815, with the #3638 lineage: the + attained T360 owner clock and fill, and the allocation programs that + made the table with every head kept on #3945. + - hexapode (Pierre-Loic Doulcet), #3802 and #3875: the earlier complete + endpoint combination and its refinement. + - Dugongue, #3857 (general proof and evaluator work) and #3929 (the + transported-frame compiler). + - Sagar Thakrar, #3687: audit_core.py, which reimplements Arham Tahir's + coupled-carrier audit; roger-sato, #3693: the whole-word audit adapter; + roger-sato, #3642: the T530 release retimings. + - Jeremy Diviney, #3148: the coupled-carrier T740 packing cap; dcharb78, + #3133: helpers 586 and 588 lowered by coupled carrier folds. + - Marius-Paul Dumitrean (mdumitrean), #2979: joint rank-7 end frames and + five paired extractions, on Jeremy Kothe's #2957 gate rewrites; #2802 + (hostee moves and retired-lender aliases) and #2733. + - Jeremy Kothe: the frame and preload machinery, #2833 (dirt-entry + rewrite of helpers 530 and 542), #2957 (gate rewrites on Mason Hale's + #2917 words), and the source pipeline, label swap and order and fill + of #2462, #2588 and #2673; Mason Hale, #2917 (nine paired helper + extractions); Lyy-iiis, #2857 (shared kernels) and #2848; Dugongue, + #2863; philippeVV (Philippe Van Velzen), #2853, #2559 and #2679 + (evacuation, six pre-life hosts, the refit alias). + - Cinna Davis (@1337isnot1337), #2226, with OpenAI Codex assistance: + anticipatory dirty borrowing (the borrowed helpers and their warps) + and the native exact Clifford and operator machinery. + - Tekalign (@tekuuu), #2436: the four lifted targets, the joint + twelve-source construction, and the sparse native accelerator, with + the authors its SPARSE-NOTICE names. + - zxv, #2530: the eight source-partner aliases; Mason Hale, #2696: + concentrated source-partner assignment and an independent local + interpreter; themilkman216, #2621: the priority order; Vlado + Vojdanovski, #2322: generator utilities; Jeremy Kothe, #2312: the + helper width exchange; Dugongue, #2309, with Sagar Thakrar's audit + #2315. + - icekylinx, #433 and #514, and the retained native ancestry; + DreamingOfClouds (with Claude): the inherited wrapper and outer + machinery; chafreaky (Chafik Boukhalfa), #458, and its lineage. + - Josie Elliston, #1956 (bootstrap carried-cutoff repair); Sagar + Thakrar, #1964 (label and adapter checks, mutants). + - The T74 words and owner construction underneath: Rohan Arun (#1218, + #1297, #1319 and the T74 exact-fill owner construction, with OpenAI + Codex assistance), Marius-Paul Dumitrean (#1625: the pivot-566 + kernel, words, edits and rebuild scripts), Jeremy Kothe and LeverRank + (#1672), on Jeremy Kothe's k8 leaver word and seven-slot line (#1018, + #1042, #1274) with Thomas DiFiore (#1148), Jeremy Diviney (#1193) and + Chafik Boukhalfa (#1196); the outer and the assembly by Vlado + Vojdanovski (#1673), Chafik Boukhalfa (#1699, #1786) and Jeremy + Kothe (#1377, #1839). + - Rohan Arun's draft #3939 and his #3934 stack, and Chris R / + Clear1nsight's #3883, #3936 and #3941, are acknowledged by #3945 as + neighbouring work; they are not used here. + Checks of #3945 by others, which this project read and re-ran: Chris R / + Clear1nsight's audits #3969, #3988, #3994 and #4016; the exact + eight-stream operator replay of ChaloupeMusic's gist, on the operator + model of Nick Petalas (#3187) and Matarener (#3296). + #2979, from its pull request body, CREDITS.md and NOTICE ("All original + notices of the exported predecessor packages remain in force"): + - Marius-Paul Dumitrean (mdumitrean), #2979, prepared with substantial + AI assistance (Anthropic Claude, via Claude Code): the codimension-2 + census, the joint end-frame lowering of 22 restored helpers in five + groups, the five further extractions, the composition with #2957's + rewrites, producer and checks, the overlay stage, the six-class + adapters, the literal T74 allocation, the cap certificates and the + complete fresh replay; also #2930 (cap allocation, relaxation + tools), #2942 (four normal-45 extractions; its words are #2979's + parent) and #2843 (the flow model's starting point). + - Jeremy Kothe, #2957, #2948 and #2966: the fourteen declared gate + rewrites and their applier; #2894 and #2833: the preload re-synthesis + supplier, frame accounting and cleanup, source materializer. + - Mason Hale, #2917: the nine paired extractions, the T74 chronology + (ORDER and DISPATCH), the allocation checker, moment auditor, + extension stage and adapter derivation. + - Jeremy Diviney, #2908: the paired input/output extraction, its + compensation rule, the two-sided certificate and the closed-adapter + admission chain. + - Dugongue, #2969 (comparator composition and baseline), #2863 and + #2839 (packing lineage, owner engine). + - Yiyang Lu (Lyy-iiis), #2857 and #2848: shared-kernel words, staged + native and overlay tooling, the flow model and realization of the + allocation. + - Ross Richardson, #2918: the rank-seven obstruction for helper 408. + - Tekalign: the independent owner and chronology checker; icekylinx: the + exact free-operator auditor (#2833); themilkman216: the integrality + observation behind the allocation's face step. + - Gareth Davidson (bitplane), #1995 and #2013: the fixed-word + terminal-subspace bounds that frame stage 1. + - Underneath: Cinna Davis (#2226, dirty borrowing and warps), Jeremy + Kothe (#2312, width exchange), and the T74 line above. + The table with every head kept on #2979 was made by #2979's own + allocation programs, credited as above. + h. Credit for the Lean route. + - Ryan Shea: the conversion pipeline, the generators and the Lean + instantiation of Jeremy Kothe's #588 circuit (lean/complex588), which + these packages are laid over. + - Nil Mamano: the files named at the start of this section. + - Dugongue (#401): the entrance gauges and the banks of the nine-stage + network; Zhihao Chen / jacklightChen (#377, #425): its compressed + layout with banks and padding, and the written argument for mutable + sources; lydakis (#275): the bank patterns; DaysSky (#363): the + bridged layout, and the proposal, with a written proof in the + community's terms, to host helpers in idle arrays. + - Jeremy Kothe and DreamingOfClouds: the community's lemmas about where + a helper may end, on which the charge for exit frames rests. + - For package/u8x0hq: the community's U8 circuit, Jeremy Kothe's #869 on + his #799, with Chafik Boukhalfa's frame changes (#741) and + icekylinx's gauge44 construction (#645), as the community's notices + record it. + - The idea that Theorem 1G extends is Schönhage's τ-theorem for matrix + multiplication. + - OpenAI: the cost model, the statement and the step from the lengths + 2^k to every length. + i. research/. Written for this repository by the agents under my + direction. The sections cite papers by title or arXiv identifier and + the community's pull requests by number, commit and file hash; they + copy no paper text and no file of the community's repository, with + these exceptions: research/record-track/programs/a-fc/r2/tools/ + fallback_patch.py carries a modified copy (made tolerant, as its first + lines say) of the placement loop of construction/build_fill.py of + #3815 (Erwan Secousses / ChaloupeMusic; CrocSwap/integer-mult-bounds, + Apache License, Version 2.0); and research/record-track/programs/ + a-fc/r2/tools/fillmodel.py copies the window, family and width logic + of owner/verify.py of #3945 (Dugongue and the lineage its NOTICE.md + names, see (g); CrocSwap/integer-mult-bounds, Apache License, Version + 2.0), as its first lines say; research/why-the-savers-save/programs/ + helpers-narrower-ends-skeptic-rules/asm1042.json is an unmodified + copy of research/community-frontier1042-audit/ASSEMBLY.json of the + community's main branch (the community's #1042 audit, integrated by + its maintainer Douglas R. Colkitt on 13 October 2026); + research/record-track/data/a-fc/design/ + ORDER.json and DISPATCH.json hold #2979's allocation/ORDER.json and + DISPATCH.json (Mason Hale's #2917, as #2979's NOTICE says), with the + same content, re-serialised; and research/why-the-savers-save/ + programs/helpers-half-reads/bit/xcheck_base.json, the report of the + community's checker xcheck_p.py (DreamingOfClouds' line, on eumemic's + #555) on #589's word, has the same bytes as + research/community-frontier741-audit/bit/xcheck.json of the + community's main branch, integrated by Douglas R. Colkitt on 13 + October 2026 (these three: CrocSwap/integer-mult-bounds, + Apache License, Version 2.0). fallback_patch.py, and tools/ + place_patch.py, tools/hall_fc.py and tools/mkpatch_fill17.py of + programs/a-fc/, apply their changes to copies of community files that + they read by path (#3815's build_fill.py and hall_lp.py, #2979's + fill17.py); those files are not changed. The other programs of + programs/a-fc/ are mine. + j. What is mine: the mixed-target recursion (Theorem 1G and its Lean + proof in OpenAI's model); the lever (the head test, the half cut, the + full cut and its 24 + 24 split, the head lemma, the heads-first + certificate, and the tables with every head kept); the A-fc table on + #2979's words (its class solution and its tolerant placement); the Lean ports of + #3945 and #2979 (the conversion of their + words, the warp checker and its soundness, the networks of many copies + with hosting across copies, the dispatch, the generators); the Lean + engine of this project and its extensions for exit frames, mutable + sources, centre reading and hosting; the checks; the search and pricing + programs in tools/lever/ and tools/lever-hub/; and the research in + research/. tools/lever-hub/network/Gates.lean is an unmodified copy of + lean/complex588/Work/Bridge401/Gates.lean of Ryan Shea's repository + (commit 52394849c7ecf3412d39b925d75fc7fdb98994d8, Apache License, + Version 2.0; its header credits Dugongue, lydakis, jacklightChen and + DaysSky); the other files of tools/lever-hub/ are mine. + + The new files of package/, scripts/, tools/lever/, data/, results/ and + research/ were made between 2026-10-13 and 2026-10-20 the way section 4 + describes: by AI agents (Claude) under my direction. The credits, with + links, are in README.md. + +Not included in this repository and fetched by the build: Mathlib +(https://github.com/leanprover-community/mathlib4, Apache License 2.0) and its +dependencies. The comparator (https://github.com/leanprover/comparator) is a +separate tool and is not included. diff --git a/research/direct-mixed-flow/vendor/THREE-base-FULL-IDENTITY-NATIVE.json.gz b/research/direct-mixed-flow/vendor/THREE-base-FULL-IDENTITY-NATIVE.json.gz new file mode 100644 index 0000000000..b46d44c6ee Binary files /dev/null and b/research/direct-mixed-flow/vendor/THREE-base-FULL-IDENTITY-NATIVE.json.gz differ diff --git a/research/direct-mixed-flow/vendor/higher-moment-README.md b/research/direct-mixed-flow/vendor/higher-moment-README.md new file mode 100644 index 0000000000..0a736ca89e --- /dev/null +++ b/research/direct-mixed-flow/vendor/higher-moment-README.md @@ -0,0 +1,416 @@ +# Higher-moment strictification: tensor power 150 and a smaller uniform rank + +**Submission authorized by the user on 2026-10-21.** + +The complete p7 mixed supplier in [PR4416](https://github.com/CrocSwap/integer-mult-bounds/pull/4416) +has productive ranks down to 5 and paid ranks up to 48. Its chronological +product, paid target completion and disjoint splitting overcome that overlap. +This package improves the charged tail estimate in that construction, then +generalizes the logarithmic compiler bound of +[PR4411](https://github.com/CrocSwap/integer-mult-bounds/pull/4411). +At the same proposed conditional **κ = 0.00268647**, the results are: + +| Quantity | PR4416 | This package | +| --- | ---: | ---: | +| Chronological tensor power | 6,240 | **150** | +| Product ambient rank | `121^6240` | **`121^150`** | +| Independent productive fields before uniform compilation | `7688^6240` | **`7688^150`** | +| Maximum paid rank after splitting | `10^6240` | **`10^150`** | +| Minimum productive rank after paid completion | `11^6240` | **`15^150`** | +| Sufficient uniform ambient rank | `2^16201843136005340321` | **`2^349300000000`** | + +The tensor exponent decreases by **41.6×**; the exponent of the sufficient +uniform rank decreases by about **46.38 million×**. These are comparisons of +specified finite constructions and sufficient bounds. They are not runtime +speedups, practical template sizes or corresponding estimates for every +precision/storage constant. The winning uniform word is not materialized. +The selected frontier is unchanged. + +There are three connected deliverables: a general higher-moment splitting +bound, an exact smaller paid native construction, and a uniform-rank proof +compatible with the complete consumer. This is the larger scope chosen after +the H completion obstruction; no numerical measure of scientific significance +is asserted. + +## 1. Boundary contract and expansion decision + +Retain PR4359/PR4416's all-column native contract: a finite chronological word +computes specified transforms on distinct arbitrary productive fields; paid +positions act on the actual current physical owners. Whole-job normalizers +are restored, complete spectators are preserved, and owned centers are +initialized, retained until safe erasure and never credited as new inputs. +At every positive column multiplicity, ranks multiply by that multiplicity. +Matching only rank numbers is insufficient without these native hypotheses. + +The source product algorithm runs one U copy for every productive role of V, +then substitutes V into each common chronological paid position of those U +copies. Fields may contain correlated data but have distinct physical slots. +Never combine two different paid positions of the same suspended U copy. +The targets and paid ranks are products; their moments multiply. This is a +finite chronological substitution of algorithms. Read +[the pinned product proof](vendor/p7-TENSOR.md), especially §§1–3 and 6. + +After the product finishes, normalize each complete rank-K output job by its +permitted whole-job conjugation. When K= 1, +u >= C, sigma = t+u >= 1, +J = c^v, L = b^v. +``` + +The bases c,b and the power v are integers, so L and J are exact integer +ranks. All moments here are finite sums over the actual rank inventory. + +For any original paid rank R>J, write R=qJ+r with 0<=r= 1`; this is why sigma must be at +least one. Keeping the original P_t^v as an overcount for all unsplit calls +gives total original-paid charge at most + +``` +P_t^v + 2 P_(t+u)^v / J^u. +``` + +For a completion D=L−K with 0=1 and logarithm power p=1/q. +Its proof only needs the logarithmic factor to be increasing. The same +argument works for **any real p>0**, including p>1, which is useful when +the separated unit's ambient rank m is itself large. + +Assume the finite source/exit compiler in +[FINITE-PRECOMPILATION.md](vendor/FINITE-PRECOMPILATION.md). Write +`L(n)=P_n/B_n`, with ordinary base `L(n)=n` for `0<=n=m its exact +integer-batch construction gives + +``` +L(n) = sum_s w_s L(n−s) + sum_e x_e L(e), +sum_s w_s = 1, n/m < s <= n, +sum_e x_e e^t <= sum_s w_s s^t, +e <= r_max (n/m)^theta < n, +theta = log(r_max)/log(k_min) < 1. +``` + +Choose `theta < theta_bar=a/b < 1` and p>0 with + +``` +2^(b−a) r_max^b <= m^a, +theta_bar^p < eta = t m^(t−1), +m^(1−t) < 2^p. +``` + +Then **`L(n) <= n^t (1+log2(n))^p` for every integer n>=1**; define the +right side to be zero at n=0. + +For 2<=n=m put `A(n)=(1+log2(n))^p`. The shifted logarithm +condition gives `A(e) <= theta_bar^p A(n)` for every exit, hence + +``` +sum_e x_e e^t A(e) <= theta_bar^p A(n) sum_s w_s s^t. +``` + +For y=s/n>1/m, concavity of x^t gives +`1−(1−y)^t >= t y >= eta y^t`. Since A is increasing, the source complement +capacity obeys + +``` +n^t A(n) − sum_s w_s (n−s)^t A(n−s) + >= eta A(n) sum_s w_s s^t, +``` + +with zero-rank complements treated separately. The strict inequality +`theta_bar^p < eta` closes strong induction. This uses no concavity of A +and introduces no unknown multiplicative constant. + +This is available for every separated unit with the stated t-superpotential. +Choose rational theta_bar sufficiently close to one: since r_max max((1−t)*log2(m), log(eta)/log(theta_bar)) +``` + +satisfies the other two conditions. Thus the leaf-count estimate has the +general form `L(n) <= n^t (1+log2(n))^p` with an effective fixed p. At fixed +p, a target gap z−t requires a sufficient H of order +`(p/(z−t))*log(p/(z−t))`. This concerns normalized rank-one leaf counts in +the finite compiler; it does not bound full word size or physical runtime. + +The compiler's integral batch replication, arbitrary original arrays, +whole-job routing and finite owned-bank allocation are unchanged. With +N=2^H and desired uniform exponent z>t, the final sufficient condition is + +``` +(1+H)^p < 2^((z−t)H). +``` + +For the new p7 unit, take `theta_bar=6/7`, `p=13`. Exact tests give + +``` +10^7 < 15^6, +2*(10^150)^7 <= (121^150)^6, +eta > 0.144386809622024146828684313913 > (6/7)^13, +(121^150)^C < 6.907234273066686405887998346943 < 2^13. +``` + +The smaller logarithmic power 12 fails the stated eta condition. Let +`z−t = 1/700000000`, exactly the uniform-saving slack already used by +PR4416's outer point. The rank **N=2^349300000000** satisfies + +``` +349300000001^13 < 2^499. +``` + +The preceding grid point H=348600000000 fails its corresponding comparison +with 2^498. This is the first successful multiple of 700,000,000 for this +majorant: the function `(z−t)H ln(2) − p ln(1+H)` is strictly convex, starts +at zero with negative derivative, and has just one positive zero. This +does not certify a minimum native program. + +To separate the two contributions, retaining the older power majorant on +the new v=150 unit already gives `H0=37443877100` and +`H1=140829080288374101`. That is about a 115× reduction in the exponent +from the changed tail/rank separation alone. The logarithmic majorant then +reduces that exponent by a further factor of about 403,175. + +## 5. Complete consumer and finite constants + +The complex uniform saving is **376107/140000000**, approximately +0.00268647857142857. This is exactly PR4416's uniform endpoint; neither +its tested saving nor its outer parameters change. Put + +``` +kappa = 0.00268647, d=(0.00268648−kappa)/7 = 1/700000000, +uniform = kappa+6d, b_outer = kappa+5d, +a_outer = kappa+4d, q_outer = kappa+3d, +epsilon=1−d, beta=1−3d, r0=d/10, stop=layout=d, +ordinary_BIT_saving=0.0027. +``` + +The checker replays the byte-pinned PR4405/PR4416 parameter ledger and +requires exact equality with all saved p7 parameters, nine rows, 54 checks +and three extra guards. It separately executes only the historical +`check_ledger.py` ledger function and its comparison constants as another +oracle: all nine rows agree and all 63 predicates remain strict. Its derived +grid/backoff is recorded explicitly; the old m=73 admission code is not run. +The minimum nine-row saving minus κ is exactly +`524529867/122500000000000000`. + +Mutations close epsilon, remove layout funding, raise unfunded κ, close +the uniform gap, underfund BIT, add an old per-axis scan or make group width +equal to global dimension. Each must fail its relevant ledger. + +The newly compiled word supplies its **own** finite constants. If U counts +actual raw p7 instances, allocate U distinct owned centers. Let W be the +final productive width, P the paid rank-one count, and R the full native +record/normalizer count including completion, splits and compiler routes. +As in the pinned closure argument, use + +``` +G = 2490856*U + 8*R, Z = W+U, +E = 64*(Z+N+P+G+1)^3, +B_constant = P+E, C0 = 32*N*B_constant^2. +``` + +Pay actual coordinate movement separately. Retain every owned center until +its creating unit erases it; centers are excluded from productive W. +The fixed-word recurrence and eventual constant absorption have the source +form, with these newly expanded counts substituted. Numerical full-word +counts, denominator heights and practical precision thresholds are not +computed here. Neither a smaller N nor a favorable moment supplies an +independent proof of the inherited physical/analytic premises. + +## 6. Reproduction, provenance and coverage + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B research/higher-moment-strictification/verify.py +python3.12 -B scripts/research_package.py --package research/higher-moment-strictification --check-only +python3.12 -B scripts/research_package.py --package research/higher-moment-strictification +``` + +To generate a fresh receipt, use `verify.py --out /absolute/new/path.json`. +The saved [RESULT.json](RESULT.json) records all intervals, finite parameters, +integer comparisons, ledgers, controls and source/verifier hashes. + +Logarithms use 80 exact terms of the binary-reduced atanh series with the +geometric tail. Exponentials use 64 terms after binary scaling into [0,1/2], +outward rounding at precision 2^−192, twice the next term for the remaining +tail, and outward repeated squaring. Negative arguments use reciprocal +intervals. Every decision uses fractions or integers, with no floating-point +acceptance test. A separate exact small product/pad/split example checks +the inventory and preserved surplus, and a sublinear-tail counterexample +guards the theorem's exponent restriction. + +Canonical base is `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority revision +7. [SOURCES.json](SOURCES.json) pins the orientation metadata. The 15 unchanged +exports in [VENDOR.json](VENDOR.json) include complete source paths, commit +IDs, Git blob names and SHA256 hashes; the verifier authenticates both hashes +without requiring Git. Pending commits are represented by self-contained +exports, not implied publication ancestry. Source exports remain unchanged. + +The PR4426 invoice oracle is compiled from its authenticated source bytes, +with only ROOT and PHASES rebound to the exported file locations. Its literal +controller, supplier-receipt and port-recipe checks remain intact. The two +ledger oracles retain predecessor code and attribution; they are arithmetic +cross-checks, not fresh native supplier admission. + +Local validation used Python 3.12.8 on macOS arm64. The registered replay, +metadata/pin check and committed-byte preflight passed. A separate Git-free +copy passed `python3.12 -I -O -B verify.py` in 0.333 seconds; changed-source +and changed-receipt controls rejected. The optional full source-history +preflight could not run because this checkout is shallow. All pending-source +inputs are self-contained exports; standalone replay does not need those +foreign Git objects. No Lean, Docker, native all-size or historical suite was +run. These checks authenticate the stated result, not independent scientific +acceptance. + +Overlap at 18:19 UTC covered 536 open PR bodies and 3,279 discussion/comment +records with complete reported pagination, plus local notes. The newer +#4420/#4428/#4429 checks cover earlier strictification proof/arithmetic and +slightly smaller sufficient powers; #4426 supplies the invoice replay reused +here. No remote closed-PR-body or arbitrary code-diff search was performed. +The task metadata records the changed scope and remaining direct-compiler +question. Submission was authorized after local review; no Discussion claim was posted. + +## Open next questions + +1. **A direct compiler for overlapping ranks.** A finite acyclic integer + schedule would remove strictification altogether. Start by replacing the + Pascal matching step when a paid rank exceeds a target rank, retaining + arbitrary inputs, complements and chronological suspension. No such + termination/matching proof is supplied by the mixed moment alone. +2. **Full finite-word size and precision.** Derive compressed upper bounds + for the compiler's batch denominators, widths, scalar passes and owned + instances at the specified rank. Ambient rank is only one size parameter; + this remains the main barrier to assessing practical constants. +3. **Independent scientific review.** Check the higher-moment inequality, + the p>1 induction and the native product/adapters at their actual callers. + The unchanged raw supplier's internal paid bill and all-column/physical + premises remain separate inherited obligations. Another search of nearby + c,b,u,v values would not resolve those obligations. + +Prepared by zxv with substantial OpenAI Codex assistance in discovery, +implementation and writing. No subagents or independent human review were +used for this new work. New material is Apache-2.0. Native/controller lineage: +zxv's PR4359 and its retained contributors. Product/padding and p7 controller: +@1337isnot1337's PR4412/PR4414/PR4416. Integer mixed flow: Jacob Alan +Sussman, Theorem 1G. Logarithmic-majorant predecessor: zxv's PR4411. +Invoice replay: Ryanson Jonathan / @pinterbanget, PR4426, with Claude Code +assistance and Apache-2.0. The retained supplier and outer sources preserve +their original contributor credit and notices. diff --git a/research/direct-mixed-flow/vendor/higher-moment-RESULT.json b/research/direct-mixed-flow/vendor/higher-moment-RESULT.json new file mode 100644 index 0000000000..e66b39c674 --- /dev/null +++ b/research/direct-mixed-flow/vendor/higher-moment-RESULT.json @@ -0,0 +1,384 @@ +{ + "finite_controls": { + "rank_one_surplus": 13, + "sublinear_tail_counterexample": { + "J": 1, + "R": 100, + "actual_charge": 100, + "invalid_upper": { + "lower": "73.245553203367586639977870888654", + "upper": "73.245553203367586639977870888655" + }, + "sigma": "3/4", + "t": "1/2" + }, + "toy_paid": { + "1": 5, + "4": 9 + }, + "toy_targets": { + "10": 2, + "25": 1, + "9": 1 + } + }, + "invoice_oracle": { + "laurent_monomials": 14, + "main_targets": { + "121": 224, + "25": 448, + "41": 448, + "57": 448 + }, + "new_kappa_claimed": false, + "paid": { + "1": 37305, + "16": 448, + "2": 10695, + "3": 3360, + "32": 448, + "4": 1530, + "48": 448, + "5": 300, + "8": 1464 + }, + "paid_idles": { + "16": 448, + "32": 448, + "48": 448, + "8": 1344 + }, + "rank_one": [ + 131723, + 131115 + ], + "status": "PASS_PR4416_INVOICE_REBUILD", + "targets": { + "121": 224, + "25": 448, + "41": 448, + "5": 420, + "57": 448, + "6": 270, + "7": 840, + "8": 1395, + "9": 3195 + } + }, + "kappa": "268647/100000000", + "outer": { + "ledger": { + "functional_checks": { + "fixed_halo_explicit_metadata_branch": "13475000001/175000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000", + "new_semantic_group_guard": "3/700000000" + }, + "margins": { + "boundary_algebraic_matrix": "329093274529867/122500000000000000", + "fused_gaussian": "329093273589601/122500000000000000", + "global_coordinate_router": "1880533/700000000", + "group_bit_router": "1316373794358401/490000000000000000", + "group_scans": "349999999/350000000", + "main_transform": "329093099529867/122500000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "50094718274529867/122500000000000000" + }, + "parameters": { + "a": "1880533/700000000", + "b": "940267/350000000", + "beta": "699999997/700000000", + "bit_saving": "27/10000", + "cap_xi": "111344718099529867/122500000000000000", + "complex_uniform_saving": "376107/140000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "268647/100000000", + "lambda_": "39892541/40000000", + "lambda_prime": "174529867/175000000", + "layout": "1/700000000", + "q": "470133/175000000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "33581/12500000" + }, + "strict_checks": { + "actual_bit_above_effective": "9467/700000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "11155282162970133/61250000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "699529867/122500000000000000", + "cap_above_band": "50094718099529867/122500000000000000", + "cap_below_cell": "11155281725470133/122500000000000000", + "cap_below_phase_cell_power": "133655281900470133/122500000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "9997233/350000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "698589601/122500000000000000", + "gaussian_above_main": "87029867/61250000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "3494358401/490000000000000000", + "group_gauge_power_slack": "11155282154220133/61250000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "698119469/700000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "477749790400418148631/500000000000000000000000", + "lambda_above_internal": "1/1400000000", + "lambda_above_sigma": "3/1400000000", + "lambda_above_tau": "1/1400000000", + "lambda_prime_above_lambda": "1/1400000000", + "lambda_prime_above_leaf": "699059733/245000000000000000", + "leaf_saving_above_effective": "349059733/245000000000000000", + "main_transform_above_kappa": "524529867/122500000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "2155924779/28000000", + "microbox_halo_volume": "55300000003/700000000", + "new_complex_uniform_saving_above_b": "1/700000000", + "new_semantic_guard_with_C1_one": "1/700000000", + "polynomial_products_above_kappa": "69811947/70000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "699059733/245000000000000000", + "q_positive": "470133/175000000", + "short_record_fallback": "349059733/350000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "49765625699529867/122500000000000000", + "stop_below_one": "699999999/700000000", + "stop_positive": "1/700000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/700000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/700000000", + "union_tag_work_per_visit_fits_record": "3/700000000" + } + }, + "legacy_63_checks": { + "actual_bit_above_effective": "9467/700000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "11155282162970133/61250000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "699529867/122500000000000000", + "cap_above_band": "50094718099529867/122500000000000000", + "cap_below_cell": "11155281725470133/122500000000000000", + "cap_below_phase_cell_power": "133655281900470133/122500000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "9997233/350000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fused_gaussian_above_kappa": "698589601/122500000000000000", + "gaussian_above_main": "87029867/61250000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "3494358401/490000000000000000", + "group_gauge_power_slack": "11155282154220133/61250000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "698119469/700000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_online_final": "477749790400418148631/500000000000000000000000", + "improvement_over_pkg_k2": "1008477392794717479267911225169191627777122102965890395790280701170194526587548469132116575062403/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1699": "1008828268656645435748941712936355250934431507/1000000000000000000000000000000000000000000000000", + "improvement_over_pr1712": "5044141343283227178741362020680007884145727138632283638941299969772687285461029288600736779707649/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1758": "1006724491197700948453466314800026327686526580209199320247542619067215757027414399369818327775017/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1786": "10067152118499510912194521335000000000000000000000000000000001999999800001/10000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1828": "2013430087748910957328658012158594846003377122994839409079344959674400000000000000000000000004006719019826502178085342683975683/2000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1839": "5033575219372277393321645030396487115008442807487098522698362399185677258698371805868475000000001001679754956625544521335670993920703/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1875": "5033575219372277393321645030396487115008442807487098522698362399185677258698371805868471719335776838627743415457068895139647759399172939286143496816535216421325187363046885361425772909502231218314437622205930116079297234806627210590217190600996553729143901162562581526621534715086055386213403722175000000001001679754956625544521335670993920703/5000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1876": "503357521937227739332164503039648711500844280748709852269836239918567725869837180586847171933577683862774341545706889513964775939917293928614349681653521642132518736304688536142577290950223121831443762220593011607929723480662721059021719060099655372914390116256258152662153471508605538621340372217196657216794137380775174500330086462142358142864921147118845386980694114022172311249292673931726844600000000000000000001001679754956625544521335670993920702577/500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_pr1897": "1006715043874455478664329006079297423001688561497419704539672479837135451739674361173694343867155367725548683091413779027929551879834587857228699363307043284265037472609377072285154581900446243662887524441186023215859446961325442118043438120199310745828780232512516305324306943017211077242680744434393314433588274761550349000660172924284716285729842294237690773961388228044344622498585347863453689118814253082419197486359454032147189198319033143866021423837056207677317517847011467076188001061138620310116832610271556685687769184940440093096226243113127523863162928128796969576356494654526264864467/1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "improvement_over_previous_local_final": "477749790400418148631/500000000000000000000000", + "improvement_over_previous_package": "10086500976855635663689448641223998986170598784229341400200650717283025923262102542077285802551153/10000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "lambda_above_internal": "1/1400000000", + "lambda_above_sigma": "3/1400000000", + "lambda_above_tau": "1/1400000000", + "lambda_prime_above_lambda": "1/1400000000", + "lambda_prime_above_leaf": "699059733/245000000000000000", + "leaf_saving_above_effective": "349059733/245000000000000000", + "main_transform_above_kappa": "524529867/122500000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "2155924779/28000000", + "microbox_halo_volume": "55300000003/700000000", + "polynomial_products_above_kappa": "69811947/70000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "699059733/245000000000000000", + "q_positive": "470133/175000000", + "short_record_fallback": "349059733/350000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "49765625699529867/122500000000000000", + "stop_below_one": "699999999/700000000", + "stop_positive": "1/700000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/700000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/700000000", + "union_tag_work_per_visit_fits_record": "3/700000000" + }, + "legacy_backoff": "21/5000000000", + "legacy_grid": 10000000000, + "minimum_margin_minus_kappa": "524529867/122500000000000000", + "rejected_controls": { + "closed_epsilon": [ + "actual_logarithmic_gamma_guard", + "epsilon_below_one", + "gaussian_above_main", + "global_gamma_power_slack", + "new_semantic_guard_with_C1_one", + "source_axis_superpolynomial" + ], + "closed_uniform_gap": [ + "new_complex_uniform_saving_above_b" + ], + "group_equals_dimension": [ + "group_below_dimension", + "group_key_fits_record", + "membership_arithmetic_fits_record" + ], + "insufficient_BIT": [ + "actual_bit_above_effective" + ], + "missing_layout": [ + "positive_layout_slack" + ], + "old_per_axis_scan": [ + "old_per_axis_scan_above_kappa" + ], + "unfunded_kappa": [ + "boundary_algebraic_matrix_above_kappa", + "fused_gaussian_above_kappa", + "global_coordinate_router_above_kappa", + "group_bit_router_above_kappa", + "main_transform_above_kappa" + ] + } + }, + "predecessor_H": 16201843136005340321, + "rank_exponent_reduction_factor": "16201843136005340321/349300000000", + "rejected_mutations": [ + { + "failed_at": "complete charged normalized moment", + "mutation": "too_short_product" + }, + { + "failed_at": "tail moment exponent at least one", + "mutation": "sublinear_tail" + }, + { + "failed_at": "strict finite ranks", + "mutation": "lost_separation" + } + ], + "schema": "higher-moment-native-strictification/1", + "scope": "Conditional charged transformation and finite compiler rank. Native all-column, physical, analytic, precision, storage, fixed-tape and recovery premises remain inherited. No new kappa, selected frontier or practical word.", + "source_sha256": { + "research/higher-moment-strictification/vendor/FINITE-PRECOMPILATION.md": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8", + "research/higher-moment-strictification/vendor/FINITE-TEMPLATE-CLOSURE.md": "3f8508c63862dd83968bd30df91b08ba5afcee1e10db15ca546cdff0caef95d9", + "research/higher-moment-strictification/vendor/LOG-MAJORANT.md": "3b74b9b22258bd265a025a7e6f06f199e1625f3f0b735b972e6e91047eeb8e45", + "research/higher-moment-strictification/vendor/check_ledger.py": "1dd56009986eb14dd6603c9193c7ad71dd45c7d005bf71c9cd3f916e66f54d98", + "research/higher-moment-strictification/vendor/invoice-review/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/higher-moment-strictification/vendor/invoice-review/vendor/NOTICE.md": "da983933f88516f311b2bb8750802e4bd03a537eacc0bde351cfb36b77a93f15", + "research/higher-moment-strictification/vendor/invoice-review/vendor/P7-FACTOR.json": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598", + "research/higher-moment-strictification/vendor/invoice-review/vendor/RESULT.json": "9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab", + "research/higher-moment-strictification/vendor/invoice-review/vendor/SUPPLIER-RESULT.json": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6", + "research/higher-moment-strictification/vendor/invoice-review/verify.py": "a72b0c0da8beedbdd1a65e83009295c31fcd30664e85aeb1b620235042cbf0b5", + "research/higher-moment-strictification/vendor/outer_endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "research/higher-moment-strictification/vendor/p7-ENDPOINT.md": "e7056020bb9757d45fdf1a8eea9e811040ce72d53bc16e7f90f72a5e712fa3e9", + "research/higher-moment-strictification/vendor/p7-NATIVE.md": "26bf9312cdb496b1113c9ddd8aa0fa922ed9e480005703212942af358394183d", + "research/higher-moment-strictification/vendor/p7-RESULT.json": "9b814be97e3b45fcc28eafa8a65694897a7387f71a14d44796c6aadf303d7fab", + "research/higher-moment-strictification/vendor/p7-TENSOR.md": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3" + }, + "status": "PASS_HIGHER_MOMENT_STRICTIFICATION", + "strictification": { + "alpha": { + "lower": "0.999999984403907977028692329024", + "upper": "0.999999984403907977028692329025" + }, + "ambient": "121^150", + "cutoff_base": 10, + "delta": { + "lower": "0.877942785206780917722562601792", + "upper": "0.877942785206780917722562601793" + }, + "floor_base": 15, + "gamma": { + "lower": "0.903981539721477814868265523050", + "upper": "0.903981539721477814868265523051" + }, + "materialized_product_or_uniform_word": false, + "maximum_paid": "10^150", + "minimum_target": "15^150", + "normalized_paid_upper": "1000000635204363556136250491144161837938214611877310981113991233610194892493163042995932145748443566398677069212449817849347590568236176459579539001979969712918643865874634198553766207360874447748594152802372160823515706917812863624324588309448164247279181670682524587922166460943924036141865870233593287572765694512062966529681268238027148629402289227769948550454004579273122673115283917084645472692704053780372399331749927451738974321744119172945600769747/1000001500000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000", + "old_rank_one_bound_lower": { + "lower": "2.524485503105612497245887828271", + "upper": "2.524485503105612497245887828272" + }, + "old_rank_one_gamma": { + "lower": "0.998191712473006243732169576257", + "upper": "0.998191712473006243732169576258" + }, + "paid_moment_exponent": "16216419/12500000", + "productive_fields_before_uniform_compiler": "7688^150", + "rank_one_surplus": "131723^150-131115^150", + "rational_upper_limits": [ + "99999999/100000000", + "181/200", + "439/500" + ], + "strict_moment_gap": { + "lower": "0.000000864794339252354870976549", + "upper": "0.000000864794339252354870976550" + }, + "tail_offset_u": "3/10", + "tensor_power": 150, + "tested_saving": "33581/12500000" + }, + "tail_only_power_majorant": { + "H0": 37443877100, + "H1": 140829080288374101, + "N": "2^140829080288374101", + "scope": "Tail transformation alone, retaining the older power majorant.", + "theta_upper": "6/7" + }, + "tensor_power_reduction_factor": "208/5", + "uniform_rank": { + "H": 349300000000, + "N": "2^349300000000", + "eta": { + "lower": "0.144386809622024146828684313913", + "upper": "0.144386809622024146828684313914" + }, + "eta_minus_theta_to_p": { + "lower": "0.009586237698168518342122636732", + "upper": "0.009586237698168518342122636733" + }, + "gap": "1/700000000", + "grid_step": 700000000, + "integer_test": { + "left_base": 349300000001, + "left_exponent": 13, + "right_base": 2, + "right_exponent": 499 + }, + "logarithm_power": 13, + "m_to_saving": { + "lower": "6.907234273066686405887998346942", + "upper": "6.907234273066686405887998346943" + }, + "previous_grid_point_rejected": true, + "smaller_logarithmic_power_rejected": true, + "t": "12466419/12500000", + "theta_upper": "6/7", + "uniform_saving": "376107/140000000" + }, + "verifier_sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326" +} diff --git a/research/direct-mixed-flow/vendor/p7-NATIVE.md b/research/direct-mixed-flow/vendor/p7-NATIVE.md new file mode 100644 index 0000000000..394d9a03c1 --- /dev/null +++ b/research/direct-mixed-flow/vendor/p7-NATIVE.md @@ -0,0 +1,180 @@ +# Complete all-fresh p7 native controller + +This package extends PR4359's exact local construction at +`da637c87c89482bc4c86be36bd0071b3d400dbed`. It uses the newly regenerated p7/keep232127 +Laurent word, the authenticated THREE-base full-identity native supplier, +and the source whole-job helper normalizers. The new checks establish finite +physical contacts and complete inventories. The native all-column semantics, +permitted scalar/routing primitives, uniform compiler and outer analytic +transfer remain explicit inherited premises. + +## 1. Literal word and actual arbitrary inputs + +The selected p7 controller has 15 chronological native calls, seven main pairs, +and 112 ports in each side of a pair. Its right scalar program runs first, +then its literal LOCAL/IDLE/ADD/SIGNED_SWAP program, then its left scalar +program. An independent exact Laurent interpreter replays this entire order +and checks every coefficient of the resulting diagonal operator on all 14 +formal input roles. Changing one backward local orientation to forward must +fail that equality. + +`factor_receipt.py` authenticates the exact original factor generator and its +two imported dependencies, regenerates only mask 232127, and compares every +serialized coefficient, boundary word, diagonal monomial and literal event +with `P7-FACTOR.json`. The independent Laurent replay then checks the complete +word separately. This is one admitted mask, not an exhaustive p7 census or +an optimality claim. + +There are 1,568 independent main input arrays. Each of the 15 native calls +also gets 408 distinct fresh arbitrary helper fields, named by stage and +native helper role. The total is 6,120 additional independent inputs. A +helper is never a copy, a main idle field or another stage's helper. The +source native word accepts every persistent input arbitrarily, returns each +helper autonomously, and has no external cleanup bank. Its one owned center +is initialized and erased and receives no productive credit. + +Apply helper normalizers only around a whole local native invocation. Their +actual endpoint widths are 5,6,7,8,9 with counts 28,18,56,93,213 per invocation. +The source gate authenticates the underlying word, both orientations, +helper boundaries and arbitrary-input receipt. It also restores the original +eight rank-eight center jobs per invocation; their former 3+5 split is +unnecessary before the new tensor strictification. The exact midpoint and +absolute phase remain checked against the original native receipt. + +## 2. Native owner maps at ambient rank 121 + +The old source utility used a fixed 73-axis container. Its owner formula has +a dimension-independent extension, which is checked here at every one of +15 stages and 112 ports rather than assuming that the old container extends. + +For port normal q, let b_1,...,b_8 be the actual first eight orthogonal axes +from its pinned initial idle recipe. The checker establishes + +``` +b_i dot b_j = delta_ij, b_i dot q = 0. +``` + +At stage s>0, let e_i be the fresh coordinate axes in positions +`9+8*(s-1),...,9+8*s-1`. Put `v_i=b_i+e_i` over F2 and define + +``` +G_s(x) = x + sum_i (v_i dot x)*v_i. +``` + +The v_i are mutually orthogonal isotropic vectors. Hence G_s is orthogonal +and involutive, swaps each b_i with its corresponding fresh e_i, and fixes q. +Stage zero uses the identity. The checker verifies the complete 121-column +matrix and its involution, orthogonality and q action in every stage/port. +All coordinates outside the original nine-axis block and that stage's fresh +eight-axis block are fixed. This supplies a legal full-field coordinate map. + +Write C_a for the source Gaussian factor on a nonzero binary axis a. Its +Fourier multiplier is a Z4 phase. The phase polynomial of a product of C_a +factors has linear terms modulo4 and quadratic coefficients modulo2; +higher parity terms vanish modulo4. A physical translation adds an even +linear phase. Every C_a product and translation has multiplier one at +Fourier address zero, so its constant phase is independently fixed to zero. +Comparing the stored linear and quadratic parts therefore proves the full +phase, rather than merely the polar rank. + +Let `F_s` denote the positive product on the first `9+8*s` axes and let + +``` +D_0 = F_0*C_q^(-1), +D_s = product of positive factors on fresh block s (s>0). +``` + +For each forward/backward native call the checker constructs the four +entry/exit coordinate-and-translation maps between its actual main references +and a shared spectator frame. It verifies both map directions, the exact +raw diagonal difference D_s, and the cross operator D_s*C_q^(-1) for a +forward call or D_s*C_q for a backward call. Thus the raw local contracts are + +``` +forward: D_s * [[1,0],[C_q^(-1),1]], +backward: D_s * [[1,-C_q],[0,1]]. +``` + +These are raw-input operator equalities, so they remain valid after the +controller's earlier scalar basis changes and on arbitrary correlated data. +The exact audit covers all 6,720 main contacts (15*112*4), with inverse maps. +The all-column lift replaces each coordinate by its common column block; +this is the inherited native generator substitution, not an assertion that +tensor powers distribute over addition of matrices. + +## 3. Endpoint targets and all full idle jobs + +Every literal diagonal Laurent monomial has Q exponent +1 or -1 and stage +exponents zero or one. For each of all 1,568 main outputs, the checker builds +its actual positive target axes, proves their binary independence, and checks +the full Gaussian phase after the specified translation. The 784 endpoints +that require a nonzero translation reject its omission. + +The main target profile is `{25:448,41:448,57:448,121:224}`. The exponent +factorization alone is not used as physical admission: each target has the +separate 121-dimensional axis/phase check above. + +The controller retains twelve complete idle windows. All are paid at their +literal event on both main sides and every port: + +| Window index | Pair | Stages | Rank | Physical fields | +| --- | --- | --- | --- | --- | +|0|1|0,1|16|224| +|1|1|2|8|224| +|2|2|0,1,2,3|32|224| +|3|2|4|8|224| +|4|3|0,1,2,3,4,5|48|224| +|5|3|6|8|224| +|7|4|8|8|224| +|9|5|10|8|224| +|11|6|12|8|224| +|15|3|9,10,11,12,13,14|48|224| +|16|4|11,12,13,14|32|224| +|17|5|13,14|16|224| + +A Counter equality checks a bijection between this paid inventory and the +literal IDLE events; no omitted or duplicated metadata window can alter the +bill. Every emitted recipe retains its pair, stage list, port and both +physical owner names. + +For an initial window, begin with the source's exact rank16 axis list and +translation and append its later disjoint fresh blocks. For every other +window, use precisely its listed fresh blocks with zero translation. The +checker proves rank, independence and the complete phase identity against +the product of its D_s operators. A whole-job coordinate conjugation sends +these independent axes to a canonical rank-r call. Helpers are all fresh, +so there is no partially completed borrowed idle input and no helper/bridge +chronology to assume. The entire original idle operator runs at its original +literal event. + +## 4. Complete bill and new fixed constants + +The final raw inventory is + +``` +T = {5:420,6:270,7:840,8:1395,9:3195,25:448,41:448,57:448,121:224}, +P = {1:37305,2:10695,3:3360,4:1530,5:300,8:1464,16:448,32:448,48:448}. +``` + +There are 7,688 independent productive fields and 55,998 paid calls. Target +rank mass 131,723 minus paid rank mass 131,115 gives exact surplus 608. Maximum +paid rank 48 exceeds minimum target 5, so this raw word requires the separate +tensor construction, target completion and paid-call splitting before the +original compiler applies. + +The scalar bill includes the 15 oriented native words, every boundary ADD +and SCALE, every boundary swap as three additions plus one negation, all +literal bridges and all seven terminal signed swaps. Its conservative allowance +is 2,490,856. Every coefficient in the boundary word is a unit. Coordinate +routes, inverse routes and phase translations are additional finite movement +operations and must be counted in the newly expanded word. No old p3 movement, +prefix-growth, row-stock or precision constant is reused. + +Give every instantiated raw unit its own owned center for as long as that +unit is suspended. In every product or uniform compilation, retain all actual +scalar operations, native calls, whole-job routes and inverse routes, with +all owned initialization and erasure. The new full-word counts determine +replacement precision and storage constants. The finite construction is +specified algorithmically; its enormous final tensor/uniform word has not +been materialized. This is a conditional supplier construction, not an +unconditional integer-multiplication theorem. diff --git a/research/direct-mixed-flow/vendor/p7-RESULT.json b/research/direct-mixed-flow/vendor/p7-RESULT.json new file mode 100644 index 0000000000..ebb30a9b3b --- /dev/null +++ b/research/direct-mixed-flow/vendor/p7-RESULT.json @@ -0,0 +1,296 @@ +{ + "endpoint": { + "compiler": { + "H0": 4307773805920, + "H1": 16201843136005340321, + "N_encoding": "2^16201843136005340321", + "delta": "1/1400000000", + "exit_coefficient_log2_upper": "26640", + "final_strict_power_gap": "1/1400000000", + "h": "1/26", + "materialized_tensor_rule_or_uniform_word": false, + "negative_log2_eta_upper": "147931769/1250000", + "paid_max_bound_encoding": "10^6240", + "rank_one_induction": "131723^n > 131115^n; target padding adds equal paid and target rank, and splitting preserves rank", + "t": "12466419/12500000", + "target_max_encoding": "121^6240", + "target_min_encoding": "11^6240", + "tensor_power": 6240, + "theta_upper": "25/26", + "z": "139623893/140000000", + "z0": "1396238929/1400000000" + }, + "gain_over_PR4359": "38647/100000000", + "gain_over_PR4405": "19069/50000000", + "gain_over_PR4414": "33/5000000", + "gain_over_allfresh_p3": "5223/25000000", + "kappa": "268647/100000000", + "ledger_source_sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "minimum_outer_margin": "524529867/122500000000000000", + "negative_controls": { + "closed_epsilon": { + "actual_logarithmic_gamma_guard": "0", + "epsilon_below_one": "0", + "gaussian_above_main": "-1410399/122500000000000000", + "global_gamma_power_slack": "-1/7000000000", + "new_semantic_guard_with_C1_one": "0", + "source_axis_superpolynomial": "0" + }, + "closed_uniform_gap": { + "new_complex_uniform_saving_above_b": "0" + }, + "insufficient_BIT": { + "actual_bit_above_effective": "-270533/700000000" + }, + "unfunded_outer_point": { + "boundary_algebraic_matrix_above_kappa": "-525470133/122500000000000000", + "fused_gaussian_above_kappa": "-526410399/122500000000000000", + "global_coordinate_router_above_kappa": "-3/700000000", + "group_bit_router_above_kappa": "-1405641599/490000000000000000", + "main_transform_above_kappa": "-700470133/122500000000000000" + } + }, + "outer": { + "functional_checks": { + "fixed_halo_explicit_metadata_branch": "13475000001/175000000", + "new_BIT_row_stock_sublinear_in_active_group": "697899997009/700000000000", + "new_semantic_group_guard": "3/700000000" + }, + "margins": { + "boundary_algebraic_matrix": "329093274529867/122500000000000000", + "fused_gaussian": "329093273589601/122500000000000000", + "global_coordinate_router": "1880533/700000000", + "group_bit_router": "1316373794358401/490000000000000000", + "group_scans": "349999999/350000000", + "main_transform": "329093099529867/122500000000000000", + "microbox_face_corrections": "13475000001/175000000", + "polynomial_products": "699999999/700000000", + "sparse_union_movement": "50094718274529867/122500000000000000" + }, + "parameters": { + "a": "1880533/700000000", + "b": "940267/350000000", + "beta": "699999997/700000000", + "bit_saving": "27/10000", + "cap_xi": "111344718099529867/122500000000000000", + "complex_uniform_saving": "376107/140000000", + "d": "1/700000000", + "epsilon": "699999999/700000000", + "kappa": "268647/100000000", + "lambda_": "39892541/40000000", + "lambda_prime": "174529867/175000000", + "layout": "1/700000000", + "q": "470133/175000000", + "r0": "1/7000000000", + "stop": "1/700000000", + "tested_saving": "33581/12500000" + }, + "strict_checks": { + "actual_bit_above_effective": "9467/700000000", + "actual_logarithmic_gamma_guard": "1/700000000", + "actual_logarithmic_group_guard": "11155282162970133/61250000000000000", + "alpha_logarithm_absorption": "1/7000000000", + "boundary_algebraic_matrix_above_kappa": "699529867/122500000000000000", + "cap_above_band": "50094718099529867/122500000000000000", + "cap_below_cell": "11155281725470133/122500000000000000", + "cap_below_phase_cell_power": "133655281900470133/122500000000000000", + "complex_above_effective": "1/700000000", + "complex_below_one_over_32": "9997233/350000000", + "complex_endpoint": "1/350000000", + "epsilon_below_one": "1/700000000", + "epsilon_positive": "699999999/700000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "698589601/122500000000000000", + "gaussian_above_main": "87029867/61250000000000000", + "global_coordinate_router_above_kappa": "1/175000000", + "global_gamma_power_slack": "9/7000000000", + "group_below_dimension": "1/350000000", + "group_bit_router_above_kappa": "3494358401/490000000000000000", + "group_gauge_power_slack": "11155282154220133/61250000000000000", + "group_key_fits_record": "1/350000000", + "group_positive": "699999997/700000000", + "group_scans_above_kappa": "698119469/700000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "477749790400418148631/500000000000000000000000", + "lambda_above_internal": "1/1400000000", + "lambda_above_sigma": "3/1400000000", + "lambda_above_tau": "1/1400000000", + "lambda_prime_above_lambda": "1/1400000000", + "lambda_prime_above_leaf": "699059733/245000000000000000", + "leaf_saving_above_effective": "349059733/245000000000000000", + "main_transform_above_kappa": "524529867/122500000000000000", + "membership_arithmetic_fits_record": "1/700000000", + "microbox_face_corrections_above_kappa": "2155924779/28000000", + "microbox_halo_volume": "55300000003/700000000", + "new_complex_uniform_saving_above_b": "1/700000000", + "new_semantic_guard_with_C1_one": "1/700000000", + "polynomial_products_above_kappa": "69811947/70000000", + "positive_layout_slack": "1/700000000", + "q_below_effective": "1/700000000", + "q_below_internal": "1/700000000", + "q_below_leaf": "699059733/245000000000000000", + "q_positive": "470133/175000000", + "short_record_fallback": "349059733/350000000", + "source_axis_superpolynomial": "1/700000000", + "sparse_union_movement_above_kappa": "49765625699529867/122500000000000000", + "stop_below_one": "699999999/700000000", + "stop_positive": "1/700000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/700000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/700000000", + "union_tag_work_per_visit_fits_record": "3/700000000" + } + }, + "schema": "native-p7-padding-strictification-outer-endpoint/1", + "scope": "Source-bound native p7 geometry, a finite tensor recipe with target padding, exact moment and outer inequalities, and a specified finite uniform rank. Native tensor closure and the PR4359 inherited precision, storage, analytic, fixed-tape and recovery hypotheses are written premises, not a full formal theorem certificate.", + "status": "PASS_CONDITIONAL_P7_OUTER_POINT", + "strictification_source_sha256": "1f3c2a38b34d9dad7266be212ca5d0225827d8e05bda4831e6c25c5713f624f0", + "tested_saving": "33581/12500000" + }, + "independent_interval_crosscheck": true, + "scope": "Conditional native construction and exact finite arithmetic. The finite word and inherited physical, precision, analytic and fixed-tape proofs are not formally verified or materialized by this checker.", + "source_files": 23, + "status": "PASS_SOURCE_BOUND_CONDITIONAL_P7_PAID_PADDING_IMPROVEMENT", + "strictification": { + "alpha_interval": { + "lower": "0.99999998440390797702869232902431332", + "upper": "0.99999998440390797702869232902431333" + }, + "alpha_upper": "99999999/100000000", + "completion_decay_block_length": 2, + "controls": { + "one_decay_block_rejected": true, + "undamped_completion_rejected": true, + "unpadded_rank_one_tail_rejected": true + }, + "cutoff_base": 10, + "cutoff_encoding": "10^6240", + "decay_block_count": 16, + "decay_block_length": 390, + "delta_interval": { + "lower": "0.64382470915163933966321257464784307", + "upper": "0.64382470915163933966321257464784308" + }, + "delta_upper": "2/3", + "exponent": 6240, + "gamma_interval": { + "lower": "0.99819171247300624373216957625759087", + "upper": "0.99819171247300624373216957625759088" + }, + "gamma_upper": "4991/5000", + "materialized_tensor_or_completed_word": false, + "native_inventory": { + "artifact_hash_encoding": "Uncompressed UTF-8 JSON, sort_keys=True, separators=(comma,colon)", + "artifact_sha256": "12784fff6a13e3752ea6e80018e0484c5766a8adf2e88a7e71c80cf2bb68f398", + "contacts": 6720, + "dimension": 121, + "factor_receipt_sha256": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598", + "fresh_helper_fields": 6120, + "keep": 232127, + "limits": "Finite exact physical controller admission; inherited all-column local word, tensor strictification, new full-word precision/stock and outer transfer remain written proof obligations.", + "main_fields": 1568, + "native_scalar_allowance": 2490856, + "native_source_gate": "PASS_ACTUAL_ARBITRARY_HELPERS_AND_COMPLETE_PHASE_CORRECT_IDLE_JOBS", + "negative_controls": { + "omitted_endpoint_translation_rejected": 784, + "wrong_native_orientation_rejected": true + }, + "p": 7, + "paid": { + "1": 37305, + "16": 448, + "2": 10695, + "3": 3360, + "32": 448, + "4": 1530, + "48": 448, + "5": 300, + "8": 1464 + }, + "paid_calls": 55998, + "productive_fields": 7688, + "rank_margin": 608, + "scalar_allowance": 2490856, + "schema": "source-bound-p7-all-fresh-complete-native-controller/1", + "source_sha256": { + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "research/kappa-rebuild/complex/fresh-certificates/THREE-base-HELPER-BOUNDARIES.json.gz": "f90517e395bde58c72cacd5d3481c4ea31d459fe4535384ac16547ac40460555", + "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39", + "research/kappa-rebuild/complex/full_identity_rebuild.py": "9af2ffbb0038c92e2a7d281081b0daaeadce75b11b566e5427845dc1af91e33d", + "research/kappa-rebuild/controller/P3-NATIVE-COVER.json.gz": "facfc6d6ecde151afb7e6a167776f3fdaac1c816e785a21a39f7f0bfd9140f3f", + "research/kappa-rebuild/controller/p3_native_cover.py": "fae71fcbbd20b9ee73b049cf6f43ea1d048217fb15feb6055a007e47da3363fe", + "research/kappa-rebuild/transfer-audit/p3_cover_audit.py": "a0fe9a26f77556e83b31b0c91fea909d6f3d8209d0f9f7ad4e5bc1375d33615e", + "research/kappa-rebuild/transfer-audit/p3_native_audit.py": "5504a55a50546418d10c522984438cdeedb44993f7c1dab7bd4aa1ae0515d902" + }, + "status": "PASS_EXACT_LAURENT_ALL_MAIN_CONTACTS_ENDPOINTS_AND_FULL_IDLE_PHASES", + "targets": { + "121": 224, + "25": 448, + "41": 448, + "5": 420, + "57": 448, + "6": 270, + "7": 840, + "8": 1395, + "9": 3195 + }, + "whole_idle_profile": { + "16": 448, + "32": 448, + "48": 448, + "8": 1344 + } + }, + "new_max_target_encoding": "121^6240", + "new_min_target_encoding": "11^6240", + "normalized_moment_upper_rational": "10240625039/10240638976", + "paid": { + "1": 37305, + "16": 448, + "2": 10695, + "3": 3360, + "32": 448, + "4": 1530, + "48": 448, + "5": 300, + "8": 1464 + }, + "paid_rank_one_moment": 131115, + "productive_fields": 7688, + "rank_one_surplus_encoding": "131723^6240-131115^6240", + "schema": "p7-paid-target-completion-tensor-certificate/1", + "scope": "Exact moment bounds for the documented chronological native product, paid target completion and disjoint splitting. Native all-column, precision, storage, analytic and fixed-tape premises remain separate; no full multiplication theorem is formally verified.", + "source_sha256": { + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + "status": "PASS_EXACT_P7_TARGET_COMPLETION_STRICTIFICATION", + "strict_moment_verified": true, + "strictification_gap": { + "lower": "0.00000136095023295546357907266586564", + "upper": "0.00000136095023295546357907266586565" + }, + "strictification_gap_rational": "13937/10240638976", + "target_floor_base": 11, + "target_floor_encoding": "11^6240", + "target_rank_one_moment": 131723, + "targets": { + "121": 224, + "25": 448, + "41": 448, + "5": 420, + "57": 448, + "6": 270, + "7": 840, + "8": 1395, + "9": 3195 + }, + "tested_saving": "33581/12500000", + "theta_upper": "25/26" + } +} diff --git a/research/direct-mixed-flow/vendor/theorem-1g.md b/research/direct-mixed-flow/vendor/theorem-1g.md new file mode 100644 index 0000000000..36d2399f35 --- /dev/null +++ b/research/direct-mixed-flow/vendor/theorem-1g.md @@ -0,0 +1,264 @@ +# Theorem 1G: mixed jobs with grouped paid blocks + +This note holds the proof behind the recursion lever of the record track: an extension of the τ-theorem (in the +form argued in [../../existence-routes/](../../existence-routes/), "Theorem 1") from paid moves of rank 1 to paid +blocks of any rank. It was written on 14 October 2026 by an AI agent working for me, in a simple model of jobs, and +it is reproduced here with its notation, cleaned of internal file names. + +**Status.** *Argued by hand, not checked.* Two independent AI skeptics tried to refute it on 14 October: one +re-derived the logic and simulated the construction with its own code, the other built the construction explicitly +(units, random matching inside the prescribed classes, a generic deadlock test) and checked the hypotheses of the +induction on the actual flows. Neither found an error. No person and no proof checker has read this text. A Lean +form of the theorem inside OpenAI's model was built on 19 October as part of the lever record (section 6); its +status is the record's: *proved in Lean*, as part of each of the five lever packages (in `package/leverF` and `package/leverB`, the modules under `Work/Mixed/` and `Work/MixedCost/`), with the official comparator accepting each result and three skeptics upholding each. + +Labels used inside the proof: [argued] (an argument given here in full, by hand; no proof checker has read it), +[computed] (a program, named in section 4), [what-if] (a price that rests on an unchecked step), [open]. + +## 0. The job model + +This is the model of the τ-theorem's proof, recalled so that this note can be read alone. + +- A **job of size s** is: apply the Walsh-Hadamard transform H on s chosen address bits of a register holding + 2^ν entries (ν ≥ s), that is, a batch of 2^(ν-s) independent transforms of size 2^s. Its cost is counted per entry: + T(s) is the number of full passes over the register (one per single-bit Hadamard leaf, one per free pass). A pass + over a fraction w of the entries costs w. +- A **rule** (a mixed unit) at block m: a word, correct for every number f of digit columns, with W_k registers + carrying a **rank-k target** (k of the m rows transformed, the other m - k untouched), paid blocks, and F free + register-passes. Applied at column c it turns jobs of the target sizes kc into jobs of the paid sizes r_j c. +- **Split**: a job of size a + b is the job of size a followed by the job of size b (Hadamards on disjoint bits + commute), at cost T(a) + T(b). A **plain leaf** of size s costs s passes. +- **Φ_τ** of a set of jobs (weighted by fractions of entries) is the sum of weight times size^τ. +- **τ** of a rule is the root in (0, 1) of Σ_j r_j^τ = Σ_k W_k k^τ (the *balance*). With every r_j = 1 this is the + τ-theorem's M = Σ_k W_k k^τ. + +The community's recursion is this model with one target size: a paid block is a recursive call on a whole register, +and the W arrays of the next level are W slices of that one call's batch. A rule with targets of two sizes needs jobs +of two sizes at once, which no single call's batch provides; that is what the construction below supplies. + +## 1. Re-check of the rank-1 case (the τ-theorem) + +- **Step 1 (multinomial flow).** With p_k = W_k/M and u(a) = multinomial(|a|; a) Π p_k^(a_k), Pascal's rule gives + u(b) = Σ over k with b_k ≥ 1 of p_k u(b - e_k) for b ≠ 0, so M u(b) = Σ_k W_k u(b - e_k). The region + R = {a : m c(a) ≤ L} is down-closed. A frontier point b (not in R, with some b - e_k in R) has size + c(b) = k c(b - e_k) ≤ kL/m ≤ L and c(b) > L/m. Confirmed [argued]. An exact re-run found 0 unbalanced sizes, + Φ(sources) = M to 10 digits, and sources in (L/3, L] [computed]. +- **Step 2 (Φ conservation).** Each unit is Φ-neutral at τ, so Φ(sources) = Φ(leaves) = M. Confirmed. +- **Step 3 (free passes).** The sum of u over generation j is (W/M)^j, so the sum of u is at most M/(M - W), and the + free passes come to F/(M - W) per unit of leaf Φ. The passes spent re-grouping portions (one per class level) cost + O(1) per register used by a unit, so they fold into F. +- **Lemma 2 (lockstep).** Process(g, λ) issues move k of all units in the class. The outputs plus (λ/M) Source at + generation g equal (λ/M) J at generation g, which is exactly what the child consumes. At level g there are + M^(g_max - g) calls with λ = M^-(g_max - g), so the sources used add up to Source exactly [argued]. The literal + simulation was re-run on 1+4 in 10 at L = 12, 30, 54, on 1+1 in 4 at L = 30, and on 7+38 in 88 at L = 12 + (7,833 classes): every class was fed exactly, the sources used equal Source, and the leaves equal M u(0) + [computed]. +- **Step 5 (top split and constant).** Every rest has size s - c(a) < (1 - 1/m)s. The induction closes with + C' = (A + c0)/(1 - (1 - 1/m)^τ). A sharper constant is C' = (A + c0)/η_m with + η_m = min over t in [1/m, 1] of (1 - (1-t)^τ)/t^τ, which is at least 1 - (1-1/m)^τ (Lemma A below). +- **Rounding.** The number of fluid portions is the number of lockstep classes, at most M^(g_max+1) = n^O(ln M/ln k_min). + That is polynomial in n, not the number of lattice points, and still far below 2^(n/2) batch entries, so dyadic + rounding costs a relative 2^-Ω(n). The claim stands; only the count in the earlier text was wrong. +- **A hypothesis that both theorems need and the earlier text did not state.** Each unit must be a correct word at + every column count f that occurs: products of target ranks in the rank-1 case, and products of target and paid ranks + in Theorem 1G. The community's engine also asserts m^2 > 2 max(r)^2; what that halving constraint asks of a new + recursion was not examined here. + +## 2. Lemma A: the top-split induction with leftovers (the exact condition) + +**Setting.** T(n) is the per-entry cost of the best schedule for a job of size n (with at least n/2 batch bits). A +*flow for n* consists of: +- source weights w(s) ≥ 0 on sizes 1 ≤ s ≤ n, with Σ w = 1; +- exit weights x(e) ≥ 0 on sizes e < n: jobs the flow leaves over, each completed by a separate call of the whole + procedure; +- an internal cost I ≤ A Φ̂ (free passes, re-grouping, plain size-1 leaves), where Φ̂ = Σ_s w(s) s^τ; +- a deadlock-free order, given that each exit call returns a completed job. + +The schedule splits the top job into portions w(s), each portion being s + (n - s). The s-parts feed the flow, and +the (n - s)-parts and the exits are done recursively. So + + T(n) ≤ c0 + I + Σ_e x(e) T(e) + Σ_s w(s) T(n - s). + +**Lemma A** [argued]. Let ψ ≥ 1 be nondecreasing, and let β > 0 and n0 be such that for every n ≥ n0 there is a flow +with + + (E) Σ_e x(e) e^τ ψ(e) + ψ(n) Σ_s w(s) (n - s)^τ ≤ ψ(n) (n^τ - β Φ̂). + +Then T(n) ≤ C n^τ ψ(n) for all n, with C = max{ max_{n L gives ρ_s c(b) > r_j L/m. Some b - e_k lies in R(ρ_s), so ρ_s c(b) ≤ kL/m ≤ L. ∎ + +**Lemma D (exits)** [argued]. Outputs leave the tree only at generation 0 (d = G). There each class has at most one +unit (at column ρ_s, present when m ρ_s ≤ L), and its P outputs have sizes ρ_s r_j. Φ(exits) = Φ(sources) exactly. +Every exit has size e ≤ r_max · r_max^G ≤ r_max (L/m)^θ with θ = ln r_max / ln k_min < 1, so ln e ≤ θ ln L. Exits of +size 1 are plain leaves. +*Proof.* By Lemma B, outputs at generation ≥ 1 are all consumed. Every unit is Φ-neutral at τ, and every consumed job +was produced or sourced, so Φ(exits) = Φ(sources). G ≤ log_(k_min)(L/m) because c(a) ≥ k_min^|a|, which gives +ρ_s ≤ r_max^G ≤ (L/m)^θ. Finally r_max ≤ m^θ (since r_max = k_min^θ ≤ m^θ), which gives ln e ≤ θ ln L. ∎ + +**Lemma E (number of units)** [argued]. units ≤ Φ(sources) / (W k_min^τ (1 - k_min^-τ)), with no log factor. +*Proof.* A unit at depth d sits at column ≥ c(a) ≥ k_min^(G-d), and its input Φ is +Σ_k W_k (k · col)^τ ≥ W k_min^τ k_min^(τ(G-d)). The total input Φ at each depth is at most Φ(sources), since Φ only +moves down through the tree or leaves it. Summing the geometric series over G - d gives the bound. ∎ + +**Lemma F (order: no deadlock)** [argued]. Procedure Process(s), called with the parent's round-j outputs pending: +1. the class's inputs are exactly those outputs plus top sources (Lemmas B and C); +2. for j = 1..P: issue round j of every unit of s, running the word's free steps between moves as the word says; if + d(s) = G, complete each exit job by a top call Do(e); otherwise call Process(s.j); +3. return. +A round j+1 is issued only after Process(s.j) has returned, which means every unit that consumed a round-j job has +finished. A unit starts only after all its inputs exist. So this is a straight-line program. Its recursion depth is +G + 1, and every exit call is a smaller instance (e < n). ∎ + +A careless order does deadlock: if a unit took one input from round 1 of unit A and another from round 2 of A, while +A's round 2 waits for that very unit, nothing can start. Lockstep classes, in which each child class takes only the +outputs of one round, rule this out. + +**Theorem 1G** [argued, job model]. Under (S): T(n) ≤ C n^τ (ln n)^κ for all n ≥ 3, where +κ = ⌈ln(2/η_m) / ln(1/θ)⌉ (κ = 0 when r_max = 1) and C depends only on the rule. So T(n) = O(n^(τ+δ)) for every +δ > 0. +*Proof.* Take L = n. The flow is the tree normalised to source weight 1. The sources lie in (n/m, n] (Lemma C), so +K = m. The internal cost I ≤ A Φ̂ with A = (F + O(W))/(W k_min^τ (1 - k_min^-τ)) (Lemma E, plus one size-1 leaf per +unit of leaf Φ). The exits satisfy Φ(exits) = Φ̂ and ln e ≤ θ ln n (Lemma D). The order is valid (Lemma F). Lemma A3 +applies with ψ = max(1, ln)^κ and β = η_m/2. The batch-bit and dyadic-portion arrangements are as in section 1: the +number of classes is at most Σ_d P^d = n^O(ln P / ln k_min). ∎ + +*Remarks.* +- With every r_j = 1 the tree is the rank-1 construction (ρ = 1, exits = leaves), and κ = 0 recovers O(n^τ). +- Exact O(n^τ) for grouped rules, with no log factor, would need a flow with Φ(exits) ≤ (η - β) Φ̂ (Lemma A2). This + tree has Φ(exits) = Φ̂, so by A4 it cannot give that [open]. +- The log factor costs nothing in the exponent: every saving below 1 - τ is reached with a fixed constant. OpenAI's + goal is a big-O statement, so an existential constant is allowed. +- Without (S): Lemma B needs r_j ≤ k for the pairs that meet, and Lemma D needs r_max < k_min. The case r_max ≥ k_min + is open. An example (targets {3:1, 2:4}, paid {1:6, 2:2}) has a fluid linear programme whose optimum was still rising + at n = 480. + +## 4. Numerical checks [computed] + +Every program named here is in [../programs/theorem-1g/](../programs/theorem-1g/) and its output in +[../data/theorem-1g/](../data/theorem-1g/). All were re-run on 19 October 2026 for this revision, on an Apple +M4 Mac mini with Python 3.9, in under a minute each and under 300 MB; every output was identical to the one made on +14 October. + +Three test rules, plus a control: +- A: targets {4:1, 3:2}, rounds 1,1,1,1,2,2 (τ 0.746375; θ 0.631, κ 3); +- B: targets {7:1, 4:1}, rounds 1,1,1,1,2,2,2 (τ 0.928234). This is the truncation of the pure rule {7:2} with paid + {1:4, 2:3} plus a rank-3 idle block; +- C: targets {5:1, 4:3}, rounds 1×6, 2×2, 3×2 (τ 0.930659; θ 0.792, κ 4); +- D: the rank-1 control 1+4 in 10. + +1. **Literal lockstep** (`tree_flow.py`): explicit round sequences, each round in word order. A, B and C were run at + L = 40 and 150 (up to 259 classes). Every class was exactly fed (no surplus, no deficit), the sources used equal the + merged count, and the exits match the merged count by size. +2. **Merged exact checks** at L = 10^3, 10^5, 10^7 (up to 1.6e10 classes, counted with multiplicity): 0 unbalanced + points; all sources in (L/m, L]; Φ(exits)/Φ(sources) = 1.000000000000; the largest exit at or below the bound + r_max (L/m)^θ (16,384 ≤ 21,761 for A at L = 10^7, 2,048 ≤ 2,391 for B, 177,147 ≤ 295,508 for C); the unit count + within the bound of Lemma E. +3. **Cost of the whole schedule** (`recur.py`; F = 0, L = n, exits by recursive calls), T(n)/n^τ: + + | rule | n = 50 | n = 400 | n = 3,200 | n = 6,400 | + |---|---|---|---|---| + | A | 1.612 | 1.896 | 2.034 | 2.052 | + | B | 1.144 | 1.197 | 1.218 | 1.229 | + | C | 1.177 | 1.192 | 1.249 | 1.246 | + | D (rank-1 control) | 1.162 | 1.180 | 1.183 | 1.183 | + + The grouped rules grow slowly, far below (ln n)^κ; A's local slope over the last doubling is 0.759 against + τ = 0.746 and falling. The control is flat, as the rank-1 theorem says. +4. **Re-check of the rank-1 theorem** (`recheck_t1.py`, which imports the τ-theorem's own programs from + [../../existence-routes/programs/tau-theorem-and-laser/](../../existence-routes/programs/tau-theorem-and-laser/)). +5. **The community's circuit T74, as a what-if** (`hub_whatif.py`). Control: the balance with one job size reproduces + the community's figure for T74, 1.6797550e-3 (1.6797549561e-3). The mixed price, assuming every idle block of T74 + is a head or a tail on its own array, is 1.8169468e-3 (+8.17 %), separated (8 < 25). **This assumption turned out + to be false**: only 11,010 of the 22,748 idle blocks are heads and none is a tail (the README of this section, + section 4.5), so this figure is **refuted** as a price of T74. It stays here as the test it was. + +The skeptics' own programs, written from this text without reusing its code: +- `indep_tree.py` rebuilds the merged tree independently (toy rule A and the T74 mixed rule up to L = 10^8): + 0 unbalanced points, Φ ratio 1, exits within the bound. `partial.py` prices partial truncation, which showed that + the result depends on how many idle blocks really are heads. +- `explicit_sim.py` builds explicit unit objects, matches outputs to inputs at random inside the prescribed classes, + and runs a generic topological sort of start, issue and finish events as a deadlock test independent of Lemma F; + Φ is tracked to 50 digits. Every lockstep run is deadlock-free with Φ(exits) = Φ(sources); a deliberately careless + matching across classes deadlocks, as it should. +- `cost_fit.py` and `check_E.py` compute the actual flows up to n = 12,800 and check hypothesis (E) of Lemma A3 at + every n there, the unit bound of Lemma E and the exit bound; for the T74 rule `check_E.py` checks every n up to + 20,000 and every 997th n up to 3,000,000. No violation anywhere. They also + confirm Lemma A4: (E) with ψ = 1 fails at every n, as predicted. + +## 5. What the new recursion needs that the community's uniform recursion does not have + +The community's recursion is one call per job: a call of size s slices its own batch into W rank-m arrays at column +s/m, and each paid block is an independent recursive call; no call ever needs a job of another size. Theorem 1G needs: +1. **Several sizes at once.** A unit at column c takes rank-73 arrays of size 73c and smaller ones (rank 49 for the + half cut, rank 25 for the full cut) in a fixed ratio. These come from different producers' outputs, never from one + call's batch. +2. **Fluid portions.** Classes are fractional portions of batches, which needs a portion and relabel step in the cost + model and dyadic rounding with at least n/2 batch bits (the class count is polynomial in n). +3. **A class tree in lockstep**, ordered as in Lemma F. +4. **A top split** of the top job into frontier portions of sizes in (n/m, n] plus rests, done recursively. +5. **Exit calls.** Jobs of size ρ_s r_j are completed by fresh top calls. +6. **Mixed-target words.** The word with the head blocks removed or shortened must be proved correct for the reduced + targets at every column count f that occurs. +7. **Hypothesis (S).** On the circuits of the record track it holds with room: for the half cut every paid rank is at + most 48 and the smaller job is 49; for the full cut every paid rank is at most 24 and the smaller job is 25. +8. **The structure of the circuit.** Each block that is cut must be the first operation on its array, acting on that + array alone (the truncation lemma of [../../existence-routes/](../../existence-routes/)). This is the head test + of the README, section 4.5. + +## 6. The Lean form + +On 19 October the recursion was written in Lean inside OpenAI's RAM model as part of the lever record. Two things +changed against the plan in section 5: + +- **No log factor.** The Lean cost bound does not use Lemma A3. It applies Lemma D at a rate point z1 and argues that + for every exponent z above z1 the exits' share of the sources' Φ shrinks by a factor at most 2 (E m/n)^(z - z1), + where E = r_max^(G+1) bounds the exits; since E m/n tends to 0, Lemma A closes with ψ = 1 for all large n, and a + finite maximum covers the small ones. The statement is: if the balance holds at z1, then for every z in (z1, 1] there + is a constant C with cost ≤ C · 2^n · (n + 1)^z. The constants exist but are astronomically large; only their + existence is used, which OpenAI's big-O goal allows. Lemma A4 is not contradicted: it concerns the exponent τ itself. +- **The program.** Units are coded as sequences of roles (the Pascal bijection of Lemma B as arithmetic on codes); + each paid block of a class becomes one child call whose answers are read back ("Hadamards on disjoint bits + commute"); the leaf class hands its exits to one fresh top call; the order is the lockstep order of Lemma F, by + induction over the word. + +Status of this Lean form: *proved in Lean*, as part of each of the five lever packages (in `package/leverF` and `package/leverB`, the modules under `Work/Mixed/` and `Work/MixedCost/`), with the official comparator accepting each result and three skeptics upholding each. Its module and theorem names are listed in the lever package +(package/leverB/). diff --git a/research/direct-mixed-flow/vendor/tree_flow.py b/research/direct-mixed-flow/vendor/tree_flow.py new file mode 100644 index 0000000000..31a9c1ae4d --- /dev/null +++ b/research/direct-mixed-flow/vendor/tree_flow.py @@ -0,0 +1,167 @@ +# tree_flow.py (bound-check/rl-prove, 14 Oct 2026). The DILATED LOCKSTEP TREE of PROOF.md section 3 (Theorem 1G), +# for a mixed rule with GROUPED paid blocks: targets {k: W_k} (k in K), rounds r_1..r_P (P_r rounds of rank r), and +# the separation hypothesis r_max < k_min. Exact integers / fractions. +# u(a) = multinomial(|a|; a) prod_k W_k^a_k (a in N^K), c(a) = prod_k k^a_k, m = max K, +# R(rho) = {a : m rho c(a) <= L}, G = max{|a| : a in R(1)}. +# Class s (a round sequence of length d <= G, rho_s = product of its ranks): u(a) units at column rho_s c(a) for +# every a in R(rho_s) with |a| = G - d. Round j of class s feeds class s+(j) only. +# Checks (merged by (d, rho) with path multiplicities N(d, rho)): +# (1) exact balance: at every point b in R(rho') the child's demand equals the parent's round output; +# (2) every other demand is a SOURCE of size in (r_j L/m, L] (root: (L/m, L]); +# (3) exits only at generation 0: P jobs of sizes rho*r_j per class, all <= r_max * (L/m)^theta, theta = ln r_max/ln k_min; +# (4) Phi conservation at tau_c: Phi(sources) = Phi(exits); (5) unit count <= Phi(sources)/(W k_min^tau (1-k_min^-tau)). +# Literal lockstep simulation (lockstep_literal): explicit recursion over round sequences, a pool of issued jobs per +# class, every class must find all its inputs issued (parent round j + sources) and consume every job it is given. +import sys +from fractions import Fraction as Fr +from math import factorial, log, prod +from itertools import product as iprod + +def tau_c(Wt, P): + lo, hi = 0.0, 1.0 + for _ in range(200): + mid = (lo + hi) / 2 + if sum(w * k ** mid for k, w in Wt.items()) > sum(p * r ** mid for r, p in P.items()): hi = mid + else: lo = mid + return (lo + hi) / 2 + +def lattice(Wt, L, rho): + """points a in R(rho), as tuples over sorted K, grouped by |a|""" + K = sorted(Wt); m = max(K) + pts = {} + def rec(i, a, c): + if i == len(K): + pts.setdefault(sum(a), []).append(tuple(a)); return + k = K[i]; e = 0; cc = c + while m * rho * cc <= L: + rec(i + 1, a + [e], cc); e += 1; cc *= k + rec(0, [], 1) + return pts + +def mult(a): + return factorial(sum(a)) // prod(factorial(x) for x in a) + +class Tree: + def __init__(self, Wt, P, L): + self.Wt, self.P, self.L = dict(Wt), dict(P), L + self.K = sorted(Wt); self.m = max(self.K) + assert max(P) < min(self.K), "separation r_max < k_min fails" + self.Wv = [Wt[k] for k in self.K] + self.lat = {} + self.G = max(lattice(Wt, L, 1)) + def R(self, rho): + if rho not in self.lat: self.lat[rho] = lattice(self.Wt, self.L, rho) + return self.lat[rho] + def u(self, a): return mult(a) * prod(w ** x for w, x in zip(self.Wv, a)) + def c(self, a): return prod(k ** x for k, x in zip(self.K, a)) + def inR(self, a, rho): return self.m * rho * self.c(a) <= self.L + def units(self, d, rho): + return {a: self.u(a) for a in self.R(rho).get(self.G - d, [])} + def demand(self, d, rho): + need = {} + for a, ua in self.units(d, rho).items(): + for i, k in enumerate(self.K): + b = list(a); b[i] += 1; b = tuple(b) + need[b] = need.get(b, 0) + self.Wt[k] * ua + return need + +def check(Wt, P, L, tau=None): + T = Tree(Wt, P, L); tau = tau_c(Wt, P) if tau is None else tau + G, m, kmin, rmax = T.G, T.m, min(T.K), max(P) + theta = log(rmax) / log(kmin) if rmax > 1 else 0.0 + N = {(0, 1): 1} + src_w, src_phi, ex_w, ex_phi, units, bad = 0, 0.0, 0, 0.0, 0, [] + src_sizes, ex_sizes = set(), {} + # root + for b, x in T.demand(0, 1).items(): + s = T.c(b) + if T.inR(b, 1): bad.append(('root demand inside R(1)', b)) + if not (L / m < s <= L): bad.append(('root source size', s)) + src_w += x; src_phi += x * s ** tau; src_sizes.add(s) + for d in range(0, G + 1): + layer = {k: v for k, v in N.items() if k[0] == d} + for (_, rho), n in layer.items(): + us = T.units(d, rho) + units += n * sum(us.values()) + if d == G: # generation 0: exits + for a, ua in us.items(): + assert a == tuple(0 for _ in T.K) + for r, pr in P.items(): + e = rho * r + ex_w += n * pr * ua; ex_phi += n * pr * ua * e ** tau + ex_sizes[e] = ex_sizes.get(e, 0) + n * pr * ua + continue + for r, pr in P.items(): # children via a round of rank r + rc = rho * r + N[(d + 1, rc)] = N.get((d + 1, rc), 0) + n * pr + need = T.demand(d + 1, rc) + supply = {a: ua for a, ua in us.items()} # parent round output at point a, size rc*c(a) + for b in set(need) | set(supply): + sup = supply.get(b, 0); dem = need.get(b, 0) + if T.inR(b, rho): + if sup != dem: bad.append(('unbalanced', d, rho, r, b, sup, dem)) + else: + if sup: bad.append(('supply outside R', b)) + s = rc * T.c(b) + if dem and not (r * L / m < s <= L): bad.append(('source size', s, r)) + src_w += n * pr * dem; src_phi += n * pr * dem * s ** tau + if dem: src_sizes.add(s) + emax = max(ex_sizes) + bound = rmax * (L / m) ** theta if rmax > 1 else 1 + ubound = src_phi / (sum(Wt.values()) * kmin ** tau * (1 - kmin ** -tau)) + return dict(L=L, G=G, tau=tau, unbalanced_or_bad=len(bad), bad=bad[:3], sources=src_w, Phi_src=src_phi, + exits=ex_w, Phi_exit=ex_phi, Phi_ratio=ex_phi / src_phi, src_size_range=(min(src_sizes), max(src_sizes)), + exit_max=emax, exit_bound=bound, units=units, unit_bound=ubound, classes=sum(N.values()), + ex_sizes=ex_sizes, src_sizes=sorted(src_sizes)) + +def lockstep_literal(Wt, P_list, L): + """Explicit recursion over round sequences (P_list = ranks of rounds 1..P in word order).""" + Pd = {} + for r in P_list: Pd[r] = Pd.get(r, 0) + 1 + T = Tree(Wt, Pd, L); G = T.G + st = dict(classes=0, src=0, exits={}, issued_before_start=True) + def process(path, rho, fluid): + d = len(path); st['classes'] += 1 + us = T.units(d, rho) + need = T.demand(d, rho) + # fluid = parent's round output (points in R(parent rho)); top it up with sources, then it must equal need + for b, x in need.items(): + have = fluid.get(b, 0) + if have > x: raise AssertionError(('surplus', path, b, have, x)) + if have < x: st['src'] += x - have # source from the top split (always available) + for b in fluid: + if b not in need and fluid[b]: raise AssertionError(('unconsumed', path, b)) + for j, r in enumerate(P_list): # rounds in word order; round j+1 only after round j completes + out = dict(us) # one job of rank r per unit, at point a, size rho*r*c(a) + if d == G: + for a, ua in out.items(): + e = rho * r; st['exits'][e] = st['exits'].get(e, 0) + ua # handled by a new top call Do(e) + else: + process(path + (j,), rho * r, out) + process((), 1, {}) + return st, T + +if __name__ == "__main__": + rules = [("A: targets {4:1,3:2}, rounds [1,1,1,1,2,2]", {4: 1, 3: 2}, [1, 1, 1, 1, 2, 2]), + ("B: pure {7:2}+idle 3 -> targets {7:1,4:1}, rounds [1,1,1,1,2,2,2]", {7: 1, 4: 1}, [1, 1, 1, 1, 2, 2, 2]), + ("C: targets {5:1,4:3}, rounds [1]*6+[2]*2+[3]*2", {5: 1, 4: 3}, [1] * 6 + [2] * 2 + [3] * 2)] + print("(A) literal lockstep (explicit round sequences):", flush=True) + for name, Wt, rl in rules: + for L in (40, 150): + Pd = {} + for r in rl: Pd[r] = Pd.get(r, 0) + 1 + ref = check(Wt, Pd, L) + st, T = lockstep_literal(Wt, rl, L) + ok = (st['src'] == ref['sources'] and st['exits'] == ref['ex_sizes']) + print(f" {name}, L={L}: G={T.G}, classes {st['classes']}, every class exactly fed, sources {st['src']} " + f"(= merged count: {ok}), exits by size {dict(sorted(st['exits'].items()))}", flush=True) + print("(B) merged checks at larger L:", flush=True) + for name, Wt, rl in rules: + Pd = {} + for r in rl: Pd[r] = Pd.get(r, 0) + 1 + for L in (1000, 10 ** 5, 10 ** 7): + ch = check(Wt, Pd, L) + print(f" {name}, L={L}: tau_c={ch['tau']:.6f} G={ch['G']} classes={ch['classes']} bad={ch['unbalanced_or_bad']} " + f"sources in {ch['src_size_range']} (L/m={L/max(Wt):.1f}); Phi_exit/Phi_src={ch['Phi_ratio']:.12f}; " + f"max exit {ch['exit_max']} <= bound {ch['exit_bound']:.1f}; units {float(ch['units']):.4g} <= " + f"bound {ch['unit_bound']:.4g}", flush=True) diff --git a/research/direct-mixed-flow/verify.py b/research/direct-mixed-flow/verify.py new file mode 100644 index 0000000000..df9ca12ad0 --- /dev/null +++ b/research/direct-mixed-flow/verify.py @@ -0,0 +1,274 @@ +#!/usr/bin/env python3 +"""Partial direct compiler, nested integer batches and exact size controls. + +The near-root direct exponent theorem remains open. No floating-point result +is used by this verifier. zxv with OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha1, sha256 +import json +import gzip +from pathlib import Path + +HERE = Path(__file__).resolve().parent + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def source(path): + env = {'__file__': str(path), '__name__': 'pinned_or_local_library'} + exec(compile(path.read_bytes(), str(path), 'exec'), env) + return env + + +FLOW = source(HERE/'flow.py') +Flow = FLOW['Flow'] + + +def authenticate(): + result = {} + prefix = Path('research/direct-mixed-flow/vendor') + for row in json.loads((HERE/'VENDOR.json').read_text())['files']: + raw = (HERE/'vendor'/Path(row['path']).relative_to(prefix)).read_bytes() + digest = sha256(raw).hexdigest() + need(digest == row['sha256'], 'changed source: '+row['path']) + need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() + == row['git_blob'], 'changed Git source blob') + result[row['path']] = digest + return result + + +def bigint_record(n): + return {'bits': n.bit_length(), + 'unsigned_big_endian_sha256': sha256(n.to_bytes((n.bit_length()+7)//8, 'big')).hexdigest()} + + +def ratio_interval(n, d): + scale = 10**18 + low = n*scale//d + return {'lower': str(Q(low, scale)), 'upper': str(Q(low+1, scale))} + + +def compile_counts(targets, paid, maximum, force_unit_replication=False): + m, W, calls = max(targets), sum(targets.values()), sum(paid.values()) + surplus = sum(k*v for k, v in targets.items())-sum(k*v for k, v in paid.items()) + need(surplus > 0, 'positive raw rank-one surplus') + widths = [1]*(maximum+1) + leaves = list(range(maximum+1)) + units = [0]*(maximum+1) + columns = [0]*(maximum+1) + slots = [0]*(maximum+1) + largest_sources = 1 + for n in range(m, maximum+1): + f = Flow(targets, paid, n).merged() + a = 1 if force_unit_replication else widths[n-1] + widths[n] = a*f['source_count'] + leaves[n] = 0 + units[n] = a*f['units'] + columns[n] = a*f['column_mass'] + slots[n] = a*(f['source_count']+sum(f['exits'].values())+(W+calls)*f['units']) + for histogram, complement in [(f['sources'], True), (f['exits'], False)]: + for rank, count in histogram.items(): + e = n-rank if complement else rank + need(0 <= e < n, 'all recursive ranks strictly decrease') + need(a % widths[e] == 0, 'whole integer subprogram batches') + copies = count*(a//widths[e]) + for records in (leaves, units, columns, slots): + records[n] += copies*records[e] + need(widths[n] % widths[n-1] == 0, 'nested divisibility') + need(widths[n]*n-leaves[n] == surplus*columns[n], 'whole-word rank-one identity') + need(units[n] <= columns[n] <= widths[n]*n//surplus, 'owned-unit upper bound') + need(slots[n] <= 2*(W+calls)*units[n], 'all compiler routing slots counted') + largest_sources = max(largest_sources, f['source_count']) + f = Flow(targets, paid, maximum).merged() + Cmax = W*(W+calls+1)**(f['height']+1) + need(largest_sources <= Cmax and widths[maximum] <= Cmax**maximum, + 'single-exponential width envelope') + n = maximum + return {'n': n, 'productive_width': bigint_record(widths[n]), + 'paid_rank_one_leaves': bigint_record(leaves[n]), + 'raw_instances': bigint_record(units[n]), + 'column_mass': bigint_record(columns[n]), + 'routing_slots': bigint_record(slots[n]), + 'leaves_per_array': ratio_interval(leaves[n], widths[n]), + 'width_exponent_envelope': Cmax.bit_length()*n, + 'source_count_upper': Cmax, 'rank_one_surplus': surplus, + 'paid_above_99_percent_linear': leaves[n] > 99*widths[n]*n//100, + 'nested_batch_checks': maximum-m+1}, (widths, leaves, units, columns, slots) + + +def finite_flows(): + rules = [ + ('separated-control', {3:2, 4:1}, {1:4, 2:2}, [1,1,1,1,2,2]), + ('strict-overlap', {2:1, 5:1}, {1:2, 4:1}, [1,1,4]), + ('source-open-equality', {2:4, 3:1}, {1:6, 2:2}, [1]*6+[2]*2), + ] + old = source(HERE/'vendor/tree_flow.py') + rows = [] + for label, targets, paid, word in rules: + for n in (20, 40, 80): + f = Flow(targets, paid, n) + merged, literal = f.merged(), f.literal(word) + need(merged['sources'] == literal['sources'] and merged['exits'] == literal['exits'], + 'literal and merged whole-job flow agree') + if label == 'separated-control': + predecessor, _ = old['lockstep_literal'](targets, word, n) + need(merged['source_count'] == predecessor['src'] and + merged['exits'] == predecessor['exits'], 'unchanged separated predecessor') + need(not merged['boundary_exits'], 'separated case has no premature exits') + rows.append({'rule': label, 'targets': targets, 'paid': paid, + 'flow': merged, 'literal_classes': literal['classes']}) + strict = Flow({2:1, 5:1}, {1:2, 4:1}, 20).merged() + mass = lambda h: sum(k*v for k, v in h.items()) + without_boundary = strict['exits']-strict['boundary_exits'] + need(strict['boundary_exits'] and + mass(strict['sources'])-mass(without_boundary) > + strict['rank_one_surplus']*strict['column_mass'], 'omitted boundary exits undercharge') + return rows + + +def inherited_rank_size_bound(): + old = json.loads((HERE/'vendor/higher-moment-RESULT.json').read_text()) + p7 = json.loads((HERE/'vendor/p7-RESULT.json').read_text())['strictification'] + T = {int(k): v for k, v in p7['targets'].items()} + P = {int(k): v for k, v in p7['paid'].items()} + v = old['strictification']['tensor_power'] + H = old['uniform_rank']['H'] + need((v, H) == (150, 349300000000), 'unchanged sufficient ambient rank') + W = sum(T.values())**v + paid_mass_upper = sum(k*n for k, n in P.items())**v+W*15**v + need(W < 2**1950, 'productive field exponent envelope') + need(paid_mass_upper < 2**2701 and W+paid_mass_upper+1 < 2**2702, + 'every padded/split paid call counted by its positive rank mass') + D = 1950+2702*(H+1) + need(sum(k*n for k, n in T.items())-sum(k*n for k, n in P.items()) == 608, + 'underlying raw p7 rank-one surplus') + native_bytes = gzip.decompress((HERE/'vendor/THREE-base-FULL-IDENTITY-NATIVE.json.gz').read_bytes()) + native = json.loads(native_bytes) + factor_bytes = (HERE/'vendor/P7-FACTOR.json').read_bytes() + factor = json.loads(factor_bytes) + need(sha256(factor_bytes).hexdigest() == p7['native_inventory']['factor_receipt_sha256'], + 'actual p7 factor receipt') + need(set(native) == {'forward', 'backward'} and + all(len(w) == 22633 for w in native.values()), 'actual raw native record counts') + # Macro description allowance: 15 exact local words, both serialized + # orientations as an overcount, literal controller, source scalar + # allowance, every productive/paid/contact/helper/idle slot, with 32 + # records per extra routing/ownership slot and literal payload bits. + ni = p7['native_inventory'] + slots = (ni['productive_fields']+ni['paid_calls']+ni['contacts']+ + ni['fresh_helper_fields']+ni['main_fields']+sum(ni['whole_idle_profile'].values())) + raw_allowance = (15*8*len(native_bytes)+8*len(factor_bytes)+ + 32*(ni['scalar_allowance']+slots+15*max(map(len,native.values())))) + need(raw_allowance < 2**40, 'complete raw macro/serialized-input allowance') + W0, P0 = sum(T.values()), sum(P.values()) + Uproduct = sum(W0**(v-1-i)*P0**i for i in range(v)) + need(Uproduct < 2**2392, 'chronological product raw-instance count') + strict_surplus = (sum(k*n for k,n in T.items())**v- + sum(k*n for k,n in P.items())**v) + need(strict_surplus > 0 and strict_surplus % 608 == 0 + and strict_surplus//608 >= Uproduct, 'expanded product raw-column identity') + product_allowance = (2**40+32*v*(W0+P0+1))*Uproduct+32*v*P0**v + completed_allowance = product_allowance+32*(paid_mass_upper+W+P0**v) + # Include each dense binary chart/quadratic phase descriptor and role + # indices in the fixed completed-unit allowance, not just opcodes. + ambient = 121**v + serialized_unit_upper = completed_allowance*64*ambient**2 + need(serialized_unit_upper < 2**5000, 'fixed completed-unit description allowance') + need(2**5000+32*(W+paid_mass_upper)+1 < 2**5001, 'compiled record coefficient') + need(2*D*(H+1) > 7*H+30049, 'explicit closure exponent absorption') + return {'kappa': old['kappa'], 'H': H, 'N': '2^'+str(H), 'D': D, + 'width_bound': 'B_N < 2^(D * 2^H)', + 'paid_leaf_bound': 'P_N < B_N * 2^H', + 'raw_p7_instance_bound': 'U_raw <= (B_N * 2^H - P_N)/608', + 'owned_p7_center_bound': 'one per raw instance; <= B_N * 2^H / 608', + 'routing_macro_record_bound': + 'R <= (A + 32*(W+P) + 1) * B_N * N; A < 2^5000', + 'raw_native_record_counts': {k:len(w) for k,w in native.items()}, + 'raw_macro_and_payload_allowance': raw_allowance, + 'raw_macro_allowance_upper': '2^40', + 'completed_unit_description_upper': '2^5000', + 'compiled_record_upper': 'R < 2^(D*2^H + H + 5001)', + 'source_precision_E_upper': 'E < 2^(3*D*2^H + 3*H + 15021)', + 'source_C0_upper': 'C0 < 2^(8*D*2^H)', + 'routing_slot_bound': 'slots <= 2*(W+P)*V, V completed-unit instances', + 'physical_scope': 'Encoded whole-job adapter/move records. Their permitted physical implementation and tariffs remain inherited, separately priced premises.', + 'winning_uniform_word_materialized': False} + + +def verify(): + inputs = authenticate() + flows = finite_flows() + toy = [] + for T, P in [({2:1, 5:1}, {1:2, 4:1}), ({2:4, 3:1}, {1:6, 2:2})]: + row, _ = compile_counts(T, P, 100) + toy.append(row) + p7 = json.loads((HERE/'vendor/p7-RESULT.json').read_text())['strictification'] + T, P = ({int(k): v for k, v in p7[key].items()} for key in ('targets', 'paid')) + direct, counts = compile_counts(T, P, 1000) + B, paid = counts[0][1000], counts[1][1000] + need(paid > 990*B, 'exact direct rank-1000 saving is below target') + kappa = Q('0.00268647') + # ln(2)>2/3 by its first atanh term. 1000>2^9 implies ln(1000)>6. + # exp(x)>1+x then gives 1000^kappa > 1+6*kappa > 100/99. + need(1000 > 2**9 and 1+6*kappa > Q(100,99), 'exact target comparison') + direct['target_failure'] = {'kappa': str(kappa), + 'proved': 'L(1000) > 990 > 1000^(1-kappa)', + 'scope': 'This particular finite rank fails; no asymptotic impossibility claim.'} + rejected = [] + try: + compile_counts({2:1, 5:1}, {1:2, 4:1}, 10, force_unit_replication=True) + except ValueError as e: + need(str(e) == 'whole integer subprogram batches', 'correct missing-batch rejection') + rejected.append(str(e)) + else: + raise ValueError('unit-replication mutant accepted') + try: + Flow({2:1, 5:1}, {1:1, 5:1}, 20) + except ValueError as e: + need(str(e) == 'finite direct-flow rank contract', 'nondecreasing exit rejected') + rejected.append(str(e)) + else: + raise ValueError('nondecreasing-exit mutant accepted') + return {'schema': 'partial-direct-mixed-flow-and-finite-size/1', + 'status': 'PASS_PARTIAL_DIRECT_FLOW_AND_SIZE_BOUNDS', + 'direct_exponent_theorem_established': False, + 'finite_flows': flows, 'exact_toy_compilations': toy, + 'exact_p7_direct_compilation': direct, + 'existing_supplier_size_bounds': inherited_rank_size_bound(), + 'rejected_mutations': rejected, 'source_sha256': inputs, + 'new_code_sha256': {f: sha256((HERE/f).read_bytes()).hexdigest() + for f in ('flow.py', 'verify.py')}, + 'scope': 'New finite matching/scheduling and batching/size bounds. The direct near-root exponent is open. Existing conditional endpoint and native/physical hypotheses remain inherited; no new kappa.'} + + +def normalize(x): + if isinstance(x, dict): + return {str(k): normalize(v) for k, v in x.items()} + if isinstance(x, (list, tuple)): + return [normalize(v) for v in x] + return x + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--out', type=Path) + args = parser.parse_args() + result = normalize(verify()) + if args.out: + need(not args.out.exists(), 'new output path required') + args.out.write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + need(json.loads((HERE/'RESULT.json').read_text()) == result, 'changed saved receipt') + print(json.dumps({'status': result['status'], 'direct_exponent_theorem': False, + 'p7_width_bits_at_1000': result['exact_p7_direct_compilation']['productive_width']['bits'], + 'target_failure': result['exact_p7_direct_compilation']['target_failure']['proved']})) + + +if __name__ == '__main__': + main()