diff --git a/research/complex-x4-target-forest/CLAIM.md b/research/complex-x4-target-forest/CLAIM.md new file mode 100644 index 0000000000..b8cb15b889 --- /dev/null +++ b/research/complex-x4-target-forest/CLAIM.md @@ -0,0 +1,37 @@ +# Sprint claim + +- Track: complex supplier; OS-random assignment seed **34**. +- Base: `91a2094f2e022930069e8cfdc810a3ea1b81cd09`. +- Claim recorded: 2026-10-14 Australia/Melbourne. +- Expected finish: 2026-10-14 00:45 Australia/Melbourne (2026-10-13 13:45 UTC). +- Object: the selected PR799 X4 zero-frame arbitrary-helper compensation matrix. +- Method: restored signed target forests, extending the disjoint pair class of + PR901. Exact binary-Horner prices include both basis boundaries. Test whether + a minimum-spanning-tree formulation yields a cheaper complete circuit. + Seed 34 determines deterministic tie ordering, not mathematical coverage. +- Deliverable: one source-pinned finite construction or scoped negative result, + exact reproduction, arbitrary-input replay and corruption controls. +- Three candidates considered: X4 overlapping target forests (chosen); nonunit + target pairs (closed by PR909); JP8 coefficient-work sharing (substantial + existing coverage in PR722/739/751/755/811/830/839/882). +- Overlap: PR901 disjoint X4 pairs; PR909 excludes nonunit disjoint pairs; + PR816 and PR917 use target forests in historical CK compensation. This + contribution will credit the mechanism and check a complete selected-X4 + circuit, including the minimum-cost forest claim if justified. +- Coordination: live pinnedIssues query returned no pinned issues; sprint issue + search returned none. Local claim used. Open PR metadata inspected through + PR925 immediately before this claim. No other issue opened. +- Timing: orientation bounded to first 8 minutes of a 40-minute session; + final 10 minutes reserved for verification and handoff. + +## Completion + +Submitted one contribution: [PR932](https://github.com/CrocSwap/integer-mult-bounds/pull/932). +The selected-X4 forest has 6 roots and 106 edges, reduces compensation from +6,320 to 2,324 additions, and saves 47,690 real primitives per orientation. +Its exact scoped floor is 10,883 primitives per real component. Full scalar +replay, independent Prim/cycle/operator checks, nine package tests and selected +record checks pass; VALIDATION.md records remaining integration obligations. +No new kappa is claimed. Final overlap refresh reached #931, with #901/#816 +heads unchanged and no competing selected-X4 forest found. No pinned issue +was available, so this is the single local claim update with the result link. diff --git a/research/complex-x4-target-forest/EXPECTED.json b/research/complex-x4-target-forest/EXPECTED.json new file mode 100644 index 0000000000..d0cf322358 --- /dev/null +++ b/research/complex-x4-target-forest/EXPECTED.json @@ -0,0 +1,168 @@ +{ + "base": "91a2094f2e022930069e8cfdc810a3ea1b81cd09", + "census_edges": 12544, + "census_sha256": "0418c47ee4d11eabc6f5d070a78ed31ee03216f3b4b99569e31f6a5ebe07369d", + "compensation_new_additions": 2324, + "compensation_original_additions": 6320, + "complex_compensation_floor": 10883, + "controls": [ + "missing_middle", + "missing_preparation", + "missing_restoration", + "wrong_coefficient_sign", + "wrong_order" + ], + "independent": { + "all_forest_registers_enter_in_zero_frame": true, + "arbitrary_input_columns": 328, + "component_primitive_baseline": 34728, + "component_primitive_optimum": 10883, + "cycle_inequalities_checked": 12544, + "forest_edges": 106, + "helpers": 216, + "method": "Fraction symbolic maps; explicit Horner lists; Prim; all-edge cycle property", + "negative_controls": [ + "forward:omit_prepare", + "forward:omit_restore", + "forward:wrong_injection_sign", + "backward:omit_prepare", + "backward:omit_restore", + "backward:wrong_injection_sign", + "incorrect_edge_price" + ], + "orientations": [ + "forward", + "backward" + ], + "real_primitive_baseline": 69456, + "real_primitive_optimum": 21766, + "real_primitive_savings_each_orientation": 47690, + "roots": 6, + "scalar_macros": 2324, + "scope": "Exact finite compensation operator and forest-class optimum only; no full theorem or kappa claim.", + "signed_graph_edges": 12544, + "status": "PASS_INDEPENDENT_X4_TARGET_FOREST", + "targets": 112, + "unique_microcircuit_coefficients": 8 + }, + "middle_additions": 2112, + "preparation_additions": 106, + "programs": { + "backward": { + "baseline": { + "arbitrary_input_columns": 737, + "exact_fractional_bits": 19, + "macros": 19197, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + }, + "positive_prefix_upper": "48299247699832632898063/16", + "prefix_bits": 72, + "primitive_counts": { + "add": 57212, + "clear": 73424, + "double": 13892, + "halve": 28456, + "negate": 1296, + "subtract": 18930 + }, + "primitive_sha256": "d8176fdab95309e59da5087e7e039ecd1ec9868f7d46eaa49a31e837342f7fd7", + "program_sha256": "7915679ee305927463d19725360cc15132dd21ede18897d09a935dca1df0d55d", + "real_primitives": 193210 + }, + "candidate": { + "arbitrary_input_columns": 737, + "exact_fractional_bits": 19, + "macros": 15201, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + }, + "positive_prefix_upper": "219829455967238186882729/16", + "prefix_bits": 74, + "primitive_counts": { + "add": 45404, + "clear": 57440, + "double": 13872, + "halve": 12780, + "negate": 1296, + "subtract": 14728 + }, + "primitive_sha256": "787082f54b7eb43f76b3dd859a128a31eb87491d9cb5449da9393e000f412f36", + "program_sha256": "574a8420cd769e5b0445e6f19b51a578a6e571a5e2057d24e330bb186a8caba5", + "real_primitives": 145520 + }, + "saved_real_primitives": 47690 + }, + "forward": { + "baseline": { + "arbitrary_input_columns": 737, + "exact_fractional_bits": 3, + "macros": 19197, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + }, + "positive_prefix_upper": "6812058044968180837/256", + "prefix_bits": 55, + "primitive_counts": { + "add": 58568, + "clear": 73392, + "copy": 16, + "double": 13892, + "halve": 28456, + "negate": 1296, + "subtract": 17542 + }, + "primitive_sha256": "1a675754e424290dc81ef8672f6c7e66e8da5f0d4025314df0cea52306fe903a", + "program_sha256": "076a2d428f97abb30473df05110998efbe5ac809885bae4ceb1b8bd81329a1e6", + "real_primitives": 193162 + }, + "candidate": { + "arbitrary_input_columns": 737, + "exact_fractional_bits": 3, + "macros": 15201, + "paid_profile": { + "1": 2548, + "2": 338, + "3": 430, + "4": 194, + "5": 56, + "8": 8 + }, + "positive_prefix_upper": "6812058044968180837/256", + "prefix_bits": 55, + "primitive_counts": { + "add": 46348, + "clear": 57408, + "copy": 16, + "double": 13872, + "halve": 12780, + "negate": 1296, + "subtract": 13752 + }, + "primitive_sha256": "f4a17c8ae41ee40a1a235a765bbaff74f2cf9f35643d5c920a4ea26a2f4452a3", + "program_sha256": "bf0f10d672c3314eabf264e302d40d92926895e26f8bff91dfca17b8a3b908a2", + "real_primitives": 145472 + }, + "saved_real_primitives": 47690 + } + }, + "restoration_additions": 106, + "roots": 6, + "seed": 34, + "status": "PASS_X4_TARGET_FOREST" +} diff --git a/research/complex-x4-target-forest/PROOF.md b/research/complex-x4-target-forest/PROOF.md new file mode 100644 index 0000000000..712aaa6b99 --- /dev/null +++ b/research/complex-x4-target-forest/PROOF.md @@ -0,0 +1,238 @@ +# Signed target forests for the selected X4 compensation panel + +This is a finite circuit construction and an exact cost optimum within a stated +forest class. It does not assert a new exponent or optimality among arbitrary +circuits. The source is the selected PR799 X4 word, at audited source head +`80e6463157cfc80b85af09e7e2f14748fe2dac60`, read from the accepted replay archive +on base `91a2094f2e022930069e8cfdc810a3ea1b81cd09`. The package's executable +source pins and receipt identify the precise archive members and counts. + +## 1. The boundary being replaced + +Let `y` denote the 112 compensation targets and `h` the arbitrary public helper +inputs. Write `C_i` for row `i` of the exact dyadic compensation matrix. The +forward panel has the complete logical boundary + +```text +(y, h) -> (y + C h, h). +``` + +Neither vector is assumed zero. The coefficient-work register can initially +contain arbitrary private dirt; its paid lowering clears it. All instructions +introduced by this construction occur at the panel's inherited zero frame. +The source checker must establish that frame and panel identification; the +linear argument alone would not establish geometric legality. + +Choose a rooted forest on the 112 target labels. Every nonroot `i` has one +parent `p(i)` and one sign `epsilon_i` in `{+1,-1}`. Prepare targets with + +```text +y_i <- y_i + epsilon_i y_p(i) +``` + +The executable recipe stores `sign_i=-epsilon_i`, so its equivalent notation +is `y_i <- y_i-sign_i*y_p(i)` and `C_i-sign_i*C_p(i)`. + +in leaf-before-parent order. A parent's original input has not yet been +modified when one of its children uses it. Consequently the product `T` of +these shears has rows `e_i + epsilon_i e_p(i)` at nonroots and `e_i` at roots; +no ancestor terms have silently appeared. This is a unit triangular matrix +after a forest ordering, hence invertible over the dyadic rationals. + +Run ordinary compensation on the transformed targets with rows + +```text +root i: C_i +nonroot i: C_i + epsilon_i C_p(i). +``` + +Finally undo each preparation shear, with its opposite sign, in reverse +chronological order. This yields, for arbitrary target and helper inputs, + +```text +T^-1 (T y + T C h) = y + C h. +``` + +All forward helper inputs are unchanged. Restoring in the wrong order is not +generally valid on a path of length two: a child must use the already-restored +parent when its own shear is undone. The exact recipe contains both orders. +Neither the proof nor the replay permits replacing `Ty` by zero. + +## 2. Complete scalar cost in the specified lowering + +The class uses the unchanged cleared-work binary-Horner lowering, independently +for every nonzero coefficient. Put `c(0)=0`. For a nonzero reduced dyadic +coefficient `q=a/2^k`, where `a` is a nonzero integer and `k>=0`, the cost per +real component is + +```text +c(q) = 3 + floor(log2(abs(a))) + popcount(abs(a)) + k. +``` + +The bill is one initial work clear, `floor(log2(abs(a)))` doublings, +`popcount(abs(a))` source additions, `k` halvings, one signed target +accumulation, and one final work clear. This includes leading-bit source +access and permits arbitrary initial work. It also proves `c(-q)=c(q)` and +`c(1)=c(-1)=4`. Thus a preparation shear and its restoration cost **eight** +primitives per real component, including their coefficient work. They are +not treated as two cost-free changes of notation or as two unit additions. +Both real components of a complex stream are charged separately. + +For a row `v`, let `R(v)=sum_j c(v_j)`. A root contributes `R(C_i)`. An edge +from nonroot `i` to parent `j` with sign `epsilon` contributes + +```text +w(i,j,epsilon) = R(C_i + epsilon C_j) + 8. +``` + +This is a complete forward-panel bill within this class. It includes every +residual coefficient macro, source access, preparation and restoration. No +extra helper, frame change, copy, recursive child or center is introduced. +Every non-scalar event and every scalar macro outside the panel remains the +corresponding pinned source event. Those unchanged costs are retained in the +full-program comparison; they are not a source of the reported saving. + +The model deliberately does not combine neighboring work clears, replace unit +Horner circuits by a cheaper lowering, share coefficient work across entries, +or fold the basis changes into an adjacent phase. Those are different classes. + +## 3. Exact forest optimum by a superroot spanning tree + +Construct a multigraph with target vertices `0,...,111` and one superroot `r`. +These are abstract labels; the source registers are `112,...,223`, and the +recipe represents the superroot by `-1`. +Include edge `(r,i)` of weight `R(C_i)` for every target. Between every two +distinct targets include two parallel edges with the weights +`w(i,j,+1)` and `w(i,j,-1)`. There are +`112 + 2*binom(112,2) = 12,544` edges and 113 vertices. + +The target-edge weights are independent of orientation. For the plus sign +this follows by commutativity; for the minus sign it follows from +`C_j-C_i=-(C_i-C_j)` and the sign-invariance of `c`. More uniformly, +`C_j+epsilon C_i = epsilon(C_i+epsilon C_j)`. + +Any target forest becomes a spanning tree by joining each of its roots to +`r`. Its complete cost is exactly the resulting tree's weight. Conversely, +orient any spanning tree away from `r`, remove `r` and its incident edges, +and retain the sign on each target edge. Each remaining component has one +root, each other target has one parent, and Section 1 realizes precisely the +tree's cost. These operations preserve cost in both directions. A tree cannot +use both parallel edges between the same vertices, because they would form +a cycle in the multigraph. + +It follows that a minimum spanning tree attains the minimum complete cost +over this **single-parent signed-unit target-forest class**. This is not a +heuristic claim about the deterministic tie ordering. Seed 34 only chooses +among tied options; it does not restrict the edge census. + +The finite certificate is checkable without trusting the construction's +Kruskal algorithm: check that the selected edges form a spanning tree, sum +their exact integer prices, then check for every graph edge that its weight +is at least the largest selected-edge weight on the unique tree path between +its endpoints. If a cheaper graph edge violated this condition, exchanging +it with that largest path edge would improve the tree. Conversely, when all +these cycle inequalities hold, repeated exchanges transform any spanning +tree into the selected tree without increasing weight, proving minimality. +An independently coded Prim computation supplies an additional exact check. + +This floor excludes nonunit parent coefficients, multiple parents, helper +basis changes, shared subexpressions, and changes outside the panel. It is +not an impossibility theorem for cheaper compensation circuits. + +The attained recipe has six roots and 106 signed target edges. It replaces +6,320 compensation additions by 2,324: 106 preparation, 2,112 residual, and +106 restoration additions. Its exact minimum is **10,883** primitives per +real component, compared with the original panel's **34,728**. Equivalently, +these count complex-stream primitives before charging two real components. +The complete emitted scalar-program counts are: + +| Orientation | Original real primitives | Forest real primitives | Saving | +| --- | ---: | ---: | ---: | +| Forward | 193,162 | 145,472 | 47,690 | +| Inverse transpose | 193,210 | 145,520 | 47,690 | + +These counts do not combine this construction with a different scalar +lowering or with other pending supplier changes. + +## 4. Inverse-transpose orientation + +A logical addition `G=I+q e_t e_s^T`, with distinct source and target, has +`G^-T=I-q e_s e_t^T`. Thus inverse-transposition swaps source and target and +negates the coefficient. If macros are executed chronologically as +`G_1,...,G_m`, their total map is `G_m...G_1`, whose inverse transpose is +`G_m^-T...G_1^-T`. Execute the inverse-transposed macros in the **same +chronological order** and then lower each one afresh. Their coefficient +magnitudes, and hence their scalar bills, are unchanged. + +This argument concerns invertible logical macros. The private-work CLEAR +primitives are not invertible and are not inverse-transposed. Their charged +implementation is separately checked on arbitrary private work inputs. + +The inverse-transpose panel maps `(y,h)` to `(y,h-C^T y)`. It intentionally +writes helpers in this orientation; the forward panel's unchanged-helper +statement must not be applied to it. The complete supplier's required +endpoint, including public helper restoration and private clearing, must +therefore be replayed in each orientation against its pinned baseline. + +## 5. Numerical scope, checks and inherited obligations + +Endpoint equality does not imply safe intermediate magnitudes. Prefix bounds +must be recomputed from the actual candidate instruction stream in both +orientations, including basis changes and all binary-Horner work. For a +positive upper envelope, a signed addition is safely bounded by adding the +absolute coefficient times the source bound; dyadic scaling and work clears +are applied at their actual positions. Acceptance requires the fresh bound +to meet the inherited 192-bit local payload allowance. A smaller gate count +alone is insufficient, and no containment in the original prefix trace is +asserted. This exact finite bound does not settle all-size rounding or tape +precision. + +Literal primitive replay on all 728 logical and nine arbitrary private input +columns gives the following positive prefix envelopes: + +| Orientation | Original | Forest | Original / forest bits | +| --- | ---: | ---: | ---: | +| Forward | `6812058044968180837/256` | `6812058044968180837/256` | 55 / 55 | +| Inverse transpose | `48299247699832632898063/16` | `219829455967238186882729/16` | 72 / 74 | + +The increased inverse-transpose envelope is explicitly charged; it is not +inherited unchanged. Both remain below `2^192`. The largest exact fractional +grid depths of actual replayed rows are respectively 3 and 19 bits, unchanged +between original and candidate. These are finite-stream measurements, not a +general precision theorem. + +Useful adverse controls include: omitting preparation (which may pass a +helper-only replay but fails arbitrary target columns), omitting restoration, +changing one sign or transformed coefficient, reordering a length-two path's +preparation, omitting work clear, and underbilling the two unit boundaries. +The certificate must also reject non-tree edges, altered edge prices, and a +nonminimal tree even if its resulting linear map is correct. A failed search, +a rejected corrupted certificate and a general proof are different evidence. + +The finite word replay and the forest-class proof do not reprove geometric +and physical admission, global hosting/invoices, outer assembly, or a full +multiplication theorem. Production use requires typed construction integration +and refreshed bindings. All inherited compiler/common-label/mutable-source, +whole-call hosting, precision/tape, analytic-transfer and bit-supplier +assumptions remain. The selected conditional exponent is unchanged. + +## 6. Predecessors and attribution + +This does not claim invention of restored target forests or their spanning +tree reduction. Credit Sricharan Vagvala's PR749 for rational restored target +pairs, Oscar Fennell's PR759 for binary target forests and the superroot +reduction, and **PR816 by @dd-hemant**, pinned at +`133735a2cc2319c12ba5d786214b2217e083e7da`, for the same signed rational +coefficient-dependent forest mechanism on historical CK. **PR901 by ToikY**, +pinned at `dbe8dc01f8306bd7dab8d861a953b23e5cda6a70`, applies disjoint restored +target pairs to this selected X4 compensation panel. This contribution checks +the larger forest class on that selected panel rather than asserting priority +for the mechanism. No savings from those separate packages are assumed +additive or imported without source verification. + +The X4 supplier retains Jeremy Kothe's PR799, Chafik Boukhalfa's PR741, +icekylinx's gauge44, and the compiler/cold/owner and other contributors named +in the selected maintainer review and original notices. This proof was +prepared for Ross with substantial OpenAI Codex assistance, including a +separate proof-review worker. Apache-2.0 applies to the new contribution; +predecessor notices are retained. No independent human review is claimed. diff --git a/research/complex-x4-target-forest/README.md b/research/complex-x4-target-forest/README.md new file mode 100644 index 0000000000..2794a3190a --- /dev/null +++ b/research/complex-x4-target-forest/README.md @@ -0,0 +1,157 @@ +# Selected X4 target forests: finite circuit construction, no new kappa + +A restored signed target forest reduces the selected PR799 X4 compensation +panel from **6,320 to 2,324 additions**, including **106 preparation and 106 +restoration gates**. Both complete scalar projections save **47,690 real +primitives** under the unchanged cleared-work binary-Horner lowering. + +| Complete scalar projection | Original | Forest | Saving | +|---|---:|---:|---:| +| Forward real primitives | 193,162 | 145,472 | 47,690 | +| Inverse-transpose real primitives | 193,210 | 145,520 | 47,690 | +| Scalar macros, either orientation | 19,197 | 15,201 | 3,996 | + +This gives **13,890 additional real primitives saved** compared with ToikY's +PR901 disjoint-pair result on the same selected panel (159,362 / 159,410). +Those predecessor numbers are contextual reported results, not imported +receipts or summed savings. The construction here is repriced from its own +complete emitted words. No pending implementation is imported. + +The exact attained floor is **10,883 primitives per real component** for the +compensation panel, versus 34,728 originally. Equivalently the complex-stream +circuit has 10,883 scalar instructions and costs **21,766 real primitives**. +A complete 12,544-edge graph census, independently coded Prim solver and every +cycle inequality prove optimality **only within the specified signed-unit, +single-parent target-forest class with independent Horner lowering**. + +The selected conditional kappa remains **0.001661634653669567**. This package +does not change the selected record, any supplier generator or `upstream/`. + +## Reproduce + +From the repository root with Python 3.9+ (standard library, offline): + +```sh +python3 -I -O -B research/complex-x4-target-forest/verify.py +``` + +Expected final line: + +```text +PASS_X4_TARGET_FOREST compensation=6320->2324 saved_real=47690/47690 forest_floor=10883 columns=737 orientations=2 no_new_kappa +``` + +The command checks immutable source inputs, rebuilds the exact recipe, lowers +and replays baseline and replacement scalar programs, runs adverse controls, +invokes the independent checker and compares every receipt field with +[EXPECTED.json](EXPECTED.json). It writes no files. `--write NEW_PATH` is an +explicit development-only receipt command and refuses existing output paths. + +Additional checks: + +```sh +python3 -I -O -B research/complex-x4-target-forest/test_package.py +python3 -I -O -B research/complex-x4-target-forest/independent.py +``` + +The second checker reads its own pinned inputs, implements its own graph and +symbolic operator, constructs coefficient microcircuits, runs Prim and checks +all 12,544 cycle inequalities. It does not import the generator. Both checkers +use exact Fraction arithmetic; algorithmic and implementation independence +is claimed, not an independently developed rational-arithmetic library or +independent human review. + +## Construction and coverage + +[PROOF.md](PROOF.md) gives the general substitution and cost proof. +[RECIPE.json](RECIPE.json) specifies every signed edge, root and exact weight. +[experiment.py](experiment.py) constructs an explicit candidate event stream +by replacing only the pinned 6,320-operation zero-frame compensation segment. +The recipe contains six rooted trees. Leaves are prepared before parents, +residual rows are injected, then parents are restored before children. Every +source access, coefficient work clear/double/halve/add, basis operation and +restoration is counted. No helper stream, frame adapter, recursive child or +copy is added. All non-scalar events remain byte-for-byte equal as JSON values. +The forward panel preserves helpers; the inverse-transpose panel writes them +as required by its dual map. Complete scalar endpoints restore public helpers +and erase private work in both orientations. + +Full literal primitive replay checks **728 logical plus nine arbitrary private +input columns**, including all 504 public helpers, eight private centres and +coefficient work. It checks the required final forward/dual shears, public +helper restoration, and private erasure. The independent compensation check +covers **328 arbitrary target/helper columns**, including all 216 active +helpers; the other logical registers are untouched by the panel. Eight +coefficient microcircuits are separately checked on arbitrary source, target +and private-work values. Two real components follow the same real-coefficient +circuit. These are scalar projections: neither checker executes physical +Clifford/frame/phase events or redoes global hosting. + +The five primary operator controls and seven independent controls include +missing preparation/restoration, sign errors and underbilled edges. Nine +package tests additionally reject a valid-but-nonminimal all-root forest, +a cycle, boundary corruption, uncleared private coefficient work or target corruption from an omitted clear, and +source corruption, and test minimal relocation without Git metadata. The +missing-preparation control deliberately **passes a helper-only replay** but +fails arbitrary-target checking; checking only the helpers would miss it. + +The deterministic search domain is all 112 root edges and both signs on each +of 6,216 unordered target pairs: **12,544 exact edge prices**. Kruskal ends +after its complete edge census and spanning-tree construction; no time or +probabilistic cutoff is used. Seed **34**, drawn using OS randomness, breaks +ties only. Completed coverage is the full stated graph. The written MST +reduction and checked cycle certificate justify the scoped optimum; no +arbitrary-circuit optimum or impossibility theorem is asserted. + +## Precision and remaining obligations + +The positive prefix envelope is recomputed on every literal primitive. The +baseline envelopes match the pinned selected replay exactly. Forward remains +`6812058044968180837/256` (55 bits). Backward rises from +`48299247699832632898063/16` (72 bits) to +`219829455967238186882729/16` (74 bits). Both remain below the pinned +**192-bit local allowance**. Exact maximum fractional depths of actual +intermediate rows remain **3 forward / 19 backward**, including private-input +columns. Smaller gate counts do not imply containment of all old prefixes. +These bounds are finite scalar checks, not an all-size rounding/tape proof. + +Production integration still needs a typed alternative-compensation admission, +fresh source bindings, owner/hosting/invoice replay and outer assembly. The +paid recursive profiles are unchanged. All inherited all-size/compiler, +common-label/mutable-source, whole-call hosting, precision/tape, +analytic-transfer and bit-supplier hypotheses remain. No new global bound, +practical runtime speedup or full multiplication-theorem proof is claimed. +This does not combine PR883's precondition lowering or PR917's helper changes. + +## Provenance and attribution + +Exact base: **`91a2094f2e022930069e8cfdc810a3ea1b81cd09`**. +Accepted source: PR799 at `80e6463157cfc80b85af09e7e2f14748fe2dac60`. +[SOURCES.json](SOURCES.json) pins the committed maintainer replay archive, +its consumed decompressed members and the selected X4 canonical/program pins. +No network, generated ancestor cache, or pending source is required. Immutable +input archives are hashed exactly; member equality uses decompressed bytes. + +This transports an existing mechanism to the selected X4 circuit and checks +its additional saving and exact family floor. Credit **@dd-hemant PR816** at +`133735a2cc2319c12ba5d786214b2217e083e7da` for the signed rational forest/MST +method on historical CK; **Oscar Fennell PR759** for binary forests and the +superroot reduction; **Sricharan Vagvala PR749** for rational restored pairs; +and **ToikY PR901** at `dbe8dc01f8306bd7dab8d861a953b23e5cda6a70` for selected +X4 disjoint pairs. PR909 at `5896f6fce48ee1d507722cc91eb1dcccc878670d` excludes +nonunit disjoint pairs but explicitly leaves overlapping bases outside scope. +PR917's historical CK two-sided circuit is distinct and its savings are not +assumed additive. Prior closed frame-only or disjoint-pair searches are not +reopened by extra computation; the forest class permits overlapping targets. + +Credit **Jeremy Kothe PR799**, **Chafik Boukhalfa PR741**, **icekylinx** and the +retained gauge, compiler, cold-helper, owner, precision and supplier lineage. +The source archive and notices are retained unchanged. See the selected +[maintainer review](../../docs/research/community-frontier799-review.md). + +Prepared by **Ross Richardson with substantial OpenAI Codex assistance** in +research, code, exact checking and writing, including separate AI workers for +the Prim/operator checker and mathematical review. New files are Apache-2.0, +as specified in the repository [LICENSE](../../LICENSE). No independent human +review is claimed. [CLAIM.md](CLAIM.md) records assignment and coordination; +[VALIDATION.md](VALIDATION.md) records checks and unrun gates. diff --git a/research/complex-x4-target-forest/RECIPE.json b/research/complex-x4-target-forest/RECIPE.json new file mode 100644 index 0000000000..685c8d4aa9 --- /dev/null +++ b/research/complex-x4-target-forest/RECIPE.json @@ -0,0 +1,120 @@ +{ + "seed": 34, + "complex_primitive_floor": 10883, + "census_edges": 12544, + "census_sha256": "0418c47ee4d11eabc6f5d070a78ed31ee03216f3b4b99569e31f6a5ebe07369d", + "edges": [ + [157, 219, 1, 8], + [128, 155, 1, 8], + [150, 168, 1, 8], + [129, 215, 1, 8], + [137, 191, 1, 8], + [143, 189, 1, 8], + [119, 199, 1, 8], + [182, 183, 1, 8], + [131, 214, 1, 8], + [122, 202, 1, 8], + [153, 154, 1, 8], + [222, 223, 1, 8], + [139, 193, 1, 8], + [147, 197, 1, 8], + [114, 184, 1, 8], + [118, 194, 1, 8], + [121, 201, 1, 8], + [172, 196, 1, 8], + [163, 216, 1, 8], + [170, 205, 1, 8], + [140, 187, 1, 8], + [123, 203, 1, 8], + [124, 212, 1, 8], + [142, 171, 1, 8], + [179, 192, 1, 8], + [164, 217, 1, 8], + [156, 211, 1, 8], + [176, 208, 1, 8], + [160, 210, 1, 8], + [112, 188, 1, 8], + [169, 204, 1, 8], + [130, 152, 1, 8], + [151, 167, 1, 8], + [134, 220, 1, 8], + [120, 207, 1, 8], + [174, 175, 1, 8], + [133, 148, 1, 8], + [146, 161, 1, 8], + [166, 213, 1, 8], + [185, 195, 1, 8], + [135, 145, 1, 8], + [173, 206, 1, 8], + [117, 180, 1, 8], + [132, 149, 1, 8], + [126, 127, 1, 8], + [158, 159, 1, 8], + [165, 218, 1, 8], + [125, 190, 1, 8], + [162, 221, 1, 12], + [138, 200, 1, 12], + [181, 209, 1, 12], + [136, 144, 1, 12], + [113, 198, 1, 12], + [116, 177, 1, 12], + [141, 186, 1, 12], + [115, 178, 1, 12], + [133, 222, -1, 94], + [135, 220, 1, 128], + [189, 215, 1, 132], + [174, 203, -1, 140], + [177, 208, 1, 140], + [190, 216, -1, 142], + [114, 121, 1, 144], + [147, 219, 1, 144], + [119, 169, 1, 148], + [112, 193, 1, 148], + [130, 151, 1, 150], + [120, 138, 1, 150], + [155, 216, 1, 156], + [174, 202, -1, 156], + [118, 140, -1, 156], + [189, 212, -1, 157], + [126, 165, -1, 158], + [177, 180, -1, 158], + [138, 179, -1, 158], + [173, 201, -1, 160], + [139, 169, 1, 160], + [167, 213, 1, 162], + [182, 203, -1, 165], + [141, 171, 1, 168], + [117, 209, -1, 168], + [136, 157, -1, 170], + [141, 185, -1, 171], + [124, 150, -1, 172], + [148, 159, -1, 172], + [132, 223, 1, 176], + [178, 192, -1, 178], + [156, 216, -1, 180], + [136, 210, -1, 180], + [170, 198, 1, 184], + [118, 198, -1, 187], + [127, 217, -1, 188], + [151, 214, -1, 190], + [172, 185, -1, 191], + [154, 165, -1, 192], + [135, 221, -1, 192], + [146, 220, 1, 194], + [121, 191, -1, 200], + [133, 204, 1, 208], + [129, 176, -1, 212], + [174, 216, -1, 228], + [-1, 174, 0, 236], + [138, 167, -1, 239], + [112, 114, 1, 240], + [141, 219, -1, 246], + [-1, 143, 0, 257], + [-1, 169, 0, 259], + [126, 201, 1, 260], + [134, 198, -1, 262], + [-1, 219, 0, 298], + [-1, 135, 0, 298], + [-1, 151, 0, 301] + ] +} diff --git a/research/complex-x4-target-forest/SOURCES.json b/research/complex-x4-target-forest/SOURCES.json new file mode 100644 index 0000000000..c2ef41f056 --- /dev/null +++ b/research/complex-x4-target-forest/SOURCES.json @@ -0,0 +1,13 @@ +{ + "base": "91a2094f2e022930069e8cfdc810a3ea1b81cd09", + "files": { + "research/community-frontier799-audit/integrated799-replay.tar.gz": "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb", + "research/gauge44-frames-x/construction/jx/LOCAL-PINS-jx-X4.json": "95c5114c8e937c2737a1b9f9da97303f2e5e129d39e6dfcc4010e99bfdb9c974" + }, + "members": { + "native/local/CANONICAL-WORD.json.gz": "1c0e9da767d4418f70016af599e4a447a3f7777acabe930318459c0fbbd260aa", + "native/local/LOCAL-PROGRAMS.json.gz": "223c2bb27ad68a4e9468c3ddaece1899d577b661190922fdd25f5976052c4cab", + "native/local/LOCAL-CHECKS.json": "bbde5cea7bfd5df3d3ee7dfada0ff9d165af43a4d1dec6a9597cbfd8f87cc3b2", + "native/local/INDEPENDENT-LOCAL-REPLAY.json": "355e2ae57b8eadc957bed567ba7c5caf33202ace690560c94b008f10cf906364" + } +} diff --git a/research/complex-x4-target-forest/VALIDATION.md b/research/complex-x4-target-forest/VALIDATION.md new file mode 100644 index 0000000000..d378b6e35a --- /dev/null +++ b/research/complex-x4-target-forest/VALIDATION.md @@ -0,0 +1,45 @@ +# Validation and handoff + +Base and refreshed upstream main: `91a2094f2e022930069e8cfdc810a3ea1b81cd09`. +Local validation date: 2026-10-14 Australia/Melbourne. + +## Completed + +- Exact recipe synthesis over all 12,544 signed/root graph edges. +- Full literal scalar-primitive replay for baseline and candidate, forward and + inverse-transpose, on 737 arbitrary input columns; both required shears, + 504 public helpers restored and nine private registers erased. +- Complete independent compensation maps on 328 active target/helper columns; + separately implemented Prim, all 12,544 cycle inequalities and eight explicit + coefficient microcircuits agree. Five primary and seven independent controls + reject their intended defects. +- `python3 -I -O -B research/complex-x4-target-forest/verify.py`: PASS on + CPython 3.14.6 and isolated optimized CPython 3.9.6. Frozen recipe and every EXPECTED.json field match. +- `python3 -I -O -B research/complex-x4-target-forest/test_package.py`: 9 PASS. + Covers underbilling, nonminimal valid forest, cycle, arbitrary-target omission, + private clearing, panel boundary, source corruption and minimal relocated source loading/census. +- Eight original package tests also passed in normal CPython 3.14.6; the ninth + initial-clear control was subsequently added and all nine passed under `-O`. +- Independent checker ran normally and under optimized Python. No checks depend + on Python `assert`. +- `python3 -B scripts/verify_selected_result.py`: PASS; selected kappa unchanged. +- `python3 -m unittest tests.test_selected_result`: 5 PASS. +- Main was fetched again and remains the exact base. The final overlap inventory + contained 721 open PRs through #931. Relevant #901/#909/#816/#917 and #883/#916 + have different documented scope; no competing selected-X4 forest was found. +- No pinned sprint issue existed. Claim and completion are recorded locally. + +## Coverage limits + +The scalar interpreters do not execute physical frame, Clifford or phase events. +The replacement is confined to the original zero-frame panel, and all non-scalar +records and paid profiles compare equal. This is not a fresh native physical +admission, global owner/hosting/invoice/assembly or cold supplier replay. + +`make verify`, `make frontier799-verify`, Linux/hosted CI and Lean were not run. +This isolated research package changes no existing generator, selected +certificate or upstream file. Its complete relevant finite checks are the +commands above; broad historical regeneration is not used as evidence for it. +The 74-bit reverse prefix remains within the inherited 192-bit allowance but +does not discharge all-size compiler, realization, hosting, precision/tape or +analytic obligations. No new kappa or full multiplication-theorem proof. diff --git a/research/complex-x4-target-forest/experiment.py b/research/complex-x4-target-forest/experiment.py new file mode 100644 index 0000000000..b388430278 --- /dev/null +++ b/research/complex-x4-target-forest/experiment.py @@ -0,0 +1,268 @@ +"""Selected-X4 signed target forests; Ross Richardson + OpenAI Codex, Apache-2.0. + +Forest mechanism: Oscar Fennell PR759, dd-hemant PR816; X4 pair precedent: +ToikY PR901. No pending implementation is imported. +""" +import gzip +import hashlib +import json +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +import tarfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = 'research/community-frontier799-audit/integrated799-replay.tar.gz' +WORDPIN = 'research/gauge44-frames-x/construction/jx/LOCAL-PINS-jx-X4.json' +WORK = ('W', 0) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(',', ':')).encode() + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def load(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + for path, digest in pins['files'].items(): + require(sha((ROOT / path).read_bytes()) == digest, 'source pin: ' + path) + data = {} + with tarfile.open(ROOT / ARCHIVE) as archive: + for name, digest in pins['members'].items(): + payload = archive.extractfile(name).read() + if name.endswith('.gz'): + payload = gzip.decompress(payload) + require(sha(payload) == digest, 'member pin: ' + name) + data[Path(name).name.split('.')[0]] = json.loads(payload) + word, programs, checks = (data[k] for k in ('CANONICAL-WORD', 'LOCAL-PROGRAMS', 'LOCAL-CHECKS')) + inherited = data['INDEPENDENT-LOCAL-REPLAY']['local'] + selected = json.loads((ROOT / WORDPIN).read_text()) + require(pins['members']['native/local/CANONICAL-WORD.json.gz'] == selected['canonical_sha256'], 'selected word binding') + for orientation in ('forward', 'backward'): + require(sha(canonical(programs[orientation])) == selected['program_sha256'][orientation] == checks[orientation]['sha256'], 'selected program binding') + checks[orientation]['inherited_prefix_upper'] = inherited[orientation]['prefix_l1_upper'] + checks[orientation]['charged_payload_bits'] = inherited[orientation]['charged_payload_bits'] + return word, programs, checks + + +def cost(q): + q = Q(q) + if not q: + return 0 + a, d = abs(q.numerator), q.denominator + require(d & (d - 1) == 0, 'non-dyadic') + return 3 + a.bit_length() - 1 + bin(a).count('1') + d.bit_length() - 1 + + +def matrix(word): + rows = {r: {} for r in range(112, 224)} + for tag, t, s, n, d, frame in word['compensation']: + require(tag == 'add' and frame == 0 and t in rows and 224 <= s < 728, 'compensation shape') + require(s not in rows[t], 'duplicate coefficient') + rows[t][s] = Q(n, d) + return rows + + +def difference(a, b, sign): + return {s: q for s in a.keys() | b.keys() if (q := a.get(s, 0) - sign * b.get(s, 0))} + + +def edges_for(rows): + edges = [] + for t, row in sorted(rows.items()): + edges.append([-1, t, 0, sum(cost(q) for q in row.values())]) + for u in sorted(rows): + if u >= t: + break + for sign in (-1, 1): + weight = 8 + sum(cost(q) for q in difference(row, rows[u], sign).values()) + edges.append([u, t, sign, weight]) + return edges + + +def synthesize(word): + rows = matrix(word) + edges = edges_for(rows) + parent = {v: v for v in [-1, *rows]} + def root(x): + while parent[x] != x: + parent[x] = parent[parent[x]] + x = parent[x] + return x + selected = [] + # All edge weights are exact. The OS seed only breaks tied costs. + for e in sorted(edges, key=lambda e: (e[3], sha(canonical([34, *e[:3]])))): + u, v, _, _ = e + a, b = root(u), root(v) + if a != b: + parent[a] = b + selected.append(e) + require(len(selected) == 112, 'disconnected forest') + return {'seed': 34, 'edges': selected, 'complex_primitive_floor': sum(e[3] for e in selected), + 'census_edges': len(edges), 'census_sha256': sha(canonical(edges))} + + +def forest(word, recipe): + rows = matrix(word) + graph = {v: [] for v in [-1, *rows]} + require(len(recipe['edges']) == 112, 'tree edge count') + for u, v, sign, weight in recipe['edges']: + require(u in graph and v in graph and u != v and sign in (-1, 0, 1), 'bad tree edge') + require((sign == 0) == (-1 in (u, v)), 'bad root sign') + graph[u].append((v, sign)); graph[v].append((u, sign)) + parents, order = {}, [-1] + for u in order: + for v, sign in sorted(graph[u]): + if v == parents.get(u, (None,))[0]: + continue + require(v not in order, 'tree cycle') + parents[v] = (u, sign) + order.append(v) + require(len(order) == 113, 'tree disconnected') + preparation = [['add', t, p, -s, 1, 0] for t in reversed(order[1:]) for p, s in [parents[t]] if p != -1] + middle = [] + for t in order[1:]: + p, sign = parents[t] + row = rows[t] if p == -1 else difference(rows[t], rows[p], sign) + middle += [['add', t, h, q.numerator, q.denominator, 0] for h, q in sorted(row.items())] + restoration = [['add', t, p, s, 1, 0] for t in order[1:] for p, s in [parents[t]] if p != -1] + return preparation + middle + restoration, len(preparation), parents + + +def event(op, orientation): + tag, t, s, n, d, frame = op + if orientation == 'backward': + t, s, n = s, t, -n + return ['scalar', [tag, ['L', t], ['L', s], n, d], frame] + + +def replace(program, word, new, orientation): + start = 1 + len(word['precondition']) + stop = start + len(word['compensation']) + require(program[start:stop] == [event(op, orientation) for op in word['compensation']], 'compensation boundary') + result = program[:start] + [event(op, orientation) for op in new] + program[stop:] + require([e for e in program if e[0] != 'scalar'] == [e for e in result if e[0] != 'scalar'], 'non-scalar changed') + return result + + +def lower(op): + tag, t = op[0], tuple(op[1]) + if tag == 'clear': + return [('clear', t)] + if tag == 'copy': + return [('copy', t, tuple(op[2]))] + if tag == 'scale': + q = Q(op[2], op[3]); a, d = abs(q.numerator), q.denominator + require(a and a & (a-1) == 0 and d & (d-1) == 0, 'non-dyadic scale') + shift = a.bit_length() - d.bit_length() + return [('double' if shift > 0 else 'halve', t)] * abs(shift) + ([('negate', t)] if q < 0 else []) + require(tag == 'add', 'unknown scalar') + s, q = tuple(op[2]), Q(op[3], op[4]) + require(s != t and s != WORK and t != WORK and q, 'invalid add') + out = [('clear', WORK)] + for i, digit in enumerate(bin(abs(q.numerator))[2:]): + if i: + out.append(('double', WORK)) + if digit == '1': + out.append(('add', WORK, s)) + out += [('halve', WORK)] * (q.denominator.bit_length() - 1) + out += [('add' if q > 0 else 'subtract', t, WORK), ('clear', WORK)] + require(len(out) == cost(q), 'lowering cost') + return out + + +def step(rows, op): + tag, t = op[:2] + if tag == 'clear': + rows[t] = {} + elif tag == 'copy': + rows[t] = rows[op[2]].copy() + elif tag in ('double', 'halve', 'negate'): + q = {'double': Q(2), 'halve': Q(1, 2), 'negate': Q(-1)}[tag] + rows[t] = {j: q*x for j,x in rows[t].items()} + elif tag in ('add', 'subtract'): + sign = 1 if tag == 'add' else -1 + for j, x in rows[op[2]].items(): + q = rows[t].get(j, 0) + sign*x + if q: + rows[t][j] = q + else: + rows[t].pop(j, None) + else: + raise ValueError('unknown primitive') + + +def replay(program, orientation): + regs = [('L', i) for i in range(728)] + [('C', i) for i in range(8)] + [WORK] + rows = {r: {i: Q(1)} for i, r in enumerate(regs)} + envelopes = {r: Q(1) for r in regs} + peak = Q(1); depth = 0 + counts, paid = Counter(), Counter() + digest = hashlib.sha256(); macros = 0 + for e in program: + if e[0] == 'climb': + paid[e[5]] += 1 + elif e[0] == 'center': + paid[e[4]] += 1 + elif e[0] != 'scalar': + require(e[0] in ('phase','adapter','residual_adapter'), 'unknown event') + if e[0] != 'scalar': + continue + macros += 1 + for op in lower(e[1]): + step(rows, op) + tag, t = op[:2] + if tag == 'clear': envelopes[t] = Q(0) + elif tag == 'copy': envelopes[t] = envelopes[op[2]] + elif tag in ('add','subtract'): envelopes[t] += envelopes[op[2]] + elif tag == 'double': envelopes[t] *= 2 + elif tag == 'halve': envelopes[t] /= 2 + peak = max(peak, envelopes[t]) + # Exact dyadic grid depth of every actual intermediate row. + depth = max(depth, max((q.denominator.bit_length()-1 for q in rows[t].values()), default=0)) + counts[tag] += 2 + digest.update(canonical([e[2], op]) + b'\n') + if e[1][0] == 'add': + require(not rows[WORK], 'work not cleared at macro boundary') + for i in range(728): + expected = {i: Q(1)} + if orientation == 'forward' and 112 <= i < 224: expected[i-112] = Q(1) + if orientation == 'backward' and i < 112: expected[i+112] = Q(-1) + require(rows[('L',i)] == expected, 'full arbitrary-input map at ' + str(i)) + require(all(not rows[r] for r in regs if r[0] != 'L'), 'private input not erased') + return {'real_primitives':sum(counts.values()), 'macros':macros, 'primitive_counts':dict(sorted(counts.items())), + 'primitive_sha256':digest.hexdigest(), 'program_sha256':sha(canonical(program)), + 'positive_prefix_upper':str(peak), 'prefix_bits':peak.numerator.bit_length()-peak.denominator.bit_length()+1, + 'exact_fractional_bits':depth, 'arbitrary_input_columns':len(regs), + 'paid_profile':{str(k):v for k,v in sorted(paid.items())}} + + +def boundary(word, operations, orientation, target_inputs=True): + rows = {('L',i):({i:Q(1)} if target_inputs or not 112 <= i < 224 else {}) for i in range(728)} + rows[WORK] = {728: Q(1)} + for op in operations: + for primitive in lower(event(op, orientation)[1]): step(rows, primitive) + return rows + + +def controls(word, new, prep): + old = boundary(word,word['compensation'],'forward') + require(boundary(word,new,'forward') == old, 'compensation mismatch') + # A missing preparation is invisible with zero target input: check this trap. + require(boundary(word,new[prep:],'forward',False) == boundary(word,word['compensation'],'forward',False), 'zero-target control setup') + mutants = {'missing_preparation':new[prep:], 'missing_restoration':new[:-prep], + 'wrong_order':list(reversed(new)), 'missing_middle':new[:prep]+new[prep+1:]} + changed = [x[:] for x in new]; changed[prep][3] *= -1; mutants['wrong_coefficient_sign']=changed + for label, ops in mutants.items(): + require(boundary(word,ops,'forward') != old, 'control passed: '+label) + require(boundary(word,new,'backward') == boundary(word,word['compensation'],'backward'), 'dual boundary') + return sorted(mutants) diff --git a/research/complex-x4-target-forest/independent.py b/research/complex-x4-target-forest/independent.py new file mode 100644 index 0000000000..c8e716acb1 --- /dev/null +++ b/research/complex-x4-target-forest/independent.py @@ -0,0 +1,313 @@ +#!/usr/bin/env python3 +"""Independent Fraction/Prim replay for the selected X4 target-forest experiment. + +No imports from the experiment's generator or pending predecessors. Graph prices +are obtained by constructing old binary-Horner primitive lists, rather than by +using the generator's integer coefficient-cost formula. Attribution: PR799 X4 +sources, PR901 target pairs, PR816 signed forests and PR759 binary forests. +Prepared with substantial OpenAI Codex assistance; Apache-2.0. +""" +from __future__ import annotations + +import argparse +from collections import deque +from fractions import Fraction as Q +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path +import tarfile + +ARCHIVE_SHA256 = "70dfdfcf2ff95352c6020ee9dfca6dca9032b33c10daed3f3dc574c014f4e2cb" +MEMBER_PINS = { + "native/local/CANONICAL-WORD.json.gz": "1c0e9da767d4418f70016af599e4a447a3f7777acabe930318459c0fbbd260aa", + "native/local/LOCAL-PROGRAMS.json.gz": "223c2bb27ad68a4e9468c3ddaece1899d577b661190922fdd25f5976052c4cab", + "native/local/LOCAL-CHECKS.json": "bbde5cea7bfd5df3d3ee7dfada0ff9d165af43a4d1dec6a9597cbfd8f87cc3b2", +} + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +@lru_cache(None) +def primitive_word(q): + """Construct S-preserving, W-clearing old Horner for T += q*S.""" + q = Q(q) + if not q: + return () + denominator = q.denominator + require(denominator & (denominator - 1) == 0, "non-dyadic coefficient") + ops = [("clear", "W")] + for index, bit in enumerate(bin(abs(q.numerator))[2:]): + if index: + ops.append(("double", "W")) + if bit == "1": + ops.append(("add", "W", "S")) + while denominator > 1: + ops.append(("half", "W")) + denominator //= 2 + ops += [("add" if q > 0 else "sub", "T", "W"), ("clear", "W")] + return tuple(ops) + + +def row_difference(a, b, sign): + return {source: q for source in a.keys() | b.keys() + if (q := a.get(source, Q(0)) - sign * b.get(source, Q(0)))} + + +def row_price(row): + return sum(len(primitive_word(q)) for q in row.values()) + + +def rows_from_word(word): + rows = {} + for op in word["compensation"]: + require(len(op) == 6 and op[0] == "add" and op[5] == 0, + "compensation must be zero-frame additions") + _, target, source, numerator, denominator, _ = op + q = Q(numerator, denominator) + require(q and source not in rows.get(target, {}), "zero or repeated coefficient") + rows.setdefault(target, {})[source] = q + helpers = set().union(*(set(row) for row in rows.values())) + require(not helpers.intersection(rows), "target/helper alias") + require(all(word["start"][r] == 0 for r in set(rows) | helpers), + "forest register does not enter in the zero frame") + require(all(op[-1] == 0 for op in word["precondition"]), + "precondition changes the frame used by the forest") + return rows, helpers + + +def complete_graph(rows): + targets = sorted(rows) + edges = [(-1, t, 0, row_price(rows[t])) for t in targets] + for offset, left in enumerate(targets): + for right in targets[offset + 1:]: + for sign in (-1, 1): + price = row_price(row_difference(rows[left], rows[right], sign)) + edges.append((left, right, sign, price + 2 * len(primitive_word(Q(1))))) + return edges + + +def prim_cost(nodes, edges): + adjacency = {n: [] for n in nodes} + for left, right, _, weight in edges: + adjacency[left].append((right, weight)) + adjacency[right].append((left, weight)) + remaining = set(nodes) + distance = {node: float("inf") for node in nodes} + distance[-1] = 0 + result = 0 + while remaining: + vertex = min(remaining, key=lambda n: (distance[n], n)) + require(distance[vertex] != float("inf"), "disconnected full graph") + result += distance[vertex] + remaining.remove(vertex) + for neighbour, price in adjacency[vertex]: + if neighbour in remaining: + distance[neighbour] = min(distance[neighbour], price) + return result + + +def check_tree(recipe, rows, graph): + edges = [tuple(e) for e in recipe["edges"]] + nodes = set(rows) | {-1} + require(len(edges) == len(rows), "tree must have one edge per target") + adjacency = {n: [] for n in nodes} + prices = {(a, b, s): w for a, b, s, w in graph} + for a, b, sign, weight in edges: + key = (min(a, b), max(a, b), sign) + require(key in prices and weight == prices[key], "incorrect edge or edge price") + adjacency[a].append((b, sign, weight)) + adjacency[b].append((a, sign, weight)) + parent = {-1: None} + order = [] + queue = deque([-1]) + while queue: + a = queue.popleft() + for b, sign, weight in sorted(adjacency[a]): + if b == parent[a]: + continue + require(b not in parent, "cycle or repeated edge") + parent[b] = a + order.append((b, a, sign)) + queue.append(b) + require(set(parent) == nodes, "disconnected recipe") + cost = sum(e[3] for e in edges) + require(cost == prim_cost(nodes, graph), "recipe cost differs from independent Prim optimum") + # Check the MST cycle property for EVERY signed edge, including unused signs. + maximum = {} + for start in sorted(nodes): + todo = [(start, None, 0)] + while todo: + node, previous, peak = todo.pop() + maximum[start, node] = peak + for neighbour, _, weight in adjacency[node]: + if neighbour != previous: + todo.append((neighbour, node, max(peak, weight))) + for a, b, _, weight in graph: + require(weight >= maximum[a, b], "negative cycle-exchange opportunity") + return order, cost + + +def forest_operations(order, rows): + prepare = [(child, parent, Q(-sign)) for child, parent, sign in reversed(order) + if parent != -1] + inject = [] + for child, parent, sign in order: + row = rows[child] if parent == -1 else row_difference(rows[child], rows[parent], sign) + inject.extend((child, source, q) for source, q in sorted(row.items())) + restore = [(child, parent, Q(sign)) for child, parent, sign in order if parent != -1] + return prepare, inject, restore + + +def linear_replay(ops, registers, backward=False): + state = {r: {r: Q(1)} for r in registers} + for target, source, q in ops: + if backward: + target, source, q = source, target, -q + require(target != source, "aliased shear") + row = state[target].copy() + for column, value in state[source].items(): + result = row.get(column, Q(0)) + q * value + if result: + row[column] = result + else: + row.pop(column, None) + state[target] = row + return state + + +def expected_map(rows, helpers, backward): + state = {r: {r: Q(1)} for r in set(rows) | helpers} + for target, row in rows.items(): + for source, q in row.items(): + if backward: + state[source][target] = -q + else: + state[target][source] = q + return state + + +def check_microcircuit(q): + state = {name: {name: Q(1)} for name in ("S", "T", "W")} + for op in primitive_word(q): + tag, target, *rest = op + if tag == "clear": + state[target] = {} + elif tag in ("double", "half"): + factor = Q(2) if tag == "double" else Q(1, 2) + state[target] = {k: v * factor for k, v in state[target].items()} + else: + factor = 1 if tag == "add" else -1 + for key, value in state[rest[0]].items(): + value = state[target].get(key, Q(0)) + factor * value + if value: + state[target][key] = value + else: + state[target].pop(key, None) + require(state == {"S": {"S": Q(1)}, "T": {"T": Q(1), "S": q}, "W": {}}, + "coefficient primitive lowering failed on arbitrary S,T,W") + + +def verify(recipe, word): + rows, helpers = rows_from_word(word) + graph = complete_graph(rows) + order, optimum = check_tree(recipe, rows, graph) + prepare, inject, restore = forest_operations(order, rows) + operations = prepare + inject + restore + require(sum(len(primitive_word(q)) for _, _, q in operations) == optimum, + "realization price differs from graph price") + coefficients = sorted(set(q for _, _, q in operations)) + for q in coefficients: + check_microcircuit(q) + controls = [] + for backward in (False, True): + orientation = "backward" if backward else "forward" + expected = expected_map(rows, helpers, backward) + require(linear_replay(operations, expected, backward) == expected, + orientation + " arbitrary-input operator mismatch") + for label, mutant in ( + ("omit_prepare", inject + restore), + ("omit_restore", prepare + inject), + ("wrong_injection_sign", prepare + [(inject[0][0], inject[0][1], -inject[0][2])] + inject[1:] + restore), + ): + require(linear_replay(mutant, expected, backward) != expected, + orientation + " failed to reject " + label) + controls.append(orientation + ":" + label) + bad_edges = [list(e) for e in recipe["edges"]] + bad_edges[0][3] += 1 + try: + check_tree({"edges": bad_edges}, rows, graph) + except ValueError: + controls.append("incorrect_edge_price") + else: + raise ValueError("incorrect edge price accepted") + baseline = sum(row_price(row) for row in rows.values()) + return { + "status": "PASS_INDEPENDENT_X4_TARGET_FOREST", + "method": "Fraction symbolic maps; explicit Horner lists; Prim; all-edge cycle property", + "targets": len(rows), "helpers": len(helpers), "arbitrary_input_columns": len(rows) + len(helpers), + "signed_graph_edges": len(graph), "cycle_inequalities_checked": len(graph), + "roots": sum(parent == -1 for _, parent, _ in order), + "forest_edges": len(prepare), "scalar_macros": len(operations), + "unique_microcircuit_coefficients": len(coefficients), + "component_primitive_baseline": baseline, "component_primitive_optimum": optimum, + "real_primitive_baseline": 2 * baseline, "real_primitive_optimum": 2 * optimum, + "real_primitive_savings_each_orientation": 2 * (baseline - optimum), + "orientations": ["forward", "backward"], "negative_controls": controls, + "all_forest_registers_enter_in_zero_frame": True, + "scope": "Exact finite compensation operator and forest-class optimum only; no full theorem or kappa claim.", + } + + +def read_sources(path): + require(hashlib.sha256(path.read_bytes()).hexdigest() == ARCHIVE_SHA256, "source archive pin mismatch") + parsed = {} + with tarfile.open(path, "r:gz") as archive: + for name, digest in MEMBER_PINS.items(): + member = archive.extractfile(name) + require(member is not None, "missing source member") + payload = member.read() + if name.endswith(".gz"): + payload = gzip.decompress(payload) + require(hashlib.sha256(payload).hexdigest() == digest, "source member pin mismatch") + parsed[name] = json.loads(payload) + word = parsed["native/local/CANONICAL-WORD.json.gz"] + programs = parsed["native/local/LOCAL-PROGRAMS.json.gz"] + begin = 1 + len(word["precondition"]) + for orientation in ("forward", "backward"): + expected = [] + for _, target, source, numerator, denominator, frame in word["compensation"]: + if orientation == "backward": + target, source, numerator = source, target, -numerator + expected.append(["scalar", ["add", ["L", target], ["L", source], numerator, denominator], frame]) + require(programs[orientation][0] == ["phase", "zero_frame_precondition"], "wrong initial phase") + require(programs[orientation][begin:begin + len(expected)] == expected, + "canonical compensation/local program binding mismatch") + require(programs[orientation][begin + len(expected)] == ["phase", "entry_adapters"], + "compensation boundary mismatch") + return word, parsed["native/local/LOCAL-CHECKS.json"] + + +def main(): + here = Path(__file__).resolve().parent + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--recipe", type=Path, default=here / "RECIPE.json") + parser.add_argument("--archive", type=Path, + default=here.parent / "community-frontier799-audit/integrated799-replay.tar.gz") + args = parser.parse_args() + word, checks = read_sources(args.archive) + result = verify(json.loads(args.recipe.read_text()), word) + result["archive_sha256"] = ARCHIVE_SHA256 + result["source_payload_sha256"] = MEMBER_PINS + result["source_local_programs_compensation_bound"] = True + result["inherited_full_real_primitive_bounds"] = { + orientation: checks[orientation]["real_component_primitive_bound"] for orientation in checks} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/complex-x4-target-forest/test_package.py b/research/complex-x4-target-forest/test_package.py new file mode 100644 index 0000000000..86b27a3591 --- /dev/null +++ b/research/complex-x4-target-forest/test_package.py @@ -0,0 +1,97 @@ +"""Focused mathematical and package failure controls (stdlib, offline).""" +import copy +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +import experiment as e +import independent as ind + + +class Package(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.word,cls.programs,cls.checks=e.load() + cls.recipe=json.loads((HERE/'RECIPE.json').read_text()) + cls.new,cls.prep,_=e.forest(cls.word,cls.recipe) + cls.rows,cls.helpers=ind.rows_from_word(cls.word) + cls.graph=ind.complete_graph(cls.rows) + + def test_underbilled_basis_rejected(self): + recipe=copy.deepcopy(self.recipe) + next(x for x in recipe['edges'] if x[0]!=-1)[3]-=8 + with self.assertRaisesRegex(ValueError,'edge price'): + ind.check_tree(recipe,self.rows,self.graph) + + def test_nonminimal_valid_forest_rejected(self): + # Root-only tree implements the original correct panel, but is not minimal. + recipe={'edges':[x for x in self.graph if x[0]==-1]} + new,prep,_=e.forest(self.word,recipe) + self.assertEqual(prep,0) + self.assertEqual(e.boundary(self.word,new,'forward'),e.boundary(self.word,self.word['compensation'],'forward')) + with self.assertRaisesRegex(ValueError,'Prim optimum'): + ind.check_tree(recipe,self.rows,self.graph) + + def test_cycle_rejected(self): + recipe=copy.deepcopy(self.recipe);recipe['edges'][-1]=recipe['edges'][0] + with self.assertRaisesRegex(ValueError,'cycle|repeated'): + ind.check_tree(recipe,self.rows,self.graph) + + def test_missing_preparation_arbitrary_targets(self): + original=self.word['compensation'];bad=self.new[self.prep:] + self.assertEqual(e.boundary(self.word,bad,'forward',False),e.boundary(self.word,original,'forward',False)) + self.assertNotEqual(e.boundary(self.word,bad,'forward'),e.boundary(self.word,original,'forward')) + + def test_missing_private_clear(self): + op=['add',['L',0],['L',1],-3,4] + rows={('L',0):{0:e.Q(1)},('L',1):{1:e.Q(1)},e.WORK:{2:e.Q(1)}} + for p in e.lower(op)[:-1]:e.step(rows,p) + self.assertEqual(rows[('L',0)],{0:e.Q(1),1:e.Q(-3,4)}) + self.assertTrue(rows[e.WORK]) + + def test_missing_initial_work_clear(self): + op=['add',['L',0],['L',1],3,4] + rows={('L',0):{0:e.Q(1)},('L',1):{1:e.Q(1)},e.WORK:{2:e.Q(1)}} + for primitive in e.lower(op)[1:]:e.step(rows,primitive) + self.assertFalse(rows[e.WORK]) + self.assertIn(2,rows[('L',0)]) + self.assertNotEqual(rows[('L',0)],{0:e.Q(1),1:e.Q(3,4)}) + + def test_wrong_program_boundary(self): + p=copy.deepcopy(self.programs['forward']);p[169][1][3]*=-1 + with self.assertRaisesRegex(ValueError,'compensation boundary'): + e.replace(p,self.word,self.new,'forward') + + def test_source_pin_corruption(self): + with tempfile.TemporaryDirectory() as temp: + root=Path(temp) + for path in json.loads((HERE/'SOURCES.json').read_text())['files']: + target=root/path;target.parent.mkdir(parents=True,exist_ok=True) + shutil.copyfile(e.ROOT/path,target) + (root/e.WORDPIN).write_text('{}') + with patch.object(e,'ROOT',root),self.assertRaisesRegex(ValueError,'source pin'): + e.load() + + def test_relocated_minimal_source_closure(self): + with tempfile.TemporaryDirectory(prefix='X4 forest with spaces ') as temp: + root=Path(temp) + package=root/'research/complex-x4-target-forest';package.mkdir(parents=True) + for name in ('experiment.py','independent.py','RECIPE.json','SOURCES.json'): + shutil.copyfile(HERE/name,package/name) + for path in json.loads((HERE/'SOURCES.json').read_text())['files']: + target=root/path;target.parent.mkdir(parents=True,exist_ok=True) + shutil.copyfile(e.ROOT/path,target) + code="import sys;sys.path.insert(0,sys.argv[1]);import experiment as e;w,p,c=e.load();r=e.synthesize(w);print(r['complex_primitive_floor'])" + run=subprocess.run([sys.executable,'-I','-O','-B','-c',code,str(package)],cwd=root,text=True,capture_output=True) + self.assertEqual(run.returncode,0,run.stderr) + self.assertEqual(run.stdout.strip(),'10883') + + +if __name__=='__main__':unittest.main() diff --git a/research/complex-x4-target-forest/verify.py b/research/complex-x4-target-forest/verify.py new file mode 100644 index 0000000000..cbf558cf4b --- /dev/null +++ b/research/complex-x4-target-forest/verify.py @@ -0,0 +1,56 @@ +#!/usr/bin/env python3 +"""Offline finite scalar certificate; no selected frontier mutation.""" +import argparse +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import experiment as e + + +def compute(): + word, programs, checks = e.load() + recipe = json.loads((HERE / 'RECIPE.json').read_text()) + e.require(e.canonical(recipe) == e.canonical(e.synthesize(word)), 'recipe does not match complete census') + new, prep, parents = e.forest(word, recipe) + e.require(sum(e.cost(e.Q(op[3], op[4])) for op in new) == recipe['complex_primitive_floor'], 'attained forest floor') + result = {'status':'PASS_X4_TARGET_FOREST', 'seed':34, 'base':'91a2094f2e022930069e8cfdc810a3ea1b81cd09', + 'compensation_original_additions':len(word['compensation']), 'compensation_new_additions':len(new), + 'preparation_additions':prep, 'restoration_additions':prep, 'middle_additions':len(new)-2*prep, + 'roots':sum(p==-1 for p,s in parents.values()), 'complex_compensation_floor':recipe['complex_primitive_floor'], + 'census_edges':recipe['census_edges'], 'census_sha256':recipe['census_sha256'], + 'controls':e.controls(word,new,prep), 'programs':{}} + for orientation in ('forward','backward'): + baseline=e.replay(programs[orientation],orientation) + e.require(baseline['real_primitives'] == checks[orientation]['real_component_primitive_bound'], 'baseline count') + e.require(baseline['macros'] == checks[orientation]['scalar_macros'], 'baseline macros') + e.require(baseline['positive_prefix_upper'] == checks[orientation]['inherited_prefix_upper'], 'baseline prefix mismatch') + candidate=e.replay(e.replace(programs[orientation],word,new,orientation),orientation) + e.require(candidate['paid_profile'] == baseline['paid_profile'] == checks[orientation]['paid_profile'], 'paid profile changed') + e.require(candidate['prefix_bits'] <= checks[orientation]['charged_payload_bits'], 'prefix exceeds inherited allocation') + result['programs'][orientation]={'baseline':baseline,'candidate':candidate, + 'saved_real_primitives':baseline['real_primitives']-candidate['real_primitives']} + print(orientation, 'real',baseline['real_primitives'],'->',candidate['real_primitives'], + 'prefix_bits',baseline['prefix_bits'],'->',candidate['prefix_bits'],flush=True) + import independent + result['independent'] = independent.verify(recipe,word) + return result + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write',type=Path,help='development only: save a newly computed receipt') + args=parser.parse_args() + result=compute() + if args.write: + # Explicit development command only. Normal verification is read-only. + with args.write.open('x') as out: out.write(json.dumps(result,indent=2,sort_keys=True)+'\n') + else: + expected=json.loads((HERE/'EXPECTED.json').read_text()) + e.require(e.canonical(result)==e.canonical(expected),'receipt mismatch') + print('PASS_X4_TARGET_FOREST compensation=6320->2324 saved_real=47690/47690 forest_floor=10883 columns=737 orientations=2 no_new_kappa') + + +if __name__=='__main__': main()