diff --git a/research/chronological-dirty-intervals/CERTIFICATE.json b/research/chronological-dirty-intervals/CERTIFICATE.json new file mode 100644 index 0000000000..8334ad41e7 --- /dev/null +++ b/research/chronological-dirty-intervals/CERTIFICATE.json @@ -0,0 +1,496 @@ +{ + "claim": "finite corroboration of the scoped written sharp-envelope proof", + "controls": [ + "adjacent_source_bits", + "reciprocal_scratch_entries", + "oversized_prefix_entry", + "factor_count_0", + "factor_count_65", + "invalid_sign", + "invalid_height", + "inverse_direction_is_essential", + "wrong_inverse_order", + "changed_leaf_sign", + "factor_order_retained", + "repeated_factor_retained" + ], + "intervals": { + "both_orientations_nonempty_intervals": 89528, + "cases": [ + { + "bound": 2, + "h": 0, + "maximum": 2, + "n": 1 + }, + { + "bound": 3, + "h": 1, + "maximum": 3, + "n": 2 + }, + { + "bound": 6, + "h": 2, + "maximum": 4, + "n": 3 + }, + { + "bound": 9, + "h": 3, + "maximum": 7, + "n": 5 + }, + { + "bound": 9, + "h": 3, + "maximum": 9, + "n": 8 + }, + { + "bound": 14, + "h": 4, + "maximum": 10, + "n": 11 + }, + { + "bound": 14, + "h": 4, + "maximum": 14, + "n": 16 + } + ] + }, + "literal_witnesses": [ + { + "cuts": [ + 0, + 2 + ], + "h": 1, + "n": 2, + "target_row": [ + 1, + 1, + 1 + ] + }, + { + "cuts": [ + 2, + 6 + ], + "h": 2, + "n": 4, + "target_row": [ + -2, + 1, + -1, + 2 + ] + }, + { + "cuts": [ + 9, + 22 + ], + "h": 3, + "n": 8, + "target_row": [ + 2, + 1, + 1, + -2, + 3 + ] + }, + { + "cuts": [ + 38, + 86 + ], + "h": 4, + "n": 16, + "target_row": [ + -3, + 1, + -1, + 2, + -3, + 4 + ] + }, + { + "cuts": [ + 153, + 342 + ], + "h": 5, + "n": 32, + "target_row": [ + 3, + 1, + 1, + -2, + 3, + -4, + 5 + ] + }, + { + "cuts": [ + 614, + 1366 + ], + "h": 6, + "n": 64, + "target_row": [ + -4, + 1, + -1, + 2, + -3, + 4, + -5, + 6 + ] + } + ], + "phase_formulas": { + "all_child_cuts_n": [ + 2, + 3, + 4, + 5 + ], + "both_orders_identity_checks": { + "01": 338, + "02": 266, + "03": 338, + "12": 338, + "13": 500, + "23": 338 + }, + "five_child_cuts_n": [ + 8, + 11, + 16 + ] + }, + "prefixes": { + "factor_counts": [ + 1, + 64 + ], + "maximum_inverse_scratch_mass_by_height": { + "0": 0, + "1": 2, + "2": 4, + "3": 8, + "4": 12, + "5": 18, + "6": 24 + }, + "positive_prefix_boundaries": 95735, + "sampled_inverse_identities": 317 + }, + "scalar_witnesses": { + "controls": [ + "false_linear_bound", + "sharp_bound_minus_one", + "wrong_product_order" + ], + "exact_integer_witnesses": [ + { + "cuts": [ + 0, + 2 + ], + "h": 1, + "n": 2, + "norm": 3 + }, + { + "cuts": [ + 2, + 6 + ], + "h": 2, + "n": 4, + "norm": 6 + }, + { + "cuts": [ + 9, + 22 + ], + "h": 3, + "n": 8, + "norm": 9 + }, + { + "cuts": [ + 38, + 86 + ], + "h": 4, + "n": 16, + "norm": 14 + }, + { + "cuts": [ + 153, + 342 + ], + "h": 5, + "n": 32, + "norm": 19 + }, + { + "cuts": [ + 614, + 1366 + ], + "h": 6, + "n": 64, + "norm": 26 + }, + { + "cuts": [ + 2457, + 5462 + ], + "h": 7, + "n": 128, + "norm": 33 + }, + { + "cuts": [ + 9830, + 21846 + ], + "h": 8, + "n": 256, + "norm": 42 + }, + { + "cuts": [ + 39321, + 87382 + ], + "h": 9, + "n": 512, + "norm": 51 + }, + { + "cuts": [ + 157286, + 349526 + ], + "h": 10, + "n": 1024, + "norm": 62 + }, + { + "cuts": [ + 629145, + 1398102 + ], + "h": 11, + "n": 2048, + "norm": 73 + }, + { + "cuts": [ + 2516582, + 5592406 + ], + "h": 12, + "n": 4096, + "norm": 86 + }, + { + "cuts": [ + 10066329, + 22369622 + ], + "h": 13, + "n": 8192, + "norm": 99 + }, + { + "cuts": [ + 40265318, + 89478486 + ], + "h": 14, + "n": 16384, + "norm": 114 + }, + { + "cuts": [ + 161061273, + 357913942 + ], + "h": 15, + "n": 32768, + "norm": 129 + }, + { + "cuts": [ + 644245094, + 1431655766 + ], + "h": 16, + "n": 65536, + "norm": 146 + }, + { + "cuts": [ + 2576980377, + 5726623062 + ], + "h": 17, + "n": 131072, + "norm": 163 + }, + { + "cuts": [ + 10307921510, + 22906492246 + ], + "h": 18, + "n": 262144, + "norm": 182 + }, + { + "cuts": [ + 41231686041, + 91625968982 + ], + "h": 19, + "n": 524288, + "norm": 201 + }, + { + "cuts": [ + 164926744166, + 366503875926 + ], + "h": 20, + "n": 1048576, + "norm": 222 + }, + { + "cuts": [ + 659706976665, + 1466015503702 + ], + "h": 21, + "n": 2097152, + "norm": 243 + }, + { + "cuts": [ + 2638827906662, + 5864062014806 + ], + "h": 22, + "n": 4194304, + "norm": 266 + }, + { + "cuts": [ + 10555311626649, + 23456248059222 + ], + "h": 23, + "n": 8388608, + "norm": 289 + }, + { + "cuts": [ + 42221246506598, + 93824992236886 + ], + "h": 24, + "n": 16777216, + "norm": 314 + }, + { + "cuts": [ + 168884986026393, + 375299968947542 + ], + "h": 25, + "n": 33554432, + "norm": 339 + }, + { + "cuts": [ + 675539944105574, + 1501199875790166 + ], + "h": 26, + "n": 67108864, + "norm": 366 + }, + { + "cuts": [ + 2702159776422297, + 6004799503160662 + ], + "h": 27, + "n": 134217728, + "norm": 393 + }, + { + "cuts": [ + 10808639105689190, + 24019198012642646 + ], + "h": 28, + "n": 268435456, + "norm": 422 + }, + { + "cuts": [ + 43234556422756761, + 96076792050570582 + ], + "h": 29, + "n": 536870912, + "norm": 451 + }, + { + "cuts": [ + 172938225691027046, + 384307168202282326 + ], + "h": 30, + "n": 1073741824, + "norm": 482 + }, + { + "cuts": [ + 691752902764108185, + 1537228672809129302 + ], + "h": 31, + "n": 2147483648, + "norm": 513 + }, + { + "cuts": [ + 2767011611056432742, + 6148914691236517206 + ], + "h": 32, + "n": 4294967296, + "norm": 546 + } + ], + "method": "compressed four-phase prefixes plus rational Gauss-Jordan inverse" + }, + "schema_version": 1 +} diff --git a/research/chronological-dirty-intervals/PROOF.md b/research/chronological-dirty-intervals/PROOF.md new file mode 100644 index 0000000000..e2e7352d4a --- /dev/null +++ b/research/chronological-dirty-intervals/PROOF.md @@ -0,0 +1,269 @@ +# The sharp joint interval envelope for the balanced dirty word + +Prepared for @CubeJerry with substantial OpenAI Codex assistance. +Apache-2.0. This is a scoped written proof, conditional on the precisely +identified predecessor lemmas below; it is not a supplier-admission proof. + +## Contract and result + +Use Chafik Boukhalfa's unchanged #628 balanced word on n >= 1 formal +noncommuting factors. There is a protected source x, an unread target y, +and h = ceil(log2 n) distinct dirty scratch registers z1,...,zh, one per +depth. Siblings reuse the same deeper scratch. Every cut is at a complete +ideal leaf, `target += sign A_j source`. + +For a matrix over the free noncommutative integer algebra, its coefficient +row mass is the sum of the absolute integer coefficients of all monomials +in that row, after collecting equal words. Define + +```text +F(0) = 2, +F(h) = floor(h^2/2) + h + 2, h >= 1. +``` + +For every ordered pair of cuts s,t in either word orientation, every row +of `P_t P_s^-1` has mass at most F(h). This is the sharp uniform envelope +at each height: Arham Tahir's #1374 family at n=2^h attains F(h), including +with commuting real scalar factors in {+1,-1}. At h=0 one leaf attains two. +Sharpness is over all n at a fixed height, not a claim that every n attains it. + +Consequently the maximum joint-register operator norm is at most F(h) for +arbitrary contractive factors, without commutation. It is at most F(h) G +when factors commute and every subset product, including the empty product, +has norm at most G >= 1. The latter implication uses #1278's squarefree +interval theorem. The contraction implication does not require it. + +The predecessor upper envelope was h^2+2h+3 for h>=1 (Nick Petalas, +#5872); the new gain is ceil(h^2/2)+h+1. #1374 already supplied both the +matching lower family and the explicit sharp-constant question. The new +content here is the upper proof, specifically the inverse-prefix sparsity +invariant and its use in chronological phase products. + +## Imported premises and notation + +Hanson Sun's #1085 proves that every prefix and inverse prefix, for both +orientations, has entries zero or one signed monomial; its source row and +target column are identity. For a positive call of complete product T, +the target/source coefficient of a prefix is 0 or T, and that of its +inverse is 0 or -T. A suffix has the same entry-size bound, because it is +the inverse of a prefix of the inverse word. Each such child row has mass +at most its number of registers. We use these assertions as written premises. + +Write B for the ordered left product, A for the ordered right product, +and z for the parent's first scratch. The completed child maps are + +```text +U = I + e_z B e_x^T, V = I + e_y A e_z^T, +F = V^-1 U^-1 V U = I + e_y AB e_x^T. +``` + +Let P_a be a positive prefix of the left child and Q_b a positive prefix +of the right child. They act on the same deeper scratch W. #1278's four +positive-parent phase formulas are + +```text +0: P_a; 1: Q_b U; 2: P_a U^-1 V U; 3: Q_b F. +``` + +At a child boundary either adjacent representation gives the same map. +The last representation includes the final boundary. Negative prefixes +have the same maps after complementary cuts and full-map multiplication. +All algebra below uses matrix action on column vectors, with chronological +execution multiplying on the left. No factor commutation is used. + +## Lemma 1: scratch support has at most one direction per pair + +For every positive prefix and its inverse, each scratch diagonal entry is +one, and for every pair of distinct scratch registers at most one of the +two opposite off-diagonal entries is nonzero. + +Induct on the call. Completed outer maps only change z by a multiple of x +or y by a combination of x,z. Their left or right multiplication does not +change the scratch-to-scratch block of the active child, in any of the four +phase formulas or their inverses. For a left child z is its unread target: +its column in this block is the identity column. For a right child z is +its protected source: its row in this block is the identity row. The block +on W satisfies the induction hypothesis. Thus z cannot participate in +both directions of any pair, nor can any pair inside W. Its diagonal and +the deeper diagonals are one. This also proves the claim for an unused +reserved depth, whose row and column are identity. The leaf case is empty. + +In particular, with k scratch registers the scratch-to-scratch block has +coefficient mass at most k(k+1)/2. #1085's unit entry-size premise is used +here: counting occupied entries is then counting their coefficient mass. + +## Lemma 2: inverse-positive-prefix source occupancy is nonadjacent + +For an inverse of a positive prefix, record which entries in its source +column are nonzero, in row order `(target,z1,...,zk)`. This binary string +has no consecutive ones. The leaf strings have length one, so the claim +holds initially. + +For an active left child, let f in {0,1} indicate its inverse-prefix +target/source entry, which is `-f B`; let v be its deeper source-occupancy +string. Its induction string is `(f,v)`. Inverting the four phase formulas +gives the following parent strings: + +| Phase | Inverse-parent source occupancy `(y,z,W)` | +| --- | --- | +| 0 | `(0,f,v)` | +| 1 | `(0,1,0,...,0)` | +| 2 | `(1-f,f,v)` | +| 3 | `(1,0,...,0)` | + +For phase 1, `U^-1 Q_b^-1 e_x = e_x-e_z B`, because x is external +to the right child. For phase 3, `F^-1 Q_b^-1 e_x = e_x-e_y AB`. +For phase 2, applying `U^-1 V^-1 U` to `P_a^-1 e_x` leaves the z +coefficient `-f B`, changes the y coefficient to `-(1-f)AB`, and leaves +the W coefficients unchanged. These are exact free-algebra identities. +Since `(1-f)f=0`, all four strings remain nonadjacent. Padding unused +deepest registers adds zero bits, so unequal child sizes cause no exception. + +There are therefore at most ceil(k/2) occupied source entries among the k +scratch rows. Their target entries vanish. Lemma 1 now gives the new bound + +```text +H(k) := k(k+1)/2 + ceil(k/2) = floor((k+1)^2/2) +``` + +on the *sum of the masses of all scratch rows* of an inverse-positive +prefix. For k=0 this is zero. Left multiplication by the full positive +map changes only the child's target row. Hence a positive suffix +`U P_a^-1` or `V Q_a^-1` has the same scratch rows and the same H(k) bound. + +## Lemma 3: cross-child products with the correct right factor + +Embed a left-child map L on `(x,z,W)` and a right-child map R on `(z,y,W)`; +there are k shared scratch registers W. Every entry has mass at most one. +Assume that the rightmost factor in a product is either an inverse-positive +prefix or a positive suffix, so its W-row mass sum is at most H(k). +All its rows have mass at most k+2. + +For R L, the y row is the sum of its own identity row, at most one copy of +L's z row, and at most one monomial multiple of each W row of L. Its mass +is at most `1+(k+2)+H(k)`. A W row is bounded by `(k+2)+H(k)`; the z row +is L's z row, and x is fixed. Thus every row of R L is bounded by + +```text +H(k)+k+3 = F(k+1). +``` + +For L R, the z row is at most one x term, the unchanged z row, and the +weighted sum of W rows of R: mass at most `H(k)+2`. A W row has at most +one x term plus that W-row sum; the y row is unchanged from R. Thus its +maximum row mass is at most `max(H(k)+2,k+2) <= F(k+1)`. +The products use shared W throughout; no fresh scratch is introduced. + +## All six phase pairs, both cut orders + +Induct on n, keeping both cut orders. Both children have height at most +h-1; pad them to k=h-1 shared scratch registers as needed. Lemma 2 holds +with this padding. Same-phase intervals reduce to child intervals, including +the reversed order, and are bounded by F(h-1) <= F(h). + +For distinct phases, the three adjacent pairs and their inverses are: + +| Pair | Forward interval | Reverse interval | +| --- | --- | --- | +| 0,1 | `Q_b (U P_a^-1)` | `(P_a U^-1) Q_b^-1` | +| 1,2 | `(P_b U^-1) (V Q_a^-1)` | `(Q_a V^-1) (U P_b^-1)` | +| 2,3 | `(Q_b V^-1) P_a^-1` | `P_a (V Q_b^-1)` | + +Every factor is a child prefix, inverse prefix or suffix. In each product +the rightmost factor is specifically an inverse-positive prefix or positive +suffix. Lemma 3 applies and gives F(h). This chronological restriction is +the point that the generic product of two arbitrary prefix bounds misses. + +For repeated left phases, #1278 gives + +```text +I_02 = P_b P_a^-1 + e_y A [e_z^T U P_a^-1]. +``` + +The added row is external to the child. Its mass including its identity +entry is at most `1+(k+2)=h+2`; the other rows are child-interval rows. +For the inverse interchange a,b and negate the added term. Thus both orders +are bounded by `max(F(h-1),h+2) <= F(h)`. + +For repeated right phases, + +```text +I_13 = Q_b Q_a^-1 - [(Q_b V^-1)e_z] B e_x^T. +``` + +The new column x is external to the child. Its contribution to each row has +mass at most one, by the prefix entry-size premise for `Q_b V^-1`. +The reverse formula interchanges a,b and changes minus to plus. Hence both +orders are bounded by `F(h-1)+1 <= F(h)`, also at h=1. + +The final pair is + +```text +I_03 = Q_b P_a^-1 + e_y AB e_x^T, +I_03^-1 = P_a Q_b^-1 - e_y AB e_x^T. +``` + +For the forward direction, only the y row requires a refinement to Lemma 3. +Write `Q_b[y,z]=e A` and `P_a^-1[z,x]=-f B`, e,f in {0,1}. +If e=0, the target row has mass at most `H(k)+2` (its identity, the W-row +sum, and the added AB). If e=1, combine the added AB with the z-row +contribution before applying the triangle inequality. Its x entry is +`(1-f)AB`; its other entries are unchanged from A times the z row. The +combined row has mass at most k+2: when f=1 the x terms cancel, and when +f=0 the original z-row x entry was absent, leaving at most k+1 other +entries before the one addition. The y row is therefore bounded by +`1+H(k)+(k+2)=F(h)`. Other rows already obey Lemma 3. + +For the reverse direction, Lemma 3 bounds the z and W rows of +`P_a Q_b^-1`; the extra term changes only the external y row. That row +is the y row of Q_b^-1 plus one x entry, of mass at most `k+3=h+2`. +This too is at most F(h). + +The n=1 base consists only of identity and the single leaf shear in either +sign and has envelope two. This completes the induction for positive words +and both cut orders. An interval of the negative word is a positive-word +interval at the complementary cuts in the opposite order, so both word +orientations follow. The proof never expands a rounded leaf internally. + +## Sharpness and operator substitution + +#1374's pinned lower theorem uses n=2^h, scalar factors all +1 except +`A_(n-2^j-1)=-1` for 0<=j<=h-2, and chronological cuts + +```text +a_h = floor(3*4^(h-1)/5), b_h = (4^h+2)/3. +``` + +Its target row is exactly + +```text +y + (-1)^(h-1)(1+floor(h/2)) x + + sum_(j=1..h) j*(-1)^(h+j) z_j. +``` + +The absolute row sum is F(h). This predecessor theorem supplies all-height +attainment; our verifier independently corroborates that target row by +literal replay at small sizes and compressed exact scalar prefix matrices +at larger heights. No priority is claimed for the lower family or the old +n<=16 maximum census. + +For arbitrary contractive factors every formal word evaluates to an operator +of norm at most one, so coefficient row mass bounds the maximum joint norm. +For commuting factors with all subset products bounded by G, first invoke +#1278's squarefree conclusion in the free algebra, then commute each +surviving word into a subset product and apply the triangle inequality. +Bounding individual factors by G alone is not sufficient. Sharpness of the +coefficient envelope and contraction-domain envelope does not claim equality +F(h)G for every fixed nonminimal choice of G. + +## Trust boundary + +The all-size conclusion is the written induction using #1085 and #1278 +as stated premises, and #1374 for sharpness. Exact finite checks corroborate +the new invariants, six phase identities, interval bounds and scalar witnesses; +they are not the basis for extrapolation. Formal proof-kernel verification +and independent human review are unclaimed. This theorem concerns arbitrary +joint disturbances; Philippe Van Velzen's separate destination-only #2177 +result is unchanged. Internal rounding, inverse-leaf preimages, precision, +physical movement, compiler, stock, analytic recovery and a complete caller +invoice remain outside scope. No selected framework assumption or kappa changes. diff --git a/research/chronological-dirty-intervals/README.md b/research/chronological-dirty-intervals/README.md new file mode 100644 index 0000000000..d9b23d69fb --- /dev/null +++ b/research/chronological-dirty-intervals/README.md @@ -0,0 +1,170 @@ +# Sharp joint interval transport for the balanced dirty word + +**Scoped written theorem with exact finite corroboration; no new kappa.** + +For the unchanged [#628](https://github.com/CrocSwap/integer-mult-bounds/pull/628) +balanced word, with h=ceil(log2 n) shared dirty scratch registers, the sharp +uniform joint interval coefficient envelope is + +```text +F(h) = floor(h^2/2) + h + 2, h >= 0. +``` + +Every ordered pair of complete ideal-leaf cuts and both word orientations +are covered. The bound holds without commutation for contractive operator +factors. For commuting factors whose every subset product has norm at most +G>=1, the bound is F(h)G. The word, scratch allocation and leaf interfaces +are unchanged. Uniform sharpness means the maximum over n of each height; +it does not assert equality for every n. + +This closes the explicit sharp-constant question in Arham Tahir's +[#1374](https://github.com/CrocSwap/integer-mult-bounds/pull/1374) and Nick +Petalas's [#5872](https://github.com/CrocSwap/integer-mult-bounds/pull/5872). +The latter upper bound was h^2+2h+3 for h>=1. The matching all-height lower +family is entirely credited to #1374; this package supplies the new upper +proof. The exact destination-only result of Philippe Van Velzen's +[#2177](https://github.com/CrocSwap/integer-mult-bounds/pull/2177) is separate. + +| Height h | #5872 upper bound | New sharp envelope | +| --- | --- | --- | +| 1 | 6 | 3 | +| 2 | 11 | 6 | +| 3 | 18 | 9 | +| 4 | 27 | 14 | +| 8 | 83 | 42 | +| 16 | 291 | 146 | + +## Why the bound improves + +[PROOF.md](PROOF.md) proves that an inverse of a positive prefix has no two +consecutive occupied source-column entries in row order `(target,z1,...,zh)`. +Its scratch block has at most one occupied direction per scratch pair. +Together, these give total scratch-row mass at most floor((h+1)^2/2). + +The six chronological phase-pair formulas always place an inverse-positive +prefix or positive suffix on the right of a cross-child product. That +direction matters: an ordinary positive prefix can violate the new scratch +mass bound. Applying the invariant to the correct factor, and retaining one +endpoint cancellation in the first-to-last phase pair, proves F(h). + +Hanson Sun's [#1085](https://github.com/CrocSwap/integer-mult-bounds/pull/1085) +entry invariant is an explicit proof premise. Charles Bethin's +[#1278](https://github.com/CrocSwap/integer-mult-bounds/pull/1278) supplies the +phase decomposition and the squarefree theorem needed for the commuting +subset-product corollary. These retained proofs were read in full; their +all-size premises are not established by the finite certificate here. + +## Exact verification and reproduction + +The Python 3.12 standard-library verifier imports no predecessor executable. +Its free noncommutative polynomials retain repeated indices and collect +equal words before measuring mass; no commutative or squarefree quotient +is imposed. A separate scalar engine skips completed subtrees using the +four phase formulas and uses rational Gauss-Jordan inversion. Its sampled +prefixes are checked against the literal polynomial engine. +That compressed-prefix/Gauss-Jordan corroboration strategy follows #1374; +the implementation here is separately written and imports none of its code. + +- All positive prefixes at every n=1..64: **95,735 boundaries**, checking + the new inverse source-occupancy and scratch-mass invariants, both + prefix/inverse scratch-pair restrictions, protected boundaries, full + restoration and literal inverse word order. There are **317** sampled + exact inverse identities and independent scalar-prefix comparisons. +- **89,528 nonempty intervals**, both orientations, at + n=1,2,3,5,8,11,16. Every surviving monomial is checked without assuming + squarefreeness. Empty intervals are identities. This corroboration does + not claim priority for the predecessor's finite maxima. +- **2,118** exact phase-identity checks, including reverse order: all child + cuts at n=2,3,4,5 and five selected child cuts at n=8,11,16. +- The predecessor's attaining scalar family is checked by literal free + algebra at h=1..6 and by compressed exact matrices at h=1..32, the last + having n=4,294,967,296 factors without expanding its word. +- **15 controls** cover adjacent source occupancy, reciprocal scratch + support, an oversized entry, invalid capacities/sign, applying the + scratch bound in the wrong prefix direction, unreversed inversion, a + changed leaf sign, noncommutation, absence of a squarefree quotient, + a false linear bound, an understated sharp bound and wrong matrix order. + +From the repository root: + +```sh +python3 -B -W error -X dev research/chronological-dirty-intervals/verify.py +python3 -B -W error -X dev -O research/chronological-dirty-intervals/verify.py +python3 -B scripts/research_package.py --package research/chronological-dirty-intervals +python3 -B scripts/check_research_commit.py --package research/chronological-dirty-intervals --check-source-history +``` + +Expected markers are `PASS_CHRONOLOGICAL_DIRTY_INTERVALS`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +Default verification is read-only and compares every deterministic field +with [CERTIFICATE.json](CERTIFICATE.json). `--write PATH` is explicit +certificate authoring, not evidence that a preexisting certificate passed. +The stdout receipt hashes every package .py/.md/.json file present at run +time. The mathematical replay works from a Git-free export of this package; +source-provenance validation additionally requires the pinned Git history. + +The finite emitter is capped at 64 factors. The compressed scalar oracle +is capped at 2^32 factors and only uses +-1 coefficients. All fixtures, +cut selections and stopping coverage are explicit in the code/certificate. +Python-managed allocation is used; no fixed-allocation implementation is +claimed. No network, subprocess, numerical solver or floating point is used +by the mathematical verifier. Normal and optimized execution are required +by [VERIFY.json](VERIFY.json). +Both registered commands passed on Linux x86_64 with CPython 3.12.14; +the separate package metadata/source-pin check also passed. +The committed-byte preflight passed. Its optional `--check-source-history` +extension could not complete because this checkout is shallow; it reports +`source-history check requires full Git history`. No history-wide ancestry +validation is claimed. The base and all declared sources use the same +pinned canonical-main commit; there are no unmerged-source dependencies. + +## Scope and provenance + +Base canonical main is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +[SOURCES.json](SOURCES.json) pins exact Git and SHA256 bytes for the selected +record, task card, dispatcher, imported proof premises, lower family, prior +upper bound and destination-only context. They are historical provenance, +not runtime imports. The assignment narrows the archived +`commuting-dirty-precision` follow-up to the still-open sharp joint constant; +it is explicitly a changed scope from the current caller-admission card. + +The lead checked live overlap before assignment and found #5872's explicit +remaining sharp question. This package does not treat that bounded overlap +search as proof of global novelty. The written all-size induction, finite +corroboration and imported lower theorem are distinct claims. Independent +human review and formal proof-kernel verification are unclaimed. + +The selected conditional kappa 0.003125804 and its five framework assumptions +remain unchanged. Internal rounded leaves, inverse preimages, nonlinear error +support, precision/tape integration, preparation, physical movement, compiler, +stock, analytic recovery and a complete caller invoice remain unproved or +unrun here. No actual cyclic rounding failure or precision minimum follows. + +## Open next questions + +1. What is the exact joint envelope for **each n**, rather than the sharp + height-uniform envelope? For example n=3 has finite maximum four, below + F(2)=six. Derive recurrences that retain unequal child heights and the + available phase cuts. The obstacle is simultaneous attainability of + support and source-occupancy maxima. This may refine sufficient bounds + for specific unchanged words; it is not a reason to expand a supplier. +2. Can a concrete rounded caller benefit from this joint bound after its + actual perturbation support is retained? Start with its exact leaf error + contract and compare the destination-supported #2177 bound before using + a joint bound. Negative-leaf preimages, preparation, internal magnitudes + and the full physical invoice must still be supplied. No such integration + is attempted here. + +Structured versions and the frozen stop decision are in [TASK.json](TASK.json). + +## Credit + +Prepared for **@CubeJerry**, with substantial **OpenAI Codex assistance** in +mathematics, implementation, verification and writing. New material is +Apache-2.0. Chafik Boukhalfa supplies #628/#905 and the retained word lineage; +Hanson Sun supplies #1085; Charles Bethin supplies #1278 and #1416; Arham +Tahir supplies #1374's exact lower family and sharp-constant question; Nick +Petalas supplies #5872's predecessor upper improvement and explicit handoff; +Philippe Van Velzen supplies the separate #2177 result. Philipp/mightyOil, +Gareth Davidson and 0xkilgore retain the precision, perturbation, counting +and restoration lineage credited in those predecessor sources. diff --git a/research/chronological-dirty-intervals/REVIEW.md b/research/chronological-dirty-intervals/REVIEW.md new file mode 100644 index 0000000000..243ac44730 --- /dev/null +++ b/research/chronological-dirty-intervals/REVIEW.md @@ -0,0 +1,71 @@ +# Exact-commit cross-review + +Reviewed on 2026-11-06 by a separate OpenAI Codex worker in the @CubeJerry +research session. This is an independent AI derivation/code review within +the author-side workflow, not independent human or proof-kernel acceptance. + +The reviewed commit is `485c8174677bfef24472d4cdf46e83574cfc3b44`. +The reviewer checked a clean working tree and these exact SHA256 hashes: + +| File | SHA256 | +| --- | --- | +| PROOF.md | `eeb46c387e9a3965c9e15a8d75f750796fa1d8d8f1b32a6808bd4feaa799a53a` | +| verify.py | `5687a7fbec81378d66f514a006cd327dd9cb6156cab19089b0f8f42ca141e48e` | +| scalar_oracle.py | `9213efcd7dafd9a171c0b6d60c9badf6307c945e6d031702ce19a584767b4ac9` | +| CERTIFICATE.json | `ea0061f56cfdc39fee148e401b9d88cfddaea0760c6d2daa7d0926a68bb3afb7` | + +The reviewer independently checked the scratch-pair restriction, inverse +source-column nonadjacency (including phase 2 and unequal-child padding), +both cross-child product orders, all six phase identities and their reverse +directions, the first-to-last phase endpoint cancellation, induction height +inequalities and the negative-word reduction. No unresolved scientific gap +was found under the explicitly imported #1085/#1278/#1374 premises. + +Implementation inspection confirmed that the formal verifier retains +noncommuting and repeated factors, uses the correct leaf and inverse-prefix +updates, and maps complementary cuts correctly. Its controls distinguish +the inverse direction, factor order and a changed leaf sign. The compressed +scalar route is meaningfully distinct from the literal polynomial engine. +The registered commands correctly omit `-I`, since the verifier imports its +sibling scalar module by name. + +The reviewer did not rerun the author's already-passed scientific suite and +did not independently audit the imported predecessor theorems. The original +normal/optimized runs, provenance-pin check and committed-byte check remain +author-side evidence, with the shallow-history limitation described in the +README. This review supplies no rounded-caller admission, selected-framework +assumption, precision invoice or new kappa. + +This follow-up adds only the review record; the four scientific files above +remain unchanged from the reviewed commit. + +## Additional all-height upper-proof audit + +On 2026-11-06, the fresh reviewer `/root/final_interval_audit` independently +audited the all-height upper argument. This review binds the same four +scientific SHA256 hashes in the table above, including PROOF.md +`eeb46c387e9a3965c9e15a8d75f750796fa1d8d8f1b32a6808bd4feaa799a53a`. +No scientific file changed for this documentation update. + +The fresh derivation checked inverse-positive-prefix source nonadjacency, +especially the phase-2 pattern `(1-f,f,v)`, unequal-height zero padding, +and the scratch-row bound `H(k)=floor((k+1)^2/2)`. It verified that the +argument assumes no correlation between source occupancy and scratch +support. The reviewer also checked the rightmost-factor cross-child +estimates, all six phase pairs, reverse and complementary cuts, the +phase-0-to-3 source cancellation or filling `AB-efAB`, and the height-one +and leaf bases. No gap was found in the scoped upper proof. + +The reviewer verified the imported source pins. A separate delegated audit +rederived #1085's eight signed prefix cases and corroborated them with 32 +abstract free-ring cases and 16 outer inverse identities. These checks do +not assume `e=f`. They support the stated prefix argument; they are not a +comprehensive reproof of every imported predecessor theorem. + +This was an author-side AI written-proof audit. It did not rerun the +author's interval census or independently reprove #1374's all-height lower +family, and it supplies neither formal verification nor human acceptance. +The historical #628 proposal is closed and unmerged; that provenance does +not invalidate a theorem about its precisely specified ideal word and does +not provide caller admission. No rounded execution, precision invoice, +selected-framework assumption or new kappa follows from this audit. diff --git a/research/chronological-dirty-intervals/SOURCES.json b/research/chronological-dirty-intervals/SOURCES.json new file mode 100644 index 0000000000..c45c231fa7 --- /dev/null +++ b/research/chronological-dirty-intervals/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/commuting-dirty-precision/vendor/pr1085/PROOF.md", + "usage": "provenance", + "git_blob": "b794f4253b30f9af1d29c875097d04349715582b", + "sha256": "b21febd8202b433f3f7c046e2c62e29c5772c8bee79327c51729d500c024a8b2" + }, + { + "path": "research/commuting-dirty-precision/vendor/pr628/dirty.py", + "usage": "provenance", + "git_blob": "2b9471083706a37519a1af7598e012f5fecf2636", + "sha256": "09e7f41141594e6540828330d27be27c083ee6569660ae42c0cd519b09fc8d21" + }, + { + "path": "research/commuting-interval-audit/PROOF.md", + "usage": "provenance", + "git_blob": "de9c8fca358c225e2ef30180c553717208015252", + "sha256": "17d346b53eb71780410e1ec5e87d56bc444215a540e98c84283f12553c0c81e9" + }, + { + "path": "research/dirty-interval-coefficient-boundary/README.md", + "usage": "provenance", + "git_blob": "59cb826f1378d1311fa1994c872e3bf20703f669", + "sha256": "41c69924abe9881d4b68549879dd248adccfd379899281ad6b9289b814429604" + }, + { + "path": "research/leaf-destination-transport-bound/README.md", + "usage": "provenance", + "git_blob": "b8d857e408f4e0bbdff33d33a134a6d8e8f4649c", + "sha256": "01a2c4d599fd6e071c613026627fdf980b45f9cfaadb9cbb0c96d9ab5591ebd9" + }, + { + "path": "research/protected-boundary-interval-bound/PROOF.md", + "usage": "provenance", + "git_blob": "e479ec14188376318b6f22c054e6d8033e9dc24d", + "sha256": "44cbe214b52cad7ffcb4865c3cd0a6aa2c2f8d70d32a3cd4411550e08d738ec6" + } + ] +} diff --git a/research/chronological-dirty-intervals/TASK.json b/research/chronological-dirty-intervals/TASK.json new file mode 100644 index 0000000000..38721b9935 --- /dev/null +++ b/research/chronological-dirty-intervals/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp all-size height-uniform joint coefficient envelope floor(h^2/2)+h+2 for every ordered pair of complete ideal-leaf cuts in both orientations of the unchanged #628 balanced dirty word.", + "scope_change_reason": "Explicit assigned adversarial/precision task, seed 66, takes the archived commuting-dirty-precision sharp-constant follow-up narrowed by #5872. The new exact upper proof matches the previously known #1374 lower family; it does not discharge a current supplier assumption.", + "bottleneck_link": "A precise generic interval envelope is a local precision-interface side result; actual perturbation support and a complete caller invoice are still required for downstream admission.", + "budget_minutes": 90, + "stop_rule": "Stop or pivot after 35 minutes without a new proof direction. A new invariant was found before that cutoff; freeze after the exact uniform upper proof and bounded verification, leaving per-n sharpness and rounded integration open.", + "outcome": "completed", + "evidence": "PROOF.md; CERTIFICATE.json; standalone stdlib free-algebra verifier and independent compressed scalar oracle; normal and optimized registered commands.", + "author": "@CubeJerry", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation, verification and writing. Another Codex worker cross-reviewed the complete proof; independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact joint interval envelope for each n?", + "why_it_matters": "The sharp height-uniform envelope is not attained at every factor count; e.g. n=3 has maximum four below F(2)=six.", + "first_step": "Retain unequal child sizes and available chronological phase cuts in support/occupancy recurrences.", + "blocked_by": "Simultaneous attainment of scratch support and source occupancy for each fixed n is not established." + }, + { + "question": "Can an exact rounded caller benefit after retaining its true error support?", + "why_it_matters": "A norm lemma alone does not lower a complete paid precision or physical invoice.", + "first_step": "Fix one rounded caller and compare its leaf error support with the separate destination-supported #2177 bound before substituting a joint bound.", + "blocked_by": "Negative-leaf preimages, preparation, internal magnitudes, precision and the complete physical bill remain separate obligations." + } + ], + "environment": { + "interpreter": "3.12.14", + "platform": "Linux-6.18.57-x86_64-with-glibc2.39", + "dependencies": "Python standard library only" + }, + "overlap": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "assignment": "seed 66; adversarial/precision audit", + "lead_scope": "Live overlap check found #5872 as latest narrow upper improvement and no exact-sharp successor; destination-only #2177 was excluded as already solved.", + "coverage_limit": "A bounded live semantic search, not proof of global novelty." + }, + "expansion_decision": "Frozen local proof contribution. No supplier construction, selected record or kappa change." +} diff --git a/research/chronological-dirty-intervals/VERIFY.json b/research/chronological-dirty-intervals/VERIFY.json new file mode 100644 index 0000000000..21484deea9 --- /dev/null +++ b/research/chronological-dirty-intervals/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "-X", + "dev", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact free-algebra prefix sparsity, 89528 intervals, six phase identities in both directions, literal and compressed scalar witnesses, 15 controls, deterministic committed-certificate comparison and package byte receipt." + }, + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "-X", + "dev", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact free-algebra prefix sparsity, 89528 intervals, six phase identities in both directions, literal and compressed scalar witnesses, 15 controls, deterministic committed-certificate comparison and package byte receipt." + } + ] +} diff --git a/research/chronological-dirty-intervals/scalar_oracle.py b/research/chronological-dirty-intervals/scalar_oracle.py new file mode 100644 index 0000000000..dde144cd85 --- /dev/null +++ b/research/chronological-dirty-intervals/scalar_oracle.py @@ -0,0 +1,113 @@ +"""Compressed integer-prefix oracle, independently from formal leaf expansion. + +@CubeJerry with substantial OpenAI Codex assistance; Apache-2.0. +Only scalar +-1 factors, exact integer matrices and Fraction inversion. +""" +from fractions import Fraction +from functools import lru_cache + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def eye(d): + return [[int(i == j) for j in range(d)] for i in range(d)] + + +def product(a, b): + columns = list(zip(*b)) + return [[sum(c*d for c, d in zip(row, col)) for col in columns] for row in a] + + +def inverse(matrix): + d = len(matrix) + rows = [[Fraction(c) for c in row]+unit for row, unit in zip(matrix, eye(d))] + for j in range(d): + pivot = next((i for i in range(j, d) if rows[i][j]), None) + need(pivot is not None, "singular prefix") + rows[j], rows[pivot] = rows[pivot], rows[j] + divisor = rows[j][j] + rows[j] = [c/divisor for c in rows[j]] + for i in range(d): + if i != j: + coefficient = rows[i][j] + rows[i] = [c-coefficient*v for c, v in zip(rows[i], rows[j])] + need(all(c.denominator == 1 for row in rows for c in row), "nonintegral inverse") + return [[int(c) for c in row[d:]] for row in rows] + + +@lru_cache(maxsize=256) +def leaf_count(n): + if n == 1: + return 1 + return 2*(leaf_count(n//2)+leaf_count(n-n//2)) + + +def prefix(n, cut, negative_indices): + need(isinstance(n, int) and 1 <= n <= 1 << 32, "scalar factor capacity") + need(0 <= cut <= leaf_count(n), "scalar cut range") + need(len(set(negative_indices)) == len(negative_indices) + and all(0 <= i < n for i in negative_indices), "negative factor indices") + d = (n-1).bit_length()+2 + accumulated = eye(d) + lo, count, x, y, level = 0, n, 0, 1, 0 + def coefficient(start, size): + return (-1)**sum(start <= i < start+size for i in negative_indices) + def shear(source, target, value): + matrix = eye(d) + matrix[target][source] = value + return matrix + while True: + if cut == 0: + return accumulated + if cut == leaf_count(count): + return product(shear(x, y, coefficient(lo, count)), accumulated) + left = count//2 + right = count-left + lu, lv = leaf_count(left), leaf_count(right) + z = level+2 + b, a = coefficient(lo, left), coefficient(lo+left, right) + if cut <= lu: + count, y = left, z + elif cut <= lu+lv: + accumulated = product(shear(x, z, b), accumulated) + lo, count, x, cut = lo+left, right, z, cut-lu + elif cut <= 2*lu+lv: + completed = product(shear(x, z, -b), product(shear(z, y, a), shear(x, z, b))) + accumulated = product(completed, accumulated) + count, y, cut = left, z, 2*lu+lv-cut + else: + accumulated = product(shear(x, y, a*b), accumulated) + lo, count, x, cut = lo+left, right, z, 2*(lu+lv)-cut + level += 1 + + +def verify_witnesses(): + witnesses = [] + for h in range(1, 33): + n = 1 << h + negatives = tuple(n-(1 << k)-1 for k in range(h-1)) + a, b = 3*4**(h-1)//5, (4**h+2)//3 + pa, pb = prefix(n, a, negatives), prefix(n, b, negatives) + q = inverse(pa) + need(product(pa, q) == eye(h+2), "scalar inverse identity") + interval = product(pb, q) + expected = [(-1)**(h-1)*(1+h//2), 1] + expected += [j*(-1)**(h+j) for j in range(1, h+1)] + need(interval[1] == expected, "PR1374 exact target row") + norm = max(sum(abs(c) for c in row) for row in interval) + need(norm == h*h//2+h+2, "sharp witness norm") + if h == 2: + need(norm > h+2 and norm > h*h//2+h+1, "understated-bound controls") + need(product(q, pb) != interval, "wrong matrix product-order control") + witnesses.append({"h": h, "n": n, "cuts": [a, b], "norm": norm}) + return {"exact_integer_witnesses": witnesses, + "method": "compressed four-phase prefixes plus rational Gauss-Jordan inverse", + "controls": ["false_linear_bound", "sharp_bound_minus_one", "wrong_product_order"]} + + +if __name__ == "__main__": + import json + print(json.dumps(verify_witnesses(), sort_keys=True)) diff --git a/research/chronological-dirty-intervals/verify.py b/research/chronological-dirty-intervals/verify.py new file mode 100644 index 0000000000..ac9b58712c --- /dev/null +++ b/research/chronological-dirty-intervals/verify.py @@ -0,0 +1,356 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration, @CubeJerry + OpenAI Codex, Apache-2.0. + +No predecessor code, symbolic package, squarefree quotient or float is used. +The all-size proof is PROOF.md, not extrapolation from this finite program. +""" +import argparse +import hashlib +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +INTERVAL_SIZES = (1, 2, 3, 5, 8, 11, 16) +MAX_N = 64 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def envelope(h): + need(isinstance(h, int) and 0 <= h <= 10000, "height capacity") + return h*h//2+h+2 + + +def scratch_bound(h): + return (h+1)*(h+1)//2 + + +def add(a, b): + out = a.copy() + for word, coefficient in b.items(): + out[word] = out.get(word, 0)+coefficient + if not out[word]: + del out[word] + return out + + +def multiply_poly(a, b): + out = {} + for u, c in a.items(): + for v, d in b.items(): + word = u+v + out[word] = out.get(word, 0)+c*d + if not out[word]: + del out[word] + return out + + +def identity(d): + return [[{(): 1} if i == j else {} for j in range(d)] for i in range(d)] + + +def multiply(a, b): + d = len(a) + out = [[{} for _ in range(d)] for _ in range(d)] + for i, row in enumerate(a): + for j, left in enumerate(row): + if left: + for k, right in enumerate(b[j]): + if right: + out[i][k] = add(out[i][k], multiply_poly(left, right)) + return out + + +def row_mass(row): + return sum(abs(c) for entry in row for c in entry.values()) + + +def forward(matrix, event): + x, y, factor, sign = event + out = [row.copy() for row in matrix] + out[y] = [add(a, {(factor,)+word: sign*c for word, c in b.items()}) + for a, b in zip(matrix[y], matrix[x])] + return out + + +def inverse_prefix(matrix, event): + x, y, factor, sign = event + out = [row.copy() for row in matrix] + for row in out: + row[x] = add(row[x], {word+(factor,): -sign*c for word, c in row[y].items()}) + return out + + +def emit(n, sign=1, start=0, source=0, target=1, depth=0): + need(isinstance(n, int) and 1 <= n <= MAX_N, "factor count capacity") + need(sign in (-1, 1), "word sign") + events = [] + stack = [(start, n, source, target, depth, sign)] + while stack: + lo, count, x, y, level, direction = stack.pop() + if count == 1: + events.append((x, y, lo, direction)) + continue + left = count//2 + z = level+2 + children = [(lo, left, x, z, level+1, 1), + (lo+left, count-left, z, y, level+1, 1), + (lo, left, x, z, level+1, -1), + (lo+left, count-left, z, y, level+1, -1)] + if direction == -1: + children = [(*child[:-1], -child[-1]) for child in reversed(children)] + stack.extend(reversed(children)) + return events + + +def prefixes(events, d): + p, q = identity(d), identity(d) + result = [(p, q)] + for event in events: + p, q = forward(p, event), inverse_prefix(q, event) + result.append((p, q)) + return result + + +def check_entries(matrix): + need(all(len(p) <= 1 and all(abs(c) == 1 for c in p.values()) + for row in matrix for p in row), "prefix unit-entry invariant") + + +def check_scratch_pairs(matrix): + d = len(matrix) + need(all(matrix[i][i] == {(): 1} for i in range(d)), "identity diagonal") + need(not any(matrix[i][j] and matrix[j][i] + for i in range(2, d) for j in range(i+1, d)), "opposite scratch support") + + +def check_source_occupancy(matrix): + occupied = [bool(matrix[i][0]) for i in range(1, len(matrix))] + need(not any(a and b for a, b in zip(occupied, occupied[1:])), + "adjacent inverse source occupancy") + + +def prefix_census(): + from scalar_oracle import prefix + boundaries, identities = 0, 0 + maxima = {} + for n in range(1, MAX_N+1): + h = (n-1).bit_length() + events = emit(n) + need(emit(n, -1) == [(x, y, f, -s) for x, y, f, s in reversed(events)], + "literal negative word") + data = prefixes(events, h+2) + for t, (p, q) in enumerate(data): + boundaries += 1 + for matrix in (p, q): + check_entries(matrix) + check_scratch_pairs(matrix) + need(matrix[0] == identity(h+2)[0], "protected source") + need(all(matrix[i][1] == ({(): 1} if i == 1 else {}) + for i in range(h+2)), "unread target") + check_source_occupancy(q) + mass = sum(row_mass(row) for row in q[2:]) + need(mass <= scratch_bound(h), "inverse scratch mass") + maxima[str(h)] = max(maxima.get(str(h), 0), mass) + if t in {0, 1, len(events)//2, len(events)-1, len(events)}: + need(multiply(p, q) == identity(h+2), "prefix inverse identity") + negatives = tuple(i for i in range(n) if i % 3 == 1) + evaluated = [[sum(c*(-1)**sum(f in negatives for f in word) + for word, c in entry.items()) for entry in row] for row in p] + need(prefix(n, t, negatives) == evaluated, "independent scalar/formal prefix agreement") + identities += 1 + endpoint = identity(h+2) + endpoint[1][0] = {tuple(range(n-1, -1, -1)): 1} + need(data[-1][0] == endpoint, "full arbitrary-dirty endpoint") + return {"factor_counts": [1, MAX_N], "positive_prefix_boundaries": boundaries, + "sampled_inverse_identities": identities, + "maximum_inverse_scratch_mass_by_height": maxima} + + +def interval_census(): + results, total = [], 0 + for n in INTERVAL_SIZES: + h = (n-1).bit_length() + best = 0 + for sign in (1, -1): + events = emit(n, sign) + for a in range(len(events)): + matrix = identity(h+2) + for event in events[a:]: + matrix = forward(matrix, event) + mass = max(map(row_mass, matrix)) + need(mass <= envelope(h), "sharp interval envelope") + need(all(len(word) == len(set(word)) for row in matrix + for entry in row for word in entry), "squarefree surviving word") + best = max(best, mass) + total += 1 + results.append({"n": n, "h": h, "maximum": best, "bound": envelope(h)}) + return {"both_orientations_nonempty_intervals": total, "cases": results} + + +def shear(d, x, y, polynomial): + out = identity(d) + out[y][x] = polynomial + return out + + +def adjust(matrix, i, j, polynomial): + out = [row.copy() for row in matrix] + out[i][j] = add(out[i][j], polynomial) + return out + + +def phase_census(): + counts = {name: 0 for name in ("01", "12", "23", "02", "13", "03")} + for n in (2, 3, 4, 5, 8, 11, 16): + d = (n-1).bit_length()+2 + mid = n//2 + left = emit(mid, start=0, source=0, target=2, depth=1) + right = emit(n-mid, start=mid, source=2, target=1, depth=1) + ls, rs = prefixes(left, d), prefixes(right, d) + parent = prefixes(emit(n), d) + u, ui = ls[-1] + v, vi = rs[-1] + ab = {tuple(range(n-1, -1, -1)): 1} + b = {tuple(range(mid-1, -1, -1)): 1} + a = {tuple(range(n-1, mid-1, -1)): 1} + lu, lv = len(left), len(right) + cuts_l = range(lu+1) if n <= 5 else sorted({0, 1, lu//2, lu-1, lu}) + cuts_r = range(lv+1) if n <= 5 else sorted({0, 1, lv//2, lv-1, lv}) + for name in counts: + first = cuts_l if name[0] in "02" else cuts_r + second = cuts_l if name[1] in "02" else cuts_r + for ac in first: + for bc in second: + pa, pai = (ls if name[0] in "02" else rs)[ac] + pb, pbi = (ls if name[1] in "02" else rs)[bc] + times = (ac, lu+ac, 2*lu+lv-ac, 2*(lu+lv)-ac) + ends = (bc, lu+bc, 2*lu+lv-bc, 2*(lu+lv)-bc) + s, t = times[int(name[0])], ends[int(name[1])] + actual = multiply(parent[t][0], parent[s][1]) + reverse = multiply(parent[s][0], parent[t][1]) + if name == "01": + predicted = multiply(pb, multiply(u, pai)) + backward = multiply(multiply(pa, ui), pbi) + elif name == "12": + predicted = multiply(multiply(pb, ui), multiply(v, pai)) + backward = multiply(multiply(pa, vi), multiply(u, pbi)) + elif name == "23": + predicted = multiply(multiply(pb, vi), pai) + backward = multiply(pa, multiply(v, pbi)) + elif name == "02": + predicted, backward = multiply(pb, pai), multiply(pa, pbi) + row, backrow = multiply(u, pai)[2], multiply(u, pbi)[2] + for j in range(d): + predicted = adjust(predicted, 1, j, multiply_poly(a, row[j])) + backward = adjust(backward, 1, j, multiply_poly({w: -c for w, c in a.items()}, backrow[j])) + elif name == "13": + predicted, backward = multiply(pb, pai), multiply(pa, pbi) + col, backcol = multiply(pb, vi), multiply(pa, vi) + for i in range(d): + predicted = adjust(predicted, i, 0, multiply_poly(col[i][2], {w: -c for w, c in b.items()})) + backward = adjust(backward, i, 0, multiply_poly(backcol[i][2], b)) + else: + predicted = adjust(multiply(pb, pai), 1, 0, ab) + backward = adjust(multiply(pa, pbi), 1, 0, {w: -c for w, c in ab.items()}) + need(predicted == actual and backward == reverse, "phase identity "+name) + counts[name] += 2 + return {"both_orders_identity_checks": counts, + "all_child_cuts_n": [2, 3, 4, 5], "five_child_cuts_n": [8, 11, 16]} + + +def controls(): + passed = [] + def rejects(name, fn): + try: + fn() + except ValueError: + passed.append(name) + else: + raise ValueError("control accepted: "+name) + bad = identity(4) + bad[2][0] = {(0,): -1} + bad[3][0] = {(1,): -1} + rejects("adjacent_source_bits", lambda: check_source_occupancy(bad)) + bad_pair = identity(4) + bad_pair[2][3], bad_pair[3][2] = {(0,): 1}, {(1,): 1} + rejects("reciprocal_scratch_entries", lambda: check_scratch_pairs(bad_pair)) + oversized = identity(3) + oversized[2][0] = {(0,): 2} + rejects("oversized_prefix_entry", lambda: check_entries(oversized)) + for value in (0, 65): + rejects("factor_count_"+str(value), lambda value=value: emit(value)) + rejects("invalid_sign", lambda: emit(2, 0)) + rejects("invalid_height", lambda: envelope(-1)) + positive = prefixes(emit(8), 5)[6][0] + need(sum(row_mass(r) for r in positive[2:]) == 9 > scratch_bound(3), + "positive-prefix countercontrol") + passed.append("inverse_direction_is_essential") + events = emit(4) + wrong = [(x, y, f, -s) for x, y, f, s in events] + need(prefixes(events+wrong, 4)[-1][0] != identity(4), "wrong inverse order control") + passed.append("wrong_inverse_order") + altered = events.copy() + x, y, f, s = altered[5] + altered[5] = (x, y, f, -s) + need(prefixes(altered, 4)[-1][0] != prefixes(events, 4)[-1][0], "restoration mutation") + passed.append("changed_leaf_sign") + need(multiply_poly({(0,): 1}, {(1,): 1}) != multiply_poly({(1,): 1}, {(0,): 1}), + "noncommuting control") + need(multiply_poly({(0,): 1}, {(0,): 1}) == {(0, 0): 1}, "no squarefree quotient") + passed.extend(["factor_order_retained", "repeated_factor_retained"]) + return passed + + +def literal_witnesses(): + cases = [] + for h in range(1, 7): + n = 1 << h + negatives = {n-(1 << k)-1 for k in range(h-1)} + a, b = 3*4**(h-1)//5, (4**h+2)//3 + matrix = identity(h+2) + for event in emit(n)[a:b]: + matrix = forward(matrix, event) + row = [sum(c*(-1)**sum(f in negatives for f in word) + for word, c in entry.items()) for entry in matrix[1]] + expected = [(-1)**(h-1)*(1+h//2), 1] + expected += [j*(-1)**(h+j) for j in range(1, h+1)] + need(row == expected, "literal lower-family row") + need(row_mass(matrix[1]) == sum(map(abs, row)) == envelope(h), + "literal scalar attainment of free coefficient mass") + cases.append({"h": h, "n": n, "cuts": [a, b], "target_row": row}) + return cases + + +def certificate(): + from scalar_oracle import verify_witnesses + return {"schema_version": 1, + "claim": "finite corroboration of the scoped written sharp-envelope proof", + "prefixes": prefix_census(), "intervals": interval_census(), + "phase_formulas": phase_census(), "scalar_witnesses": verify_witnesses(), + "literal_witnesses": literal_witnesses(), + "controls": controls()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="explicit authoring output; default is read-only") + args = parser.parse_args() + result = certificate() + if args.write: + args.write.write_text(json.dumps(result, indent=2, sort_keys=True)+"\n") + else: + expected = json.loads((HERE/"CERTIFICATE.json").read_text()) + need(result == expected, "committed mathematical certificate mismatch") + bindings = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file() and p.suffix in (".py", ".md", ".json")} + print(json.dumps({"status": "PASS_CHRONOLOGICAL_DIRTY_INTERVALS", "bindings": bindings, + "prefix_boundaries": result["prefixes"]["positive_prefix_boundaries"], + "intervals": result["intervals"]["both_orientations_nonempty_intervals"]}, sort_keys=True)) + + +if __name__ == "__main__": + main()