diff --git a/research/k8-gaussian-unit-rounding-seed24/CENSUS.json.gz b/research/k8-gaussian-unit-rounding-seed24/CENSUS.json.gz new file mode 100644 index 0000000000..9f58e3291f Binary files /dev/null and b/research/k8-gaussian-unit-rounding-seed24/CENSUS.json.gz differ diff --git a/research/k8-gaussian-unit-rounding-seed24/CERTIFICATE.json b/research/k8-gaussian-unit-rounding-seed24/CERTIFICATE.json new file mode 100644 index 0000000000..5703ad6dbf --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/CERTIFICATE.json @@ -0,0 +1,570 @@ +{ + "status": "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING", + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "assignment_seed": 24, + "eligible_helpers": [ + 225, + 226, + 227, + 228, + 229, + 230, + 231, + 232, + 233, + 234, + 235, + 236, + 237, + 238, + 239, + 241, + 242, + 243, + 244, + 245, + 246, + 247, + 248, + 249, + 250, + 251, + 252, + 253, + 254, + 255, + 257, + 258, + 259, + 260, + 261, + 262, + 263, + 264, + 265, + 266, + 267, + 268, + 269, + 270, + 271, + 272, + 274, + 276, + 278, + 279, + 280, + 281, + 283, + 284, + 285, + 286, + 287, + 288, + 290, + 292, + 294, + 295, + 296, + 297, + 299, + 300, + 301, + 302, + 303, + 304, + 306, + 308, + 310, + 312, + 313, + 315, + 316, + 317, + 318, + 319, + 320, + 322, + 324, + 326, + 328, + 329, + 331, + 332, + 333, + 334, + 335, + 336, + 338, + 340, + 342, + 343, + 344, + 345, + 347, + 348, + 349, + 350, + 351, + 352, + 354, + 356, + 358, + 359, + 360, + 361, + 363, + 364, + 365, + 366, + 367, + 368, + 370, + 372, + 374, + 375, + 376, + 377, + 379, + 380, + 381, + 382, + 383, + 384, + 386, + 388, + 390, + 391, + 392, + 393, + 395, + 396, + 397, + 398, + 399, + 400, + 401, + 402, + 403, + 404, + 405, + 406, + 407, + 408, + 409, + 410, + 411, + 412, + 413, + 414, + 415, + 416, + 417, + 418, + 419, + 420, + 421, + 422, + 423, + 424, + 425, + 426, + 427, + 428, + 429, + 430, + 431, + 432, + 433, + 434, + 435, + 436, + 437, + 438, + 439, + 440, + 441, + 442, + 443, + 444, + 445, + 446, + 447, + 456, + 457, + 458, + 459, + 460, + 461, + 462, + 463, + 464, + 465, + 466, + 467, + 468, + 469, + 470, + 471, + 478, + 479, + 480, + 481, + 482, + 483, + 490, + 491, + 492, + 493, + 494, + 495, + 499, + 502, + 503, + 504, + 505, + 507, + 511, + 514, + 515, + 516, + 517, + 519, + 530, + 542, + 546, + 547, + 548, + 549, + 558, + 560, + 568, + 570 + ], + "seed_selected_probe_helper": 250, + "source_members": { + "CANONICAL-WORD.json.gz": { + "archive_member_sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "payload_sha256": "4ddb29fb9bc6f27e0c0fbfcf19a2a93a3496ad900d0f6d89059d0305c9576c0c" + }, + "LOCAL-PROGRAMS.json.gz": { + "archive_member_sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "payload_sha256": "9f41d53659e9be84e20c661560c5687abbf5cd0660cdecbe01ad5eb29e6b8ee3" + }, + "INDEPENDENT-LOCAL-REPLAY.json": { + "archive_member_sha256": "13dd18297162569532983db1a2ab67926b064330cd7edd3587e7b546b2dedf17", + "payload_sha256": "13dd18297162569532983db1a2ab67926b064330cd7edd3587e7b546b2dedf17" + }, + "LOCAL-CHECKS.json": { + "archive_member_sha256": "2b8b1891a736598010232bfb26abc31973b265a53a2009a3fcfd9138b5ecadb4", + "payload_sha256": "2b8b1891a736598010232bfb26abc31973b265a53a2009a3fcfd9138b5ecadb4" + } + }, + "orientations": { + "forward": { + "census_rows": 237, + "integer_breakpoint_evaluations": 2583, + "rounding_fixtures": [ + { + "pattern": 0, + "odd_helpers": 127, + "gaussian_cost": 224322, + "low_cost": 204262, + "high_cost": 208886, + "twice_gap_above_average": 35496 + }, + { + "pattern": 1, + "odd_helpers": 78, + "gaussian_cost": 217670, + "low_cost": 204682, + "high_cost": 206448, + "twice_gap_above_average": 24210 + }, + { + "pattern": 2, + "odd_helpers": 63, + "gaussian_cost": 209882, + "low_cost": 198748, + "high_cost": 200102, + "twice_gap_above_average": 20914 + }, + { + "pattern": 3, + "odd_helpers": 47, + "gaussian_cost": 214132, + "low_cost": 204918, + "high_cost": 207056, + "twice_gap_above_average": 16290 + } + ], + "real_winner": { + "helper": 427, + "a": -2, + "delta": -332, + "incident_adds": 123 + }, + "odd_winner": { + "helper": 427, + "a": -3, + "delta": -58, + "incident_adds": 123 + }, + "programs": { + "baseline": { + "endpoint": { + "complex_input_columns": 712, + "equivalent_real_input_columns": 1424, + "dirty_helper_columns": 480, + "all_helpers_restored": true, + "private_centres_cleared": true + }, + "invoice": { + "complex_scalar_primitives": 149002, + "primitive_stream_sha256": "31bbcdffa552e31b78033cd75f387a4a9e54e8489b9788fa27ef961af59f66e8", + "positive_prefix_l1": "2765345294379392599/1024", + "positive_prefix_bits": 52, + "inherited_charged_bits": 192, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "gaussian_macro_stream_sha256": "dc994cf24ad6a2bcb3ba34106d37d7058096e21944cd085d734017c64137c530", + "assignments": {} + }, + "real": { + "endpoint": { + "complex_input_columns": 712, + "equivalent_real_input_columns": 1424, + "dirty_helper_columns": 480, + "all_helpers_restored": true, + "private_centres_cleared": true + }, + "invoice": { + "complex_scalar_primitives": 148670, + "primitive_stream_sha256": "7575a399819bed0773a004a581708c6c7cbf3836ae5d710a8ea001c798df25e8", + "positive_prefix_l1": "2765345294379392599/1024", + "positive_prefix_bits": 52, + "inherited_charged_bits": 192, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "gaussian_macro_stream_sha256": "d8aeeb63f04263068caf8b35110d75441bbe6dd4907c2afbe7d560e6fdcb5140", + "assignments": { + "427": [ + -2, + 0 + ] + } + }, + "odd": { + "endpoint": { + "complex_input_columns": 712, + "equivalent_real_input_columns": 1424, + "dirty_helper_columns": 480, + "all_helpers_restored": true, + "private_centres_cleared": true + }, + "invoice": { + "complex_scalar_primitives": 148944, + "primitive_stream_sha256": "2912d08752ab0f0ce0b6f9271ae1242549d3f2c0cff56705fd8928d4656f00cd", + "positive_prefix_l1": "2833778267204441351/1024", + "positive_prefix_bits": 52, + "inherited_charged_bits": 192, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "gaussian_macro_stream_sha256": "1988a3a505e3c175e1098e8eea6d53076b750a3f041ac9208636ef215e4feb51", + "assignments": { + "427": [ + -3, + 1 + ] + } + } + } + }, + "backward": { + "census_rows": 237, + "integer_breakpoint_evaluations": 2583, + "rounding_fixtures": [ + { + "pattern": 0, + "odd_helpers": 127, + "gaussian_cost": 221390, + "low_cost": 204534, + "high_cost": 203446, + "twice_gap_above_average": 34800 + }, + { + "pattern": 1, + "odd_helpers": 78, + "gaussian_cost": 216744, + "low_cost": 204544, + "high_cost": 203872, + "twice_gap_above_average": 25072 + }, + { + "pattern": 2, + "odd_helpers": 63, + "gaussian_cost": 216702, + "low_cost": 207280, + "high_cost": 206438, + "twice_gap_above_average": 19686 + }, + { + "pattern": 3, + "odd_helpers": 47, + "gaussian_cost": 210816, + "low_cost": 202902, + "high_cost": 202808, + "twice_gap_above_average": 15922 + } + ], + "real_winner": { + "helper": 427, + "a": 2, + "delta": -332, + "incident_adds": 123 + }, + "odd_winner": { + "helper": 427, + "a": 2, + "delta": -58, + "incident_adds": 123 + }, + "programs": { + "baseline": { + "endpoint": { + "complex_input_columns": 712, + "equivalent_real_input_columns": 1424, + "dirty_helper_columns": 480, + "all_helpers_restored": true, + "private_centres_cleared": true + }, + "invoice": { + "complex_scalar_primitives": 149018, + "primitive_stream_sha256": "c5630edd33fb4c0db4dc249ceb3aebba39211208d9faf85cf48fedc654cfdb8d", + "positive_prefix_l1": "14824960514781440791821/64", + "positive_prefix_bits": 68, + "inherited_charged_bits": 192, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "gaussian_macro_stream_sha256": "0428583855918e475d437a3136599f83e18ae414e64c0acabfa7a2a767b50c43", + "assignments": {} + }, + "real": { + "endpoint": { + "complex_input_columns": 712, + "equivalent_real_input_columns": 1424, + "dirty_helper_columns": 480, + "all_helpers_restored": true, + "private_centres_cleared": true + }, + "invoice": { + "complex_scalar_primitives": 148686, + "primitive_stream_sha256": "8856a5a46cdbd09aebee0b798e71f63e0ccf8d4d0ecadfe88af56e195ed5fa83", + "positive_prefix_l1": "14824960514781440791821/64", + "positive_prefix_bits": 68, + "inherited_charged_bits": 192, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "gaussian_macro_stream_sha256": "7ba646b557ca2380efd266c231ec3381716fcfecc45ebc01531116d5424d7220", + "assignments": { + "427": [ + 2, + 0 + ] + } + }, + "odd": { + "endpoint": { + "complex_input_columns": 712, + "equivalent_real_input_columns": 1424, + "dirty_helper_columns": 480, + "all_helpers_restored": true, + "private_centres_cleared": true + }, + "invoice": { + "complex_scalar_primitives": 148960, + "primitive_stream_sha256": "aeb1a21b8abca9e456761765f5722faeaec261a69618ef50b52deefeccbeeb25", + "positive_prefix_l1": "14824960514781440791821/64", + "positive_prefix_bits": 68, + "inherited_charged_bits": 192, + "paid_profile": { + "1": 2412, + "2": 418, + "3": 432, + "4": 142, + "5": 82, + "8": 8 + } + }, + "gaussian_macro_stream_sha256": "f9ba81c679839458077fdcfe89b2afe9260d2a4f4b5df5d59ae6cd38e699a398", + "assignments": { + "427": [ + 2, + 1 + ] + } + } + } + } + }, + "local_primitive_checks": { + "distinct_gaussian_macros": 464, + "formal_columns_per_macro": 6, + "boundary_pairs": 66 + }, + "rejection_controls": [ + "missing_shared_target", + "wrong_cross_channel_sign", + "missing_product_initialization", + "dirty_work_not_cleared", + "missing_inverse_boundary", + "wrong_boundary_shift", + "operand_alias", + "outside_gaussian_support", + "nondyadic_coefficient", + "gaussian_nonunit", + "zero_factor", + "false_one_step_lipschitz", + "false_independent_rounding", + "removed_source_pin", + "wrong_base", + "modified_lowerer" + ], + "census_payload_sha256": "03534b945a641f5365b7bab50fa38a2d0275c655031a028d013baf990722577d", + "scope": "Written common-rounding theorem for the specified macro-local lowering and separate two-register boundaries; finite exact k8 evidence. No native hosting, new paid profile, kappa or full multiplication theorem." +} diff --git a/research/k8-gaussian-unit-rounding-seed24/INDEPENDENT.json b/research/k8-gaussian-unit-rounding-seed24/INDEPENDENT.json new file mode 100644 index 0000000000..94e9ef24be --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/INDEPENDENT.json @@ -0,0 +1,32 @@ +{ + "helper_count": 237, + "orientations": { + "backward": { + "complete_scalar_baseline": 149018, + "integer_grid_evaluations": 6842, + "incident_term_evaluations": 557508, + "grid_rows_sha256": "068c1608fbc35fafca85fbeef300afc178bf4a579bbecec25f846eab6146c08e" + }, + "forward": { + "complete_scalar_baseline": 149002, + "integer_grid_evaluations": 6842, + "incident_term_evaluations": 557508, + "grid_rows_sha256": "a15d84ff5bbf4a71d9d75a95c9ccc21c109f599cf9ad36e367d328c650c94fc5" + } + }, + "unit_membership_grid": { + "distinct_nonzero_inputs": 3488, + "units": 64, + "nonunits": 3424, + "numerators": [ + -16, + 16 + ], + "common_denominator_exponents": [ + 0, + 3 + ] + }, + "literal_distinct_coefficients": 2532, + "status": "PASS_INDEPENDENT_LITERAL_GAUSSIAN_GRID" +} diff --git a/research/k8-gaussian-unit-rounding-seed24/README.md b/research/k8-gaussian-unit-rounding-seed24/README.md new file mode 100644 index 0000000000..0a761f6f21 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/README.md @@ -0,0 +1,247 @@ +# Common rounding of static Gaussian helper gauges + +**Scoped negative result, with exact finite circuits; no new κ.** Enlarging +static real-dyadic helper gauges to all units of `Z[1/2,i]` does not improve the +unconstrained scalar-cost optimum under the lowering and boundary contract +below. For any finite simultaneous assignment, two explicitly defined +real-dyadic assignments have costs `C0,C1` satisfying + +\[ +C_G \;\ge\; (C_0+C_1)/2+4N_{\rm odd}. +\] + +Here `Nodd` counts helpers with an odd power of `1+i`. Thus one common rounding +costs at least `4Nodd` fewer primitives whenever an odd factor is present. +This is a written proof about a specified scalar circuit class. It does not +assert that rounding preserves an additional precision or physical-admission +constraint, and it does not cover a better Gaussian lowering or boundary fusion. + +The selected k8 word gives a concrete comparison over all 237 eligible helpers, +both orientations, every integer exponent and all four unit phases: + +| Scalar program | Forward | Backward | Saving per orientation | +|---|---:|---:|---:| +| Retained word with PR696 lowering | 149,002 | 149,018 | — | +| Best single real-dyadic gauge, already in PR1161 | 148,670 | 148,686 | 332 | +| Best single odd Gaussian gauge in this class | 148,944 | 148,960 | 58 | + +All winners use L427, which has 123 incident ADDs. The real factors are `1/4` +forward and `4` backward. The odd Gaussian factors are `(1+i)/8` forward and +`4(1+i)` backward. Both boundary transformations, both real components and all +coefficient-work cleanup are charged. The new odd circuits are cheaper than the +original word but are dominated by the known real choice. The 332 saving is +predecessor work, not a new record. + +## Exact source and accounting scope + +Base: `410026dc5513b87db92ae98571d1d5984c69a983`; assignment seed **24**, drawn +from OS randomness for the user's complex-supplier track. The selected record +at that base is the conditional PR1094 construction with +κ `836330098538459/500000000000000000`. [SOURCES.json](SOURCES.json) records Git +blobs and SHA256 hashes. The verifier checks that the PR1042 local word/programs +are byte-identical to the actual PR1094 provider aliases and checks their +retained receipt bindings. It does not rerun the complete selected cold replay. + +The circuit class fixes the real-dyadic ADD topology and all original SCALEs. +A helper has a constant gauge throughout the program. Its entry and inverse +exit use its own two real coordinates, with no boundary workspace or sharing +between helpers. Elementary operations are signed additions, doubling, +halving, negation, copy and clear. COPY and clear cannot occur in an invertible +two-register boundary word, since their singularity cannot be repaired without +another register. Each boundary circuit implements its full map on arbitrary +dirty inputs. Original helper SCALEs are not fused into these boundaries. + +In the k8 census, helpers must be cold/FULL (`start=0`, `final=1`), unwrapped, +non-center, and absent from every scalar COPY/clear in either orientation. +Exactly 237 of the 480 helpers qualify. This is narrower than PR1161's 477-helper +search domain and matches the relevant restriction used in PR1214. The complete +one-helper census is [CENSUS.json.gz](CENSUS.json.gz). Simultaneous assignments +are covered by the theorem; a new joint optimum is **not** computed. + +Each changed ADD is lowered locally, sharing a coefficient product between its +two target channels. The two existing real coefficient-work registers may be +dirty on entry and are cleared on exit. No new helper or source register is +introduced. Original COPY/clear, SCALE, frame, adapter and recursive-call events +are retained. The finite invoices count every scalar primitive, including +source reads, product preparation, accumulation and restoration. The paid +recursive histogram is compared unchanged, not replaced by the scalar count. + +## Proof of the common-rounding inequality + +**1. The unit class is complete.** If `z` and `1/z` lie in `Z[1/2,i]`, then +their squared norms lie in `Z[1/2]` and multiply to one. Hence `|z|²` is an +integer power of two. Write `z=(u+iv)/2^s`, remove common factors of two from +`u,v`, and use `u²+v²=2^k`. If exactly one of the remaining integers is odd, +the sum is odd, so it equals one. If both are odd, the sum is two modulo four, +so it equals two. The remaining pair is therefore an axis unit or `(±1,±1)`. +Every unit has the form + +\[ +g_h=2^{a_h}i^{j_h}(1+i)^{b_h},\quad +a_h\in\mathbb Z,\quad j_h\in\{0,1,2,3\},\quad b_h\in\{0,1\}. +\] + +This argument is elementary and all-exponent; the finite unit census below is +a check of its implementation, not its proof. + +**2. The exact macro costs.** For nonzero real dyadic `q=±p 2^e`, with `p` odd +and positive, Sagar Thakrar's PR696 copy-initialized circuit has real cost + +\[ +c(q)=2+\lfloor\log_2 p\rfloor+\operatorname{popcount}(p)+|e| +-[p=1\text{ and }e=0]. +\] + +Thus `c(2q)-c(q) ≤ 2`; equality occurs at `q=±1`. Ignoring this unit discount +would incorrectly replace two by one. A real or purely imaginary complex ADD +costs `2c(q)`, with signs or exchanged source channels as appropriate. + +For coefficient `q(1+i)`, form each real source-channel product once, add it +to both target channels with the required signs, then clear its work register. +This inserts one accumulation into each PR696 word, for cost `2c(q)+2`. When +`|q|=1`, use the source directly twice and clear its initially dirty work. +The signs in `q(1-i)` and multiplication by `i^j` have the same cost. +[model.py](model.py) emits these circuits. Each has the full six-real-register +map `(T,S,W) -> (T+zS,S,0)`; it assumes neither clean work nor independent data. +The cost is for this explicit lowering, not a lower bound for all Gaussian +ADD circuits. + +**3. Standalone boundaries have an exact minimum.** The real matrix of +multiplication by `g_h` has determinant `2^(2a_h+b_h)`. Signed additions and +negation do not change the determinant's power of two; each doubling or halving +changes it by one. Each boundary therefore costs at least `|2a_h+b_h|` such +operations. If `b_h=1`, all four matrix entries are nonzero, requiring at least +two additions: diagonal operations and one shear cannot make both off-diagonal +entries nonzero. Entry and exit together cost at least + +\[ +B(a,b)=2|2a+b|+4b. +\] + +The lower bound is attained at phase zero. For `a≥0`, first scale both +coordinates by `2^a`, then apply +`y+=x; x*=2; x-=y`, which multiplies by `1+i`. For `a≤-1`, first scale by +`2^(a+1)`, then apply `x-=y; x/=2; y+=x`, which multiplies by `(1+i)/2`. +Reverse the word and invert each elementary operation for the exit. Real +gauges use direct scaling and its inverse, costing `4|a|`. Other unit phases +cannot beat the lower bound and have identical internal ADD costs, so phase +zero suffices for the optimum. + +**4. Round all odd gauges with the same bit.** Discard unit phases and define +two real assignments `g_h^(θ)=2^(a_h+θ b_h)`, for a single common `θ=0,1`. +An original coefficient `q` on `source -> target` becomes `q g_target/g_source`. +If both endpoints have the same `b`, their factor of `1+i` cancels and the two +rounded costs equal the Gaussian cost. If the `b`s differ, the Gaussian +coefficient is a unit phase times `r(1±i)`, while the two rounded coefficients +have magnitudes `|r|,|2r|`. Consequently their average complex cost is + +\[ +c(r)+c(2r)\le 2c(r)+2, +\] + +the charged Gaussian cost. Shared edges between two gauged helpers are included; +rounding helpers independently would invalidate the equal-parity case. + +For a real gauge, boundary costs are unchanged. For an odd gauge, the average +rounded boundary cost is `2|a|+2|a+1|=2|2a+1|`, since `a` is integral. Its +Gaussian boundary costs at least four more. Sum over all ADDs and helpers, +then add the unchanged scalar costs, to obtain the stated inequality. +At least one of the two rounded complete assignments is no more expensive than +their average. The real assignments are themselves in the Gaussian-unit class, +so the unconstrained scalar-cost infima agree. This does not prove that an +external admissibility predicate is closed under rounding. + +## Finite coverage and verification + +For one helper, the real objective is `4|k|` plus its incident real-ADD deltas. +The odd objective is `2|2a+1|+4` plus the incident shared-product deltas. Both +are affine between integer coefficient-exponent breakpoints; unit discounts +only lower breakpoint values. The odd boundary kink is at `-1/2`, so include +both `-1,0`. The two outward tail slopes are `4+2d`, where `d` is the number of +incident ADDs. Every integer minimum is therefore attained in the recorded +finite breakpoint set. No heuristic cutoff or random search is used. + +[CERTIFICATE.json](CERTIFICATE.json) records 5,166 breakpoint evaluations across +both orientations, the complete minima, actual emitted primitive-stream hashes, +unchanged paid histograms, and eight simultaneous common-rounding fixtures. +The baseline, real winner and odd winner each pass all 712 formal complex input +columns (equivalently 1,424 real columns), including 480 arbitrary dirty helpers +and eight private centers. All 464 distinct macro fixtures check six real input +columns, including both arbitrary dirty work registers; 66 boundary pairs check +their exact maps and inverses. The complete literal positive envelopes remain +52 bits forward and 68 backward for all three variants; the inherited 192-bit +charge is retained. These finite envelopes do not discharge the all-size +precision/tape obligation. + +[independent.py](independent.py) separately reconstructs the helper domain and +incident coefficients, enumerates all integers in a provably sufficient interval, +and prices them by the literal pinned PR696 lowerer. It uses neither the +producer's cost formula nor its breakpoint search. [INDEPENDENT.json](INDEPENDENT.json) +records 13,684 grid evaluations, 1,115,016 incident-term evaluations, 2,532 +literal coefficients, and 3,488 distinct Gaussian inputs classified by checking +their actual reciprocal (64 units, 3,424 nonunits). Both implementations are by +the same AI-assisted author; this is not independent human review. + +Sixteen controls reject missing product initialization, omitted accumulation, +wrong cross-channel sign, uncleared dirt, missing/inaccurate inverse boundaries, +aliasing, invalid coefficient support, nondyadic coefficients, Gaussian nonunits, +zero factors, a false unit-cost inequality, false independent rounding, and +missing or modified source bindings. Certificates are compared canonically; +compressed output equality is based on decompressed content. + +## Reproduce + +From the repository root, with Python 3.12 and no third-party dependencies: + +```sh +python3.12 scripts/research_package.py --package research/k8-gaussian-unit-rounding-seed24 +``` + +The three registered commands print: + +```text +PASS_GAUSSIAN_UNIT_COMMON_ROUNDING helpers=237 orientations=2 real_saving=332 odd_saving=58 controls=16 +PASS_INDEPENDENT_LITERAL_GAUSSIAN_GRID +PASS_GAUSSIAN_PACKAGE_CONTROLS read_only_export=2 corrupted_artifacts=3 equivalent_gzip=1 +``` + +Direct `python3 -I -O -B research/k8-gaussian-unit-rounding-seed24/verify.py` +and the corresponding `independent.py` command are also supported. Default +replay is read-only and offline. `--write` on either script regenerates only +this package's own receipts. Metadata/provenance checking uses full Git history; +direct replay needs only the package and the pinned input files. + +This is a scalar circuit result and a scoped cost obstruction. Native/global +admission, the selected cold replay, compiler/realization, whole-call hosting, +roundoff, tape, recovery and analytic obligations have not been newly verified. +No supplier is installed, no selected certificate is changed, and no κ gain, +arbitrary-circuit optimum or Lean multiplication theorem is claimed. + +## Open next questions + +Can sharing a coefficient product **across distinct ADD macros**, while restoring +all dirty state and respecting chronological frames, break the inequality used +here? A useful first test would be an explicit two-ADD word whose complete bill +beats the sum of the two macro bills. That needs a new local interface and full +frame/precision accounting; a larger static Gaussian exponent search adds no +new evidence within this class. + +Can a joint boundary circuit across multiple helpers reduce the sum of the +standalone determinant charges? Opposite determinant exponents make this a +different problem. Start with two helpers and an exact four-real-register +boundary map; all source restoration and subsequent coefficients must be priced. +Neither possible escape is asserted to work. Structured questions and the +changed catalogue scope are in [TASK.json](TASK.json). + +## Credit and disclosure + +Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance in the argument, +implementation, verification and writing. New work is Apache-2.0. Credit +Sagar Thakrar's PR696 coefficient lowering; woklerx's +[PR1161](https://github.com/CrocSwap/integer-mult-bounds/pull/1161) +at `d210969d3158a1e6c505e41f67dd84e555c88564`; Hanson's +[PR1214](https://github.com/CrocSwap/integer-mult-bounds/pull/1214) +at `26162c56ec9c50a80e49949f36d4dd9a137a76a6`; and the retained complex-supplier +lineage of icekylinx, Jeremy Kothe, Rohan Arun and the other contributors credited +in Douglas Colkitt's PR1094 review. No pending predecessor implementation is +vendored or required. Source licenses and frozen evidence remain unchanged. diff --git a/research/k8-gaussian-unit-rounding-seed24/SOURCES.json b/research/k8-gaussian-unit-rounding-seed24/SOURCES.json new file mode 100644 index 0000000000..922baea812 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "input", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1042-audit/RESULT.json", + "usage": "input", + "git_blob": "8182d0818c0cbda7e52c10120f15b2c3a2c8f933", + "sha256": "bf12c6ed3b412539638b76addb40591a631609b2ab9e5ee0db1f6bbe067d0ec0" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/community-frontier1094-audit/RESULT.json", + "usage": "input", + "git_blob": "131d9c96a54632ae385ced4138fd7f30ad448a3e", + "sha256": "1e3e47e9ec24bcb6fb5f703b7fce0aab658d84ff72bfae5da3ae429d17b6e752" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + }, + { + "path": "research/complex-dyadic-lowering/README.md", + "usage": "input", + "git_blob": "18999b7d252471054af43dea926d81efdf292c2b", + "sha256": "798209e9869d1612a2c34412ef2eb87c0eb0dcebcbed9963a45e0fe248326c2f" + }, + { + "path": "research/complex-dyadic-lowering/lower.py", + "usage": "input", + "git_blob": "a2c2889e5be41a0fc30d4dfa5dfcebb03d6d47f8", + "sha256": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753" + } + ] +} diff --git a/research/k8-gaussian-unit-rounding-seed24/TASK.json b/research/k8-gaussian-unit-rounding-seed24/TASK.json new file mode 100644 index 0000000000..14032c27eb --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/TASK.json @@ -0,0 +1,132 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 2, + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract, not another mixture already covered by the frozen catalogue.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the frozen catalogue bound exclusions and select one genuinely different helper endpoint inventory.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write the complete optimistic child histogram and reject it immediately if even the relaxation has insufficient headroom.", + "bottleneck_link": "Helper inventory changes can improve the moment; repacking a covered cost interface cannot evade its scoped bound.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Static Gaussian-dyadic unit helper gauges with shared-product macro lowering and independent two-real-register boundaries; common-rounding cost theorem and exact k8 single-helper census.", + "scope_change_reason": "The user explicitly assigned the complex-supplier track and permits scoped circuit negative results. This is a scalar-circuit side result rather than the catalogue card's changed paid helper inventory; the recursive profile stays fixed.", + "bottleneck_link": "Rules out Gaussian unit coefficient-field extension as an intrinsic scalar-cost improvement within this lowering/boundary class. It does not improve the paid recursive moment or approach kappa > 0.01.", + "budget_minutes": 60, + "stop_rule": "Stop after the complete unit normal-form and rounding argument, all 237 eligible single-helper integer domains in both orientations, exact finite circuit checks, independent literal census, controls and one PR. No heuristic search or arbitrary Gaussian circuit synthesis.", + "outcome": "negative-result", + "evidence": "Written argument in README.md; exact CERTIFICATE.json and CENSUS.json.gz; separately implemented literal grid in INDEPENDENT.json.", + "author": "Hanson Sun (@bbMisk)", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, code, verification and writing. Separate implementations by the same AI-assisted author; no independent human review or formal proof assistant.", + "open_questions": [ + { + "question": "Can product reuse across two distinct Gaussian ADD macros beat the sum of their macro-local bills?", + "why_it_matters": "This would change the key edge-cost premise of the rounding theorem.", + "first_step": "Exhibit one exact two-ADD word and complete dirty-state primitive invoice.", + "blocked_by": "Requires chronological frame legality, source restoration and precision/hosting costs; no such improvement is claimed." + }, + { + "question": "Can joint boundaries across helpers beat the independent two-register determinant charges?", + "why_it_matters": "Opposite determinant exponents may permit a different boundary interface.", + "first_step": "Synthesize one exact four-real-register entry/exit pair and price all conjugated ADDs.", + "blocked_by": "The present theorem excludes cross-helper boundary sharing; a circuit and full interface proof are missing." + } + ], + "assignment_seed": 24, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "started_at_utc": "2026-10-14T01:00:55.081120+00:00", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1163#discussioncomment-18912584", + "track": "Complex supplier, user allocation 20-39", + "candidate_tasks": [ + { + "task": "Gaussian-dyadic unit extension of static helper rescaling", + "decision": "selected by 24 mod 3 = 0; new coefficient class and common-rounding method" + }, + { + "task": "Temporal two-helper gauge composition", + "decision": "deferred; overlaps PR1380/1408" + }, + { + "task": "Masked P112 rank-eight extension", + "decision": "deferred; active Discussion1411 and PR1419/1425" + } + ], + "predecessors": [ + { + "pr": 1161, + "head": "d210969d3158a1e6c505e41f67dd84e555c88564", + "credit": "woklerx; one-helper real dyadic optimum and source binding" + }, + { + "pr": 1214, + "head": "26162c56ec9c50a80e49949f36d4dd9a137a76a6", + "credit": "Hanson Sun; eligible two-helper dyadic domain" + }, + { + "pr": 696, + "path": "research/complex-dyadic-lowering/lower.py", + "credit": "Sagar Thakrar; exact copy-initialized coefficient lowering, pinned on main" + } + ], + "outcome_description": "Scoped negative result with attained odd-class finite witnesses; real single-helper record independently corroborated.", + "overlap": { + "initial_complete_open_pr_snapshot": { + "records": 823, + "fetched_at": "2026-10-14T01:04:22.002089+00:00" + }, + "final_discussions": { + "fetched_at": "2026-10-14T01:33:43.603581+00:00", + "complete_pagination": true, + "records": 173 + }, + "full_pr_refresh_limitation": "The overlap helper and REST full pagination returned HTTP 500. The earlier complete snapshot was supplemented by the newest 50 open PRs ordered by updated_at.", + "fresh_updated_prs": { + "records": 50, + "fetched_at": "2026-10-14T01:38:25Z", + "oldest_updated_at": "2026-10-14T00:51:37Z", + "newest_updated_at": "2026-10-14T01:37:49Z", + "covers_updates_since_initial_snapshot": true, + "snapshot_sha256": "4d76f270eff9cef016bd5a16bc01582d5995be505baf4aca51074d759a43746e" + }, + "terms": [ + "Gaussian unit", + "Gaussian-unit", + "Gaussian helper", + "static Gaussian", + "shared-product", + "common rounding" + ], + "disposition": "No matching external scope found. Own package/claim match. Discussion1462 concerns truncation commuting with linear maps, not helper gauge cost. PR1469/1474 concern masked decoder rigidity; PR309/1172 concern physical response/owner gauges. Searches do not cover arbitrary code diffs or establish novelty." + } +} diff --git a/research/k8-gaussian-unit-rounding-seed24/VALIDATION.json b/research/k8-gaussian-unit-rounding-seed24/VALIDATION.json new file mode 100644 index 0000000000..e55aca66d0 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/VALIDATION.json @@ -0,0 +1,55 @@ +{ + "status": "PASS_LOCAL_SCOPED_VERIFICATION", + "base_commit": "410026dc5513b87db92ae98571d1d5984c69a983", + "registered_python": "3.12.13", + "host_platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "registered_replay": { + "command": "python3.12 scripts/research_package.py --package research/k8-gaussian-unit-rounding-seed24", + "exit_code": 0, + "elapsed_seconds": 64.488, + "output": "CHECK Exact Gaussian primitive circuits, complete selected-word scalar columns/invoices, breakpoint certificate and sixteen rejection controls.\nPASS_GAUSSIAN_UNIT_COMMON_ROUNDING helpers=237 orientations=2 real_saving=332 odd_saving=58 controls=16\nCHECK Separate literal-lowerer integer census, source domain, tails and reciprocal unit membership.\nPASS_INDEPENDENT_LITERAL_GAUSSIAN_GRID\nCHECK Optimized read-only relocated export, actual source/certificate/census corruptions and canonical gzip equivalence.\nPASS_GAUSSIAN_PACKAGE_CONTROLS read_only_export=2 corrupted_artifacts=3 equivalent_gzip=1\nPASS_REGISTERED_RESEARCH_PACKAGE research/k8-gaussian-unit-rounding-seed24 outcome=negative-result\n" + }, + "optimized_default_python": { + "command": [ + "/opt/homebrew/opt/python@3.14/bin/python3.14", + "-I", + "-O", + "-B", + "research/k8-gaussian-unit-rounding-seed24/verify.py" + ], + "python": "3.14.6 (main, Jun 10 2026, 10:03:53) [Clang 21.0.0 (clang-2100.0.123.102)]", + "exit_code": 0, + "elapsed_seconds": 12.725, + "stdout": "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING helpers=237 orientations=2 real_saving=332 odd_saving=58 controls=16\n", + "stderr": "" + }, + "additional_checks": { + "ruff": "pass", + "git_diff_check": "pass", + "selected_result_checker": "pass; selected certificate unchanged", + "optimized_python314_independent_grid": "pass" + }, + "upstream_compatibility": { + "fetched_main": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "base_to_main_diff_on_live_inputs_selected_record_AGENTS_CONTRIBUTING_and_replay_runner": "empty" + }, + "scientific_artifacts_sha256": { + "model.py": "246803b9ca3f14984d9460173923f3f726bdcf15307b28a64fb5ecb3a761c9fe", + "verify.py": "a1630c4492bd35b86d624f3dcc60b18e468d6abdd16645a5442a0482155b88d3", + "independent.py": "7fb0f45c5dada54a2df3f6053279aa688ec83561f7c6e944e76b9157acbad2be", + "test_package.py": "f9cc696ceb9a24afd17d73ea8b0d1276feabb909e9afd93c514c1de7eb5f00d7", + "CERTIFICATE.json": "1135b004e367aa7c4b6bc953b7f0b21ceb5c22953584391d105e7f9f8c70907c", + "CENSUS.json.gz": "551606e065f1436de6568b83bbebc3988226dcc54e30052481142699ccdc84ad", + "INDEPENDENT.json": "3b0ee5801584db9cb5f99dd5a412e128ed5971962478d4ba1d2951f45674e0e0", + "SOURCES.json": "4cd986939bc423341b7e1469f82652a4469249d46fff370b3d71f1296f28a037", + "VERIFY.json": "a8ff996c8e1c0040f06a59a98d89f0fa3fe33743bb305ca73f57ad7da53bad99" + }, + "not_run": [ + "Selected full native/global cold replay", + "Native Gaussian supplier admission", + "New global assembly or kappa certification", + "Lean formalization", + "Hosted CI (separate from these local results)" + ], + "writing": "Argument and scope independently checked against executable evidence; substantial AI assistance disclosed." +} diff --git a/research/k8-gaussian-unit-rounding-seed24/VERIFY.json b/research/k8-gaussian-unit-rounding-seed24/VERIFY.json new file mode 100644 index 0000000000..976451f9bb --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/VERIFY.json @@ -0,0 +1,47 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/community-batch1099-review.md", + "research/community-frontier1042-audit/RESULT.json", + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/community-frontier1094-audit/RESULT.json", + "research/community-frontier1094-audit/selected-replay.tar.gz", + "research/complex-dyadic-lowering/README.md", + "research/complex-dyadic-lowering/lower.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact Gaussian primitive circuits, complete selected-word scalar columns/invoices, breakpoint certificate and sixteen rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 240, + "checks": "Separate literal-lowerer integer census, source domain, tails and reciprocal unit membership." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 600, + "checks": "Optimized read-only relocated export, actual source/certificate/census corruptions and canonical gzip equivalence." + } + ] +} diff --git a/research/k8-gaussian-unit-rounding-seed24/independent.py b/research/k8-gaussian-unit-rounding-seed24/independent.py new file mode 100644 index 0000000000..e604c56192 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/independent.py @@ -0,0 +1,170 @@ +#!/usr/bin/env python3 +"""Literal-lowerer grid audit, separately implemented by the same AI-assisted author. + +It shares source authentication with model.py, but not its cost formula, helper +selection, incidence extraction, breakpoint search, Gaussian lowering or replay. +Hanson Sun with OpenAI Codex; Apache-2.0. PR696 lowerer: Sagar Thakrar. +""" +from fractions import Fraction +from functools import lru_cache +import gzip +import importlib.util +import json +from pathlib import Path +import sys +import tarfile + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import model + + +def insist(ok, message): + if not ok: + raise ValueError(message) + + +def run(): + model.check_sources() + root = model.ROOT + with tarfile.open(root / model.ARCHIVE1042) as archive: + programs = json.loads(gzip.decompress(archive.extractfile("slots/local/LOCAL-PROGRAMS.json.gz").read())) + word = json.loads(gzip.decompress(archive.extractfile("slots/local/CANONICAL-WORD.json.gz").read())) + spec = importlib.util.spec_from_file_location("independent_pr696", root / model.LOWER) + lowerer = importlib.util.module_from_spec(spec) + spec.loader.exec_module(lowerer) + census = json.loads(gzip.decompress((model.HERE / "CENSUS.json.gz").read_bytes())) + certificate = json.loads((model.HERE / "CERTIFICATE.json").read_bytes()) + + @lru_cache(maxsize=None) + def literal(q): + return len(lowerer.lower(["add", ("target",), ("source",), + q.numerator, q.denominator], work=("work",))) + + def two(k): + return Fraction(2 ** k) if k >= 0 else Fraction(1, 2 ** -k) + + # Reconstruct the exclusion contract register by register, not by using the + # producer's domain routine or the supplied helper list. + eligible = [] + for h in range(224, 704): + if h in word["centers"] or word["start"][h] != 0 or word["final"][h] != 1: + continue + blocked = False + for events in programs.values(): + for event in events: + if event[0] == "residual_adapter" and event[2] == h: + blocked = True + elif event[0] == "scalar" and event[1][0] in ("copy", "clear") and ["L", h] in event[1][1:]: + blocked = True + if not blocked: + eligible.append(h) + insist(eligible == certificate["eligible_helpers"] and len(eligible) == 237, "independent helper domain") + summary = {"helper_count": len(eligible), "orientations": {}} + for orientation, events in programs.items(): + target_terms = {h: [] for h in eligible} + source_terms = {h: [] for h in eligible} + baseline = 0 + for event in events: + if event[0] != "scalar": + continue + op = event[1] + baseline += 2 * len(lowerer.lower(op)) + if op[0] == "add": + q = Fraction(op[3], op[4]) + if op[1][0] == "L" and op[1][1] in target_terms: + target_terms[op[1][1]].append(q) + if op[2][0] == "L" and op[2][1] in source_terms: + source_terms[op[2][1]].append(q) + insist(baseline == certificate["orientations"][orientation]["programs"]["baseline"]["invoice"]["complex_scalar_primitives"], "literal full baseline") + rows = {r["helper"]: r for r in census[orientation]} + grid_evaluations = 0 + term_evaluations = 0 + critical_rows = [] + for h in eligible: + incoming, outgoing = target_terms[h], source_terms[h] + all_terms = incoming + outgoing + exponents = [] + for q in all_terms: + n, d, exponent = abs(q.numerator), q.denominator, 0 + while n % 2 == 0: + n //= 2 + exponent += 1 + while d > 1: + insist(d % 2 == 0, "dyadic source") + d //= 2 + exponent -= 1 + exponents.append(exponent) + radius = max([abs(e) for e in exponents] + [0]) + 3 + lo, hi = -radius, radius + original = 2 * sum(literal(q) for q in all_terms) + + def r(k): + return 4 * abs(k) + 2 * sum(literal(q * two(k)) for q in incoming) + 2 * sum(literal(q / two(k)) for q in outgoing) - original + + def g(a): + # Two copies of the exact predecessor coefficient circuit, + # one extra target accumulation each, and optimal boundaries. + return 2 * abs(2 * a + 1) + 4 + sum(2 * literal(q * two(a)) + 2 for q in incoming) + sum(2 * literal(q / two(a + 1)) + 2 for q in outgoing) - original + + real_grid = [(k, r(k)) for k in range(lo, hi + 1)] + odd_grid = [(a, g(a)) for a in range(lo, hi + 1)] + def key(pair): + return pair[1], abs(pair[0]), pair[0] + insist(list(min(real_grid, key=key)) == rows[h]["real_best"], "independent real minimum") + insist(list(min(odd_grid, key=key)) == rows[h]["odd_best"], "independent odd minimum") + for k, value in rows[h]["real_candidates"]: + insist(lo <= k <= hi and r(k) == value, "real breakpoint receipt") + for a, value in rows[h]["odd_candidates"]: + insist(lo <= a <= hi and g(a) == value, "odd breakpoint receipt") + slope = 4 + 2 * len(all_terms) + for cost in (r, g): + insist(cost(lo - 1) - cost(lo) == slope and cost(hi + 1) - cost(hi) == slope, + "independent outward tails") + for a in range(lo, hi + 1): + insist(2 * g(a) >= r(a) + r(a + 1) + 8, "single-helper common rounding") + grid_evaluations += len(real_grid) + len(odd_grid) + term_evaluations += (len(real_grid) + len(odd_grid)) * len(all_terms) + critical_rows.append([h, lo, hi, min(real_grid, key=key), min(odd_grid, key=key)]) + summary["orientations"][orientation] = { + "complete_scalar_baseline": baseline, "integer_grid_evaluations": grid_evaluations, + "incident_term_evaluations": term_evaluations, + "grid_rows_sha256": model.sha(model.canonical(critical_rows))} + + # Independently decide unit membership by computing the actual reciprocal, + # then compare the normal-form implementation on a finite exact domain. + units = nonunits = 0 + seen = set() + for denominator_exponent in range(4): + for re in range(-16, 17): + for im in range(-16, 17): + z = Fraction(re, 2 ** denominator_exponent), Fraction(im, 2 ** denominator_exponent) + if z == (0, 0) or z in seen: + continue + seen.add(z) + norm = z[0] * z[0] + z[1] * z[1] + reciprocal = z[0] / norm, -z[1] / norm + is_unit = all(q.denominator & (q.denominator - 1) == 0 for q in reciprocal) + try: + coordinates = model.unit_coordinates(z) + except ValueError: + insist(not is_unit, "unit wrongly rejected") + nonunits += 1 + else: + insist(is_unit and model.gauge(*coordinates) == z, "nonunit or wrong normal form") + units += 1 + summary["unit_membership_grid"] = {"distinct_nonzero_inputs": len(seen), "units": units, "nonunits": nonunits, + "numerators": [-16, 16], "common_denominator_exponents": [0, 3]} + summary["literal_distinct_coefficients"] = literal.cache_info().currsize + summary["status"] = "PASS_INDEPENDENT_LITERAL_GAUSSIAN_GRID" + return summary + + +if __name__ == "__main__": + result = run() + path = model.HERE / "INDEPENDENT.json" + if sys.argv[1:] == ["--write"]: + path.write_text(json.dumps(result, indent=2) + "\n") + else: + insist(sys.argv[1:] in ([], ["--json"]), "arguments") + insist(result == json.loads(path.read_bytes()), "independent receipt mismatch") + print(json.dumps(result, indent=2) if sys.argv[1:] == ["--json"] else result["status"]) diff --git a/research/k8-gaussian-unit-rounding-seed24/model.py b/research/k8-gaussian-unit-rounding-seed24/model.py new file mode 100644 index 0000000000..72bc4d22de --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/model.py @@ -0,0 +1,400 @@ +"""Static Gaussian-unit gauges, Hanson Sun with OpenAI Codex, Apache-2.0. + +The real macro lowering is Sagar Thakrar's PR696; the local word is the +source-bound PR1094/1042 k8 word. No pending PR implementation is imported. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from functools import lru_cache +import copy +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "410026dc5513b87db92ae98571d1d5984c69a983" +ARCHIVE1042 = "research/community-frontier1042-audit/selected-replay.tar.gz" +ARCHIVE1094 = "research/community-frontier1094-audit/selected-replay.tar.gz" +LOWER = "research/complex-dyadic-lowering/lower.py" +INPUTS = frozenset((ARCHIVE1042, ARCHIVE1094, LOWER, + "research/community-frontier1042-audit/RESULT.json", + "research/community-frontier1094-audit/RESULT.json", + "research/complex-dyadic-lowering/README.md", + "docs/research/community-batch1099-review.md")) +MEMBERS = ("CANONICAL-WORD.json.gz", "LOCAL-PROGRAMS.json.gz", + "INDEPENDENT-LOCAL-REPLAY.json", "LOCAL-CHECKS.json") +ZERO = (Q(0), Q(0)) +ONE = (Q(1), Q(0)) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":"), + allow_nan=False).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def check_sources(manifest=None, reader=None): + manifest = manifest or json.loads((HERE / "SOURCES.json").read_bytes()) + reader = reader or (lambda p: (ROOT / p).read_bytes()) + require(manifest["base_commit"] == BASE, "base commit") + rows = [r for r in manifest["files"] if r["usage"] == "input"] + require(len(rows) == len(INPUTS) and {r["path"] for r in rows} == INPUTS, + "source inventory") + for r in rows: + data = reader(r["path"]) + require(sha(data) == r["sha256"], "source SHA256: " + r["path"]) + blob = hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + require(blob == r["git_blob"], "source Git blob: " + r["path"]) + return manifest + + +def load(): + check_sources() + raw = {} + with tarfile.open(ROOT / ARCHIVE1042) as archive: + for name in MEMBERS: + raw[name] = archive.extractfile("slots/local/" + name).read() + with tarfile.open(ROOT / ARCHIVE1094) as archive: + for name in MEMBERS: + actual = archive.extractfile( + "candidate/strict/global8/base/providers/gauge44/" + name).read() + require(actual == raw[name], "selected provider alias: " + name) + objects = {n: json.loads(gzip.decompress(b) if n.endswith(".gz") else b) + for n, b in raw.items()} + word, programs, replay, checks = (objects[n] for n in MEMBERS) + old = (ROOT / "research/community-frontier1042-audit/RESULT.json").read_bytes() + current = json.loads((ROOT / "research/community-frontier1094-audit/RESULT.json").read_bytes()) + require(current["baseline_receipt_sha256"] == sha(old), "baseline receipt binding") + require(json.loads(old)["status"] == "PASS_COMPLETE_PR1042_COMPOSITION" and + current["status"] == "PASS_COMPLETE_PR1094_COMPOSITION", "retained receipt status") + require(replay["canonical_word_sha256"] == sha(raw[MEMBERS[0]]) and + replay["local_programs_sha256"] == sha(raw[MEMBERS[1]]), "native receipt binding") + require((word["v"], word["h"], word["R"]) == (112, 9, 480), "source geometry") + require(set(programs) == {"forward", "backward"}, "orientations") + bindings = {n: {"archive_member_sha256": sha(b), + "payload_sha256": sha(gzip.decompress(b) if n.endswith(".gz") else b)} + for n, b in raw.items()} + return word, programs, bindings, replay, checks + + +def domain(word, programs): + excluded = set(word["centers"]) + for events in programs.values(): + for event in events: + if event[0] == "residual_adapter": + excluded.add(event[2]) + if event[0] == "scalar" and event[1][0] in ("copy", "clear"): + excluded.update(r[1] for r in event[1][1:] + if isinstance(r, list) and r[0] == "L") + return [h for h in range(224, 704) if h not in excluded + and word["start"][h] == 0 and word["final"][h] == 1] + + +def power(e): + return Q(2 ** e) if e >= 0 else Q(1, 2 ** -e) + + +def parts(q): + q = Q(q) + p = abs(q.numerator) + require(p > 0 and q.denominator & (q.denominator - 1) == 0, "nonzero dyadic") + twos = (p & -p).bit_length() - 1 + return p >> twos, twos - (q.denominator.bit_length() - 1) + + +def c_parts(p, e): + require(p > 0 and p % 2 == 1, "positive odd numerator") + return 2 + p.bit_length() - 1 + p.bit_count() + abs(e) - int(p == 1 and e == 0) + + +def c(q): + return c_parts(*parts(q)) + + +def mul(x, y): + return x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0] + + +def inv(x): + d = x[0] ** 2 + x[1] ** 2 + require(d != 0, "nonzero Gaussian factor") + return x[0] / d, -x[1] / d + + +def gauge(a, odd, phase=0): + require(odd in (0, 1) and phase in range(4), "Gaussian-unit parameters") + return mul((power(a), power(a) if odd else Q(0)), + (ONE, (Q(0), Q(1)), (Q(-1), Q(0)), (Q(0), Q(-1)))[phase]) + + +def gaussian_add_cost(z): + if z[0] == 0 or z[1] == 0: + return 2 * c(z[0] or z[1]) + require(abs(z[0]) == abs(z[1]), "axis or diagonal Gaussian coefficient") + return 2 * c(z[0]) + 2 + + +def unit_coordinates(z): + """Normal form for units of Z[1/2,i]; rejects nonunits.""" + require(z != ZERO, "nonzero Gaussian unit") + if z[0] == 0 or z[1] == 0: + p, a = parts(z[0] or z[1]) + require(p == 1, "Gaussian dyadic unit norm") + phase = (0 if z[0] > 0 else 2) if z[1] == 0 else (1 if z[1] > 0 else 3) + return a, 0, phase + require(abs(z[0]) == abs(z[1]), "Gaussian dyadic unit diagonal") + p, a = parts(z[0]) + require(p == 1, "Gaussian dyadic unit norm") + phase = {(True, True): 0, (False, True): 1, + (False, False): 2, (True, False): 3}[z[0] > 0, z[1] > 0] + return a, 1, phase + + +def terms_by_helper(events): + terms = defaultdict(list) + for event in events: + if event[0] == "scalar" and event[1][0] == "add": + g = event[1] + require(g[1] != g[2], "distinct ADD operands") + p, e = parts(Q(g[3], g[4])) + for r, sign in ((g[1], 1), (g[2], -1)): + if r[0] == "L": + terms[r[1]].append((p, e, sign)) + return terms + + +def real_delta(terms, k): + return 4 * abs(k) + 2 * sum(c_parts(p, e + s * k) - c_parts(p, e) + for p, e, s in terms) + + +def odd_delta(terms, a): + # The two-register boundary minimum is attained by boundary_word below. + return 2 * abs(2 * a + 1) + 4 + sum( + 2 * c_parts(p, e + s * a - int(s < 0)) + 2 - 2 * c_parts(p, e) + for p, e, s in terms) + + +def census(events, helpers): + by_helper = terms_by_helper(events) + rows = [] + for helper in helpers: + terms = by_helper[helper] + real_points = sorted({0} | {-s * e for p, e, s in terms}) + odd_points = sorted({-1, 0} | {-s * e - int(s < 0) for p, e, s in terms}) + real = [[k, real_delta(terms, k)] for k in real_points] + odd = [[a, odd_delta(terms, a)] for a in odd_points] + rows.append({"helper": helper, "incident_adds": len(terms), + "real_candidates": real, "odd_candidates": odd, + "real_best": min(real, key=lambda x: (x[1], abs(x[0]), x[0])), + "odd_best": min(odd, key=lambda x: (x[1], abs(x[0]), x[0])), + "outward_tail_slope": 4 + 2 * len(terms)}) + return rows + + +def boundary_word(a, odd, target=("X",)): + """Exact minimum for phase-zero gauge and its inverse; no work register.""" + x, y = tuple(target) + (0,), tuple(target) + (1,) + if not odd: + e = a + result = [] + elif a >= 0: + e = a + result = [("add", y, x), ("double", x), ("subtract", x, y)] + else: + e = a + 1 + result = [("subtract", x, y), ("halve", x), ("add", y, x)] + scales = [("double" if e > 0 else "halve", r) + for r in (x, y) for _ in range(abs(e))] + forward = scales + result + inverse_tag = {"add": "subtract", "subtract": "add", "double": "halve", "halve": "double"} + backward = [(inverse_tag[g[0]], *g[1:]) for g in reversed(forward)] + expected = 2 * abs(2 * a + 1) + 4 if odd else 4 * abs(a) + require(len(forward) + len(backward) == expected, "boundary determinant/shear lower bound") + return forward, backward + + +@lru_cache(maxsize=1) +def real_lowerer(): + spec = importlib.util.spec_from_file_location("pinned_pr696_lower", ROOT / LOWER) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module.lower + + +def lower_gaussian(z, target=("T",), source=("S",)): + """Share each source-channel product across both targets, then clear work. + + Uses exactly the two existing real coefficient-work registers. Each may be + arbitrarily dirty on entry. Target/source complex registers must be distinct. + """ + require(tuple(target) != tuple(source), "distinct complex operands") + require(z != ZERO, "nonzero Gaussian ADD") + require(z[0] == 0 or z[1] == 0 or abs(z[0]) == abs(z[1]), "Gaussian support") + out = [] + for channel, coefficients in enumerate(((z[0], z[1]), (-z[1], z[0]))): + src = tuple(source) + (channel,) + work = ("W", channel) + entries = [(tuple(target) + (i,), q) for i, q in enumerate(coefficients) if q] + dst, q = entries[0] + word = real_lowerer()(["add", dst, src, q.numerator, q.denominator], work=work) + if len(entries) == 2: + other, coefficient = entries[1] + require(abs(coefficient) == abs(q), "shared product magnitude") + operand = src if abs(q) == 1 else work + word.insert(len(word) - 1, + ("add" if coefficient > 0 else "subtract", other, operand)) + out.extend(word) + require(len(out) == gaussian_add_cost(z), "Gaussian primitive invoice") + return out + + +def transformed(events, gauges): + """Return scalar Gaussian macros; non-scalar events remain unchanged.""" + factors = {("L", h): gauge(a, odd) for h, (a, odd) in gauges.items()} + stream = [] + for event in events: + if event[0] != "scalar": + stream.append(copy.deepcopy(event)) + continue + g = event[1] + tag, target = g[0], tuple(g[1]) + if tag == "add": + source = tuple(g[2]) + z = mul((Q(g[3], g[4]), Q(0)), + mul(factors.get(target, ONE), inv(factors.get(source, ONE)))) + op = [tag, list(target), list(source), [z[0].numerator, z[0].denominator], + [z[1].numerator, z[1].denominator]] + elif tag == "scale": + op = [tag, list(target), [g[2], g[3]], [0, 1]] + else: + require(tag in ("clear", "copy"), "scalar opcode") + require(not any(tuple(r) in factors for r in g[1:] if isinstance(r, list)), + "no gauge on copy/clear carrier") + op = copy.deepcopy(g) + stream.append(["scalar", op, *event[2:]]) + return stream + + +def replay(stream, gauges, orientation): + """Exact complex-linear maps: 712 complex columns = 1424 real columns.""" + rows = {("L", i): {i: ONE} for i in range(704)} + rows.update({("C", i): {704 + i: ONE} for i in range(8)}) + + def scale(target, z): + rows[target] = {i: mul(v, z) for i, v in rows[target].items()} + + for helper, (a, odd) in gauges.items(): + scale(("L", helper), gauge(a, odd)) + for event in stream: + if event[0] != "scalar": + continue + g = event[1] + tag, target = g[0], tuple(g[1]) + if tag == "clear": + rows[target] = {} + elif tag == "copy": + rows[target] = dict(rows[tuple(g[2])]) + elif tag == "scale": + scale(target, (Q(*g[2]), Q(*g[3]))) + elif tag == "add": + source = tuple(g[2]) + require(source != target, "distinct replay operands") + z = Q(*g[3]), Q(*g[4]) + for i, value in rows[source].items(): + delta = mul(value, z) + old = rows[target].get(i, ZERO) + new = old[0] + delta[0], old[1] + delta[1] + if new == ZERO: + rows[target].pop(i, None) + else: + rows[target][i] = new + else: + raise ValueError("Gaussian scalar opcode") + for helper, (a, odd) in gauges.items(): + scale(("L", helper), inv(gauge(a, odd))) + for i in range(704): + expected = {i: ONE} + if orientation == "forward" and 112 <= i < 224: + expected[i - 112] = ONE + if orientation == "backward" and i < 112: + expected[i + 112] = (Q(-1), Q(0)) + require(rows["L", i] == expected, "all-column endpoint " + str((orientation, i))) + require(all(not rows["C", i] for i in range(8)), "private centres cleared") + return {"complex_input_columns": 712, "equivalent_real_input_columns": 1424, + "dirty_helper_columns": 480, "all_helpers_restored": True, + "private_centres_cleared": True} + + +def primitive_stream(stream, gauges): + for h, (a, odd) in sorted(gauges.items()): + yield from boundary_word(a, odd, ("L", h))[0] + for event in stream: + if event[0] != "scalar": + continue + g = event[1] + if g[0] == "add": + yield from lower_gaussian((Q(*g[3]), Q(*g[4])), tuple(g[1]), tuple(g[2])) + else: + for channel in range(2): + target = tuple(g[1]) + (channel,) + if g[0] == "scale": + require(g[3] == [0, 1], "real original SCALE") + op = ["scale", target, *g[2]] + elif g[0] == "copy": + op = ["copy", target, tuple(g[2]) + (channel,)] + else: + require(g[0] == "clear", "primitive opcode") + op = ["clear", target] + yield from real_lowerer()(op, work=("W", channel)) + for h, (a, odd) in reversed(sorted(gauges.items())): + yield from boundary_word(a, odd, ("L", h))[1] + + +def invoice(stream, gauges): + env = {("L", i, channel): Q(1) for i in range(704) for channel in range(2)} + env.update({("C", i, channel): Q(1) for i in range(8) for channel in range(2)}) + env.update({("W", channel): Q(1) for channel in range(2)}) + peak, count = Q(1), 0 + digest = hashlib.sha256() + for g in primitive_stream(stream, gauges): + count += 1 + digest.update(canonical(g) + b"\n") + tag, target = g[:2] + if tag in ("add", "subtract"): + env[target] += env[g[2]] + elif tag == "copy": + env[target] = env[g[2]] + elif tag == "clear": + env[target] = Q(0) + elif tag == "double": + env[target] *= 2 + elif tag == "halve": + env[target] /= 2 + else: + require(tag == "negate", "invoice primitive") + peak = max(peak, env[target]) + require(env["W", 0] == env["W", 1] == 0, "coefficient work cleared") + require(peak < 2 ** 192, "inherited 192-bit local envelope") + paid = Counter() + for e in stream: + if e[0] == "climb": + paid[e[5]] += 1 + elif e[0] == "center": + paid[e[4]] += 1 + return {"complex_scalar_primitives": count, "primitive_stream_sha256": digest.hexdigest(), + "positive_prefix_l1": str(peak), + "positive_prefix_bits": peak.numerator.bit_length() - peak.denominator.bit_length() + 1, + "inherited_charged_bits": 192, "paid_profile": dict(sorted(paid.items()))} diff --git a/research/k8-gaussian-unit-rounding-seed24/test_package.py b/research/k8-gaussian-unit-rounding-seed24/test_package.py new file mode 100644 index 0000000000..dc47638141 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/test_package.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Exercise the actual portable commands and corrupted artifacts, without pytest. + +Hanson Sun with OpenAI Codex assistance; Apache-2.0. +""" +import gzip +import hashlib +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +FILES = ("model.py", "verify.py", "independent.py", "CERTIFICATE.json", + "CENSUS.json.gz", "INDEPENDENT.json", "SOURCES.json", "TASK.json", + "VERIFY.json", "README.md") + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def run(script, root, expected, success=True): + env = dict(os.environ, PYTHONHASHSEED="24") + result = subprocess.run([sys.executable, "-I", "-O", "-B", str(script)], + cwd=root, env=env, text=True, capture_output=True, timeout=240) + require((result.returncode == 0) == success and expected in result.stdout + result.stderr, + "subprocess outcome: " + expected + "\n" + result.stdout[-2000:] + result.stderr[-2000:]) + + +def inventory(root): + return {str(p.relative_to(root)): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob("*") if p.is_file()} + + +def writable(root): + for p in [root, *root.rglob("*")]: + p.chmod(0o755 if p.is_dir() else 0o644) + + +def main(): + manifest = json.loads((HERE / "SOURCES.json").read_bytes()) + with tempfile.TemporaryDirectory(prefix="gaussian-unit-package-") as temporary: + root = Path(temporary) + package = root / "research" / HERE.name + package.mkdir(parents=True) + for name in FILES: + shutil.copyfile(HERE / name, package / name) + for row in manifest["files"]: + if row["usage"] != "input": + continue + path = root / row["path"] + path.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / row["path"], path) + try: + before = inventory(root) + for p in root.rglob("*"): + p.chmod(0o555 if p.is_dir() else 0o444) + root.chmod(0o555) + run(package / "verify.py", root, "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING") + run(package / "independent.py", root, "PASS_INDEPENDENT_LITERAL_GAUSSIAN_GRID") + require(inventory(root) == before, "read-only export was changed") + writable(root) + + path = package / "CERTIFICATE.json" + original = path.read_bytes() + bad = json.loads(original) + bad["orientations"]["forward"]["odd_winner"]["delta"] -= 1 + path.write_text(json.dumps(bad)) + run(package / "verify.py", root, "certificate mismatch", success=False) + path.write_bytes(original) + + path = package / "CENSUS.json.gz" + original = path.read_bytes() + payload = json.loads(gzip.decompress(original)) + # Header, compression and JSON whitespace are not mathematical data. + path.write_bytes(gzip.compress(json.dumps(payload, indent=1).encode(), compresslevel=1, mtime=123456)) + run(package / "verify.py", root, "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING") + payload["forward"][0]["odd_best"][1] -= 1 + path.write_bytes(gzip.compress(json.dumps(payload).encode(), mtime=0)) + run(package / "verify.py", root, "census mismatch", success=False) + path.write_bytes(original) + + lower = root / "research/complex-dyadic-lowering/lower.py" + original = lower.read_bytes() + lower.write_bytes(original + b"\n# source mutation must be rejected before import\n") + run(package / "verify.py", root, "source SHA256", success=False) + lower.write_bytes(original) + require(inventory(root) == before, "mutation fixtures were not restored") + finally: + writable(root) + print("PASS_GAUSSIAN_PACKAGE_CONTROLS read_only_export=2 corrupted_artifacts=3 equivalent_gzip=1") + + +if __name__ == "__main__": + main() diff --git a/research/k8-gaussian-unit-rounding-seed24/verify.py b/research/k8-gaussian-unit-rounding-seed24/verify.py new file mode 100644 index 0000000000..7e3d9b8c88 --- /dev/null +++ b/research/k8-gaussian-unit-rounding-seed24/verify.py @@ -0,0 +1,237 @@ +#!/usr/bin/env python3 +"""Exact replay. Hanson Sun with substantial OpenAI Codex assistance; Apache-2.0.""" +import argparse +import copy +from fractions import Fraction as Q +import gzip +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import model as m + + +def primitive_map(word, registers): + rows = {r: [Q(int(i == j)) for j in range(len(registers))] + for i, r in enumerate(registers)} + for op in word: + tag, target = op[:2] + if tag in ("add", "subtract"): + sign = 1 if tag == "add" else -1 + rows[target] = [a + sign * b for a, b in zip(rows[target], rows[op[2]])] + elif tag == "copy": + rows[target] = rows[op[2]].copy() + elif tag == "clear": + rows[target] = [Q(0)] * len(registers) + else: + m.require(tag in ("double", "halve", "negate"), "primitive matrix opcode") + factor = {"double": Q(2), "halve": Q(1, 2), "negate": Q(-1)}[tag] + rows[target] = [factor * a for a in rows[target]] + return rows + + +def check_macro(z, word=None): + registers = [(name, c) for name in ("T", "S", "W") for c in range(2)] + word = m.lower_gaussian(z) if word is None else word + rows = primitive_map(word, registers) + expected = { + ("T", 0): [1, 0, z[0], -z[1], 0, 0], + ("T", 1): [0, 1, z[1], z[0], 0, 0], + ("S", 0): [0, 0, 1, 0, 0, 0], + ("S", 1): [0, 0, 0, 1, 0, 0], + ("W", 0): [0] * 6, ("W", 1): [0] * 6, + } + m.require(rows == expected, "six-column dirty Gaussian macro") + m.require(len(word) == m.gaussian_add_cost(z), "macro cost") + + +def check_boundary(a, odd, forward=None, backward=None): + honest_f, honest_b = m.boundary_word(a, odd) + forward = honest_f if forward is None else forward + backward = honest_b if backward is None else backward + registers = [("X", 0), ("X", 1)] + z = m.gauge(a, odd) + expected = {registers[0]: [z[0], -z[1]], registers[1]: [z[1], z[0]]} + m.require(primitive_map(forward, registers) == expected, "boundary forward map") + m.require(primitive_map(forward + backward, registers) == + {registers[0]: [1, 0], registers[1]: [0, 1]}, "boundary restoration") + + +def total_gauge_cost(events, assignments): + """Complete scalar cost, with phase-zero optimal boundary circuits.""" + factors = {("L", h): m.gauge(a, odd) for h, (a, odd) in assignments.items()} + cost = sum(2 * abs(2 * a + 1) + 4 if odd else 4 * abs(a) + for a, odd in assignments.values()) + for ev in events: + if ev[0] != "scalar": + continue + g = ev[1] + if g[0] == "add": + z = m.mul((Q(g[3], g[4]), Q(0)), + m.mul(factors.get(tuple(g[1]), m.ONE), + m.inv(factors.get(tuple(g[2]), m.ONE)))) + cost += m.gaussian_add_cost(z) + elif g[0] == "scale": + q = Q(g[2], g[3]) + p, e = m.parts(q) + m.require(p == 1, "original dyadic SCALE") + cost += 2 * (abs(e) + int(q < 0)) + else: + m.require(g[0] in ("copy", "clear"), "full invoice opcode") + cost += 2 + return cost + + +def rounding_checks(events, helpers): + results = [] + for pattern in range(4): + assignments = {h: ((h * (pattern + 1) + 24) % 9 - 4, + int((h + pattern) % (pattern + 2) == 0)) for h in helpers} + odd_count = sum(b for a, b in assignments.values()) + gaussian = total_gauge_cost(events, assignments) + low = total_gauge_cost(events, {h: (a, 0) for h, (a, b) in assignments.items()}) + high = total_gauge_cost(events, {h: (a + b, 0) for h, (a, b) in assignments.items()}) + gap_twice = 2 * gaussian - low - high + m.require(gap_twice >= 8 * odd_count, "common rounding dominance") + results.append({"pattern": pattern, "odd_helpers": odd_count, + "gaussian_cost": gaussian, "low_cost": low, "high_cost": high, + "twice_gap_above_average": gap_twice}) + return results + + +def reject(label, fn, expected): + try: + fn() + except ValueError as exc: + m.require(expected in str(exc), "wrong rejection for " + label + ": " + str(exc)) + return label + raise ValueError("control unexpectedly accepted: " + label) + + +def controls(): + result = [] + def add(label, fn, reason): + result.append(reject(label, fn, reason)) + mixed = (Q(3, 2), Q(3, 2)) + word = m.lower_gaussian(mixed) + second = next(i for i, g in enumerate(word) if g[:2] == ("add", ("T", 1))) + add("missing_shared_target", lambda: check_macro(mixed, word[:second] + word[second + 1:]), "six-column") + wrong = list(word) + wrong[second] = ("subtract", *wrong[second][1:]) + add("wrong_cross_channel_sign", lambda: check_macro(mixed, wrong), "six-column") + add("missing_product_initialization", lambda: check_macro(mixed, word[1:]), "six-column") + unit_word = m.lower_gaussian((Q(1), Q(1))) + add("dirty_work_not_cleared", lambda: check_macro((Q(1), Q(1)), unit_word[:-1]), "six-column") + f, b = m.boundary_word(-3, 1) + add("missing_inverse_boundary", lambda: check_boundary(-3, 1, f, []), "boundary restoration") + broken = list(f) + broken[0] = ("double", *broken[0][1:]) + add("wrong_boundary_shift", lambda: check_boundary(-3, 1, broken, b), "boundary forward") + add("operand_alias", lambda: m.lower_gaussian(mixed, ("T",), ("T",)), "distinct complex") + add("outside_gaussian_support", lambda: m.lower_gaussian((Q(1), Q(2))), "Gaussian support") + add("nondyadic_coefficient", lambda: m.c(Q(1, 3)), "nonzero dyadic") + add("gaussian_nonunit", lambda: m.unit_coordinates((Q(2), Q(1))), "unit diagonal") + add("zero_factor", lambda: m.unit_coordinates(m.ZERO), "nonzero Gaussian unit") + add("false_one_step_lipschitz", lambda: m.require(m.c(2) <= m.c(1) + 1, "unit discount jump"), "unit discount") + # Ten repeated edges disprove independent rather than common rounding. + gaussian_toy = 10 * 2 * m.c(1) + 12 + independent_mean = 10 * (4 * m.c(1) + 2 * m.c(2) + 2 * m.c(Q(1, 2))) // 4 + 4 + add("false_independent_rounding", lambda: m.require(gaussian_toy >= independent_mean, "rounding must be common"), "common") + manifest = json.loads((m.HERE / "SOURCES.json").read_bytes()) + missing = copy.deepcopy(manifest) + missing["files"] = [r for r in missing["files"] if r["path"] != m.LOWER] + add("removed_source_pin", lambda: m.check_sources(missing), "source inventory") + altered = copy.deepcopy(manifest) + altered["base_commit"] = "0" * 40 + add("wrong_base", lambda: m.check_sources(altered), "base commit") + add("modified_lowerer", lambda: m.check_sources(reader=lambda p: + (m.ROOT / p).read_bytes() + (b"\n# changed\n" if p == m.LOWER else b"")), "source SHA256") + return result + + +def compute(): + word, programs, bindings, _, _ = m.load() + helpers = m.domain(word, programs) + m.require(len(helpers) == 237, "eligible helper count") + census = {} + result = {"status": "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING", + "base_commit": m.BASE, "assignment_seed": 24, + "eligible_helpers": helpers, "seed_selected_probe_helper": helpers[24], + "source_members": bindings, "orientations": {}} + coefficients = set() + for orientation in ("forward", "backward"): + events = programs[orientation] + rows = m.census(events, helpers) + census[orientation] = rows + entry = {"census_rows": len(rows), + "integer_breakpoint_evaluations": sum(len(r["real_candidates"]) + len(r["odd_candidates"]) for r in rows), + "rounding_fixtures": rounding_checks(events, helpers)} + variants = [("baseline", {})] + for name in ("real", "odd"): + key = name + "_best" + winner = min(rows, key=lambda r: (r[key][1], r["helper"], abs(r[key][0]), r[key][0])) + a, delta = winner[key] + entry[name + "_winner"] = {"helper": winner["helper"], "a": a, "delta": delta, + "incident_adds": winner["incident_adds"]} + variants.append((name, {winner["helper"]: (a, int(name == "odd"))})) + prices = {} + for name, assignments in variants: + stream = m.transformed(events, assignments) + m.require([e for e in stream if e[0] != "scalar"] == + [e for e in events if e[0] != "scalar"], "non-scalar stream unchanged") + endpoint = m.replay(stream, assignments, orientation) + price = m.invoice(stream, assignments) + m.require(price["complex_scalar_primitives"] == total_gauge_cost(events, assignments), + "formula versus emitted complete invoice") + for ev in stream: + if ev[0] == "scalar" and ev[1][0] == "add": + coefficients.add((Q(*ev[1][3]), Q(*ev[1][4]))) + prices[name] = {"endpoint": endpoint, "invoice": price, + "gaussian_macro_stream_sha256": m.sha(m.canonical(stream)), + "assignments": {str(h): [a, b] for h, (a, b) in assignments.items()}} + before = prices["baseline"]["invoice"] + m.require(before["complex_scalar_primitives"] == (149002 if orientation == "forward" else 149018), "retained baseline invoice") + for name in ("real", "odd"): + after = prices[name]["invoice"] + m.require(after["paid_profile"] == before["paid_profile"], "paid profile unchanged") + m.require(after["complex_scalar_primitives"] - before["complex_scalar_primitives"] == + entry[name + "_winner"]["delta"], "census versus materialized winner") + entry["programs"] = prices + result["orientations"][orientation] = entry + for e in (-16, -3, -1, 0, 1, 2, 16): + for p in (1, 3, 5, 7): + for phase in range(4): + coefficients.add(m.mul((p * m.power(e), p * m.power(e)), m.gauge(0, 0, phase))) + for z in sorted(coefficients): + check_macro(z) + for a in range(-16, 17): + for odd in (0, 1): + check_boundary(a, odd) + result["local_primitive_checks"] = {"distinct_gaussian_macros": len(coefficients), + "formal_columns_per_macro": 6, + "boundary_pairs": 66} + result["rejection_controls"] = controls() + result["census_payload_sha256"] = m.sha(m.canonical(census)) + result["scope"] = "Written common-rounding theorem for the specified macro-local lowering and separate two-register boundaries; finite exact k8 evidence. No native hosting, new paid profile, kappa or full multiplication theorem." + return result, census + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="regenerate this package's own certificates") + parser.add_argument("--json", action="store_true") + args = parser.parse_args() + result, census = compute() + if args.write: + (m.HERE / "CERTIFICATE.json").write_text(json.dumps(result, indent=2) + "\n") + (m.HERE / "CENSUS.json.gz").write_bytes(gzip.compress(m.canonical(census), mtime=0)) + else: + m.require(m.canonical(result) == m.canonical(json.loads((m.HERE / "CERTIFICATE.json").read_bytes())), "certificate mismatch") + m.require(m.canonical(census) == m.canonical(json.loads(gzip.decompress((m.HERE / "CENSUS.json.gz").read_bytes()))), "census mismatch") + print(json.dumps(result, indent=2) if args.json else + "PASS_GAUSSIAN_UNIT_COMMON_ROUNDING helpers=237 orientations=2 real_saving=332 odd_saving=58 controls=" + str(len(result["rejection_controls"]))) + + +if __name__ == "__main__": + main()