diff --git a/research/h6-mixed-pair-capture/CERTIFICATE.json b/research/h6-mixed-pair-capture/CERTIFICATE.json new file mode 100644 index 0000000000..4495756776 --- /dev/null +++ b/research/h6-mixed-pair-capture/CERTIFICATE.json @@ -0,0 +1,539 @@ +{ + "H6_ports": 30960, + "all_labels": 14670, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "baseline_abs5_over16_parts": { + "mixed_mixed": 3225600, + "pure_pure": 138240 + }, + "baseline_helper_parts": { + "mixed_source": 210585600, + "pure_source": 16727040 + }, + "baseline_scatter_parts": { + "mixed_mixed": 412876800, + "mixed_pure_each_orientation": 33177600, + "pure_pure": 1105920 + }, + "fixture": { + "domain": { + "mixed_label_pairs": [ + [ + 11, + 20 + ], + [ + 63, + 20 + ], + [ + 63, + 108 + ], + [ + 116, + 41 + ] + ], + "seed": 83, + "source_pair": [ + 63, + 108 + ] + }, + "indices": [ + 167, + 188, + 226, + 241, + 810, + 819, + 931, + 938, + 1423, + 1442, + 1444, + 1449, + 1491, + 1579, + 1787, + 2154, + 4840, + 4841, + 17320, + 17321, + 17496, + 17497, + 30082, + 30083 + ], + "new": { + "capture_entries": 72, + "component_primitives": 3160, + "helpers": 62, + "scatter_entries": 160 + }, + "old": { + "capture_entries": 72, + "component_primitives": 4056, + "helpers": 72, + "scatter_entries": 216 + }, + "old_orientations": [ + { + "all_input_columns": 120, + "data_ports": 24, + "dual": false, + "helper_path": [ + 1, + 15, + 1 + ], + "helper_roles": 72, + "logical_dirt_return": true, + "physical_helper_endpoint": "FULL applied to its original dirt, not literal physical entrance" + }, + { + "all_input_columns": 120, + "data_ports": 24, + "dual": true, + "helper_path": [ + 1, + 15, + 1 + ], + "helper_roles": 72, + "logical_dirt_return": true, + "physical_helper_endpoint": "FULL applied to its original dirt, not literal physical entrance" + } + ], + "orientations": [ + { + "all_input_columns": 110, + "data_ports": 24, + "dual": false, + "helper_path": [ + 1, + 15, + 1 + ], + "helper_roles": 62, + "logical_dirt_return": true, + "physical_helper_endpoint": "FULL applied to its original dirt, not literal physical entrance" + }, + { + "all_input_columns": 110, + "data_ports": 24, + "dual": true, + "helper_path": [ + 1, + 15, + 1 + ], + "helper_roles": 62, + "logical_dirt_return": true, + "physical_helper_endpoint": "FULL applied to its original dirt, not literal physical entrance" + } + ] + }, + "full_E8_cosets": 256, + "invoice": { + "abs5_over16_entries_old_and_new": 3363840, + "capture_entries_old_and_new": 227312640, + "capture_range_new": "E+2X", + "capture_range_old": "E+X", + "capture_range_scope": "Forward logical mixed-source capture cut only; full and dual precision remain open.", + "component_primitive_saving": 3516825600, + "conditional_hosted_helper_deltas": [ + { + "coverage_deficit_change": "0", + "formal_stock_removed": "155520000", + "m": 49, + "mass_rank_terms_removed": [ + [ + "622080000", + 1 + ], + [ + "4665600000", + 15 + ], + [ + "2332800000", + 15 + ] + ], + "pad": 15, + "rank_mass_removed": "7620480000", + "replication_q": 2, + "scope": "Existing fractional row-stock/padding convention only; not a physical reserve proof.", + "stages": 3 + }, + { + "coverage_deficit_change": "0", + "formal_stock_removed": "129600000", + "m": 81, + "mass_rank_terms_removed": [ + [ + "1036800000", + 1 + ], + [ + "7776000000", + 15 + ], + [ + "1684800000", + 13 + ] + ], + "pad": 13, + "rank_mass_removed": "10497600000", + "replication_q": 4, + "scope": "Existing fractional row-stock/padding convention only; not a physical reserve proof.", + "stages": 5 + }, + { + "coverage_deficit_change": "0", + "formal_stock_removed": "120960000", + "m": 113, + "mass_rank_terms_removed": [ + [ + "1451520000", + 1 + ], + [ + "10886400000", + 15 + ], + [ + "1330560000", + 11 + ] + ], + "pad": 11, + "rank_mass_removed": "13668480000", + "replication_q": 6, + "scope": "Existing fractional row-stock/padding convention only; not a physical reserve proof.", + "stages": 7 + } + ], + "helper_path": [ + 1, + 15, + 1 + ], + "helpers_removed": 103680000, + "new_asymmetric_combined_dual": 6250867840, + "new_asymmetric_combined_forward": 6250865392, + "new_compensation_component_primitives": 6007265280, + "new_fractional_denominator": false, + "new_full_local_histogram": { + "1": 247265280, + "15": 123632640, + "16": 59760, + "17": 1600, + "8": 4336, + "9": 32 + }, + "new_full_local_rank_mass": 2102773216, + "new_helpers": 123632640, + "new_scatter_entries": 260536320, + "old_compensation_component_primitives": 9524090880, + "old_full_local_rank_mass": 3865333216, + "old_helpers": 227312640, + "old_scatter_entries": 480337920, + "physical_precision_allocator_tape_stock_joint_kappa": "unresolved, not inferred from semantic invoices", + "positive_rank_helper_transitions_removed": 311040000, + "scatter_entries_removed": 219801600 + }, + "mixed_block_classes": [ + { + "A": -1, + "B": -1, + "C": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "rank": 0, + "sigma": null + }, + { + "A": -1, + "B": 0, + "C": [ + [ + "-1/16", + "-1/16" + ], + [ + "-1/16", + "-1/16" + ] + ], + "rank": 1, + "sigma": 1 + }, + { + "A": -1, + "B": 1, + "C": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "rank": 0, + "sigma": null + }, + { + "A": -1, + "B": 2, + "C": [ + [ + "1/16", + "5/16" + ], + [ + "5/16", + "1/16" + ] + ], + "rank": 2, + "sigma": null + }, + { + "A": 0, + "B": -1, + "C": [ + [ + "-1/16", + "1/16" + ], + [ + "1/16", + "-1/16" + ] + ], + "rank": 1, + "sigma": -1 + }, + { + "A": 0, + "B": 0, + "C": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "rank": 0, + "sigma": null + }, + { + "A": 0, + "B": 1, + "C": [ + [ + "1/16", + "-1/16" + ], + [ + "-1/16", + "1/16" + ] + ], + "rank": 1, + "sigma": -1 + }, + { + "A": 0, + "B": 2, + "C": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "rank": 0, + "sigma": null + }, + { + "A": 1, + "B": -1, + "C": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "rank": 0, + "sigma": null + }, + { + "A": 1, + "B": 0, + "C": [ + [ + "1/16", + "1/16" + ], + [ + "1/16", + "1/16" + ] + ], + "rank": 1, + "sigma": 1 + }, + { + "A": 1, + "B": 1, + "C": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "rank": 0, + "sigma": null + }, + { + "A": 1, + "B": 2, + "C": [ + [ + "-5/16", + "-1/16" + ], + [ + "-1/16", + "-5/16" + ] + ], + "rank": 2, + "sigma": null + }, + { + "A": 2, + "B": -1, + "C": [ + [ + "1/16", + "-5/16" + ], + [ + "-5/16", + "1/16" + ] + ], + "rank": 2, + "sigma": null + }, + { + "A": 2, + "B": 0, + "C": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "rank": 0, + "sigma": null + }, + { + "A": 2, + "B": 1, + "C": [ + [ + "-5/16", + "1/16" + ], + [ + "1/16", + "-5/16" + ] + ], + "rank": 2, + "sigma": null + }, + { + "A": 2, + "B": 2, + "C": [ + [ + "0", + "0" + ], + [ + "0", + "0" + ] + ], + "rank": 0, + "sigma": null + } + ], + "mixed_cap_degree": 7168, + "mixed_labels": 14400, + "new_helpers_per_mixed_source_label": 7424, + "pure_cap_degree_from_mixed": 144, + "pure_fiber_partition_sha256": "a2b7d7d9612e7fd277a53b38a8a645be81497a1c1cd8c86b10f07ca28c6447af", + "pure_fibers_sha256": "2ee07373f4d573bcf5f243e179b28d77b145f6892e084dbecfbe6299dbd7c67f", + "pure_label_multiplicity": 8, + "pure_labels_per_block": 135, + "pure_lines_per_block": 1080, + "pure_pair_count_rows_sha256": "2fc2a61f71f955712f0d00af37c710ba6431dc7253fe39bb5e4764fb4a510f4d", + "pure_pair_table_entries": 1166400, + "pure_points_sha256": "239f624c1c40f592ec3a98d9e619bc55894f5a5a6eafd769c84c6e5f6974ee65", + "rank1_mixed_caps_per_mixed_source_label": 7056, + "rank2_mixed_caps_per_mixed_source_label": 112, + "root_lines": 120, + "root_pair_table_entries": 14400, + "root_pair_table_sha256": "3efe686459d4eda6d29852203f633270bb9b0d44076849292d54180a90bda8e1", + "root_points_sha256": "499909f15616b21ed34b704054685a0c90c244fb81819ba458e076b8dd97308c", + "root_pure_table_entries": 129600, + "root_signature_sha256": "5100e2c79ff580e5430bd11d4c730b7ede15497bac74efc4aa2118efbd93f716", + "source_pins": { + "research/e8-complex-gauge-kernel/code/emit_gk.py": "4e415bff1d9f154496ed38e6889929b600aa0f3d583a375e8ca257ad8f51fa23", + "research/h6-compensation-network/README.md": "f7c74c4da5189762fcf837bb657d44fbd9f3b1dd3273bdc60c17bbcbc066f315", + "research/h6-compensation-network/construction/network.py": "e1bd9e43179835d16f9ec561ecd61585cf320a71550da49646f5d62da744b4f1", + "research/h6-compensation-network/contract/THEOREM.md": "9752a525d22d815341b70143a06221ad4b3aec0ae8a6447786d88d0291fef45f", + "research/h6-compensation-network/physical_compiler/universal.py": "165555cf3d84b28a1a555120ec597ae55098ccdf56c7ecef01f54c12a37bdcfe", + "research/h6-compensation-network/pricing/verify.py": "56f273853bd7089c3721bc023713993ac79e961d535694624cbb60dd7dcdd454", + "research/h6-compensation-network/routes/BUCKETED-SCHEMA.json": "376b0fe2128c12a1409792de7d0917da86f27e933b4d010c5a8322689b24ac8f", + "research/niemeier-lattices/code/e8_cubed.py": "ce24f397053c0ef5b26881bb7ccfab53fb0a3d762f2de04086fed8f7b41e8234" + }, + "status": "PASS_H6_MIXED_PAIR_CAPTURE" +} diff --git a/research/h6-mixed-pair-capture/CONTEXT.json b/research/h6-mixed-pair-capture/CONTEXT.json new file mode 100644 index 0000000000..8e6af98ea3 --- /dev/null +++ b/research/h6-mixed-pair-capture/CONTEXT.json @@ -0,0 +1,57 @@ +{ + "schema_version": 1, + "canonical_base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "pending_context": { + "pr": 4027, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4027", + "head": "1bcc4f8261d2dc322c98fa9e44c4ced43cd1cd95", + "author": "Ross Richardson (RossRichardson)", + "usage": "Conditional unchanged K profile and semantic bills; not imported or executed by the primary coefficient proof.", + "proof_path": "research/h6-u9-asymmetric-compensation/PROOF.md", + "proof_sections": "4-5", + "K_component_primitive_invoice_forward": 243600112, + "K_component_primitive_invoice_dual": 243602560, + "full_local_histogram_before": { + "1": 454625280, + "8": 4336, + "9": 32, + "15": 227312640, + "16": 59760, + "17": 1600 + } + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/pull/4027#issuecomment-6265404853", + "predecessors": [ + { + "name": "Dominik Scholz", + "source": "PR606 H6 geometry and factor" + }, + { + "name": "DreamingOfClouds", + "source": "H6 model disclosure on discussion1167" + }, + { + "name": "H6 compensation network contributors", + "source": "Frozen canonical bucket schema, arbitrary-dirt contract, native frame compiler and scalar tariff" + }, + { + "name": "Ross Richardson", + "source": "PR4027 exact asymmetric U9 K factor, full bucket splice and outstanding physical obligations" + } + ], + "license": "Apache-2.0; no predecessor source is copied or modified in this package.", + "publication_overlap": { + "utc": "2026-10-19T11:20:43Z", + "canonical_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "open_pr_bodies_including_drafts": 744, + "open_issues": 1, + "recent_updated_discussions": 30, + "parent_pr_comments": "All current comments at refresh; no competing same-scope claim or objection found.", + "related_distinct_prs": [ + 3649, + 3655, + 4027 + ], + "limitation": "Bounded discovery coverage; not a proof of novelty across every closed PR or old discussion." + } +} diff --git a/research/h6-mixed-pair-capture/PROOF.md b/research/h6-mixed-pair-capture/PROOF.md new file mode 100644 index 0000000000..e882435a84 --- /dev/null +++ b/research/h6-mixed-pair-capture/PROOF.md @@ -0,0 +1,209 @@ +# Same-frame signed-column factor for H6 compensation + +## 1. Inputs and precise claim + +Use the doubled-coordinate H6 ports of the frozen PR606 lineage: two pure +E8 projective squared-norm 16 shells of 1080 ports and mixed ports +`s+=(u,v), s-=(u,-v)` for 120 projective squared-norm 8 root lines in each block. +There are 30,960 ports. Define `tau=t·s/4`, +`f(z)=(z^3-4z)/48`, `K_ts=f(tau)`, and `C=I-K`. + +The inherited binary-label isometry satisfies +`p(t)·p(s)=1+tau (mod2)`. Every source has line `P_s=span(p(s))`, +every target has cap `Q_t=p(t)^perp`, in dimension 17. Compatible means +`p(t)·p(s)=0`, hence **odd tau**. Compatible C entries are nonzero; +the result removes proportional columns, not zero columns. + +We prove a new indexed factor `DG=C` by changing only mixed-source columns +within a fixed target-label bucket. It has 123,632,640 ordinary helpers, +instead of 227,312,640. Under the complete K-word and frame/erasure contracts +of `h6-compensation-network/contract/THEOREM.md`, it gives the same exact +arbitrary-dirt data map with the helper path `[1,15,1]`. This is a scoped +factor/construction proof conditional on those inherited contracts, not a +formal or unconditional multiplication theorem. + +## 2. Same actual source frame + +In doubled E8, `v-(-v)=2v`, so v and -v have identical lattice coset mod2. +Equivalently every root pairing signature is unchanged. The source's +`binary_labels` selects an invertible mod-two root Gram basis and applies +an injective affine isometry. Thus `p(s+)=p(s-)`, with identical packed +labels, not merely isomorphic abstract lines. + +The source pure fibers have 135 labels of multiplicity 8 per block; the +mixed fibers have 14,400 labels of multiplicity 2. Root, pure and zero cosets +are disjoint and exhaust the 256 E8/2E8 classes. The primary enumeration +uses all 120 pairing signatures. Independently, for doubled E8 vectors q,r, +`(q-r)/2` belongs to doubled E8 iff the coordinate differences are all 0 +or all 2 modulo 4 and their sum is 0 modulo 8. Hence a direct coset key is +`(min(q mod4, (q+2*ones) mod4), sum(q) mod8)`. +The independent implementation confirms the exact same pure partition. + +The canonical native compiler uses `ce.cgate(H,p)` as its source +representative. Equality of p therefore gives equality of actual source +operators, including phase. At a target bucket all targets likewise have +the same actual cap representative. Reusing a surviving helper's existing +zero→line→cap→FULL recipes introduces no new native conversion family. +This argument inherits the correctness of those recipes; the present +replay does not recompile or independently verify all native operators. + +## 3. Complete two-column classification + +For target mixed pair `(a,b),(a,-b)`, put `A=u·a/4`, `B=v·b/4`. +Each lies in `{-1,0,1,2}` for canonical root lines. Its C block is + +``` +delta - [[f(A+B), f(A-B)], + [f(A-B), f(A+B)]], +``` + +where delta is the identity only for `A=B=2`, and otherwise zero. +The sixteen attainable ordered classes are recorded exactly in the receipt. + +* If B=0 and A odd, the columns are equal; take sigma=+1. +* If A=0 and B odd, f is odd, so the columns are opposite; take sigma=-1. +* If one pairing is 2 and the other odd, the block has rank 2 with determinant + of absolute value 3/32. Keep both original helpers. +* All remaining blocks are zero, including the diagonal block after I-K + cancellation. No compatible nonzero entry is discarded. + +The rank 1 entries all have magnitude 1/16. For a pure target `(w,0)`, +the two columns are equal; for `(0,w)` they are opposite. In a compatible +pure target bucket, Cauchy gives `|u·w/4|<=sqrt(8)`, and odd integrality +then gives magnitude 1 pairing, hence every C entry has magnitude 1/16. +The whole eight-port target bucket has the same pairing parity. + +For a nonzero rank 1 block write its columns as `[v,sigma*v]`. Replace +`G=I_2, D=[v,sigma*v]` by `G=[1,sigma], D=v`. Exactly +`D G=[v,sigma*v]`. This changes no other block; full-rank mixed blocks +keep the original identity capture, and every pure-source helper is kept. +Summing over disjoint source-label/target-label blocks proves **DG=C** +for the complete indexed matrix. + +## 4. Arbitrary dirt, frames and both orientations + +Allocate an independent ordinary helper for each surviving factor row h. +Let its arbitrary logical entrance be e_h; correlations with other inputs +are allowed. Its G row uses only sources at one common line P_h, and its +D column uses only targets at one common cap Q_h. Nonzero C compatibility +gives `P_h subset Q_h`. Perform these complete phases: + +1. At ZERO, `y -= D e`. +2. Helpers climb to their source line and capture `Gx` there. Both reads + of a signed pair are emitted and paid; helper values are `e+Gx`. +3. Run the **complete unchanged** arbitrary-input K word on its disjoint + data and private registers. It maps y to `y+Kx`, returns logical x, + places sources at FULL and targets at their actual caps, and restores + its own auxiliary dirt under its paid contract. Its internal source + mutation is allowed. Do not move sources to FULL before this word. +4. Helpers climb line→cap and add `D(e+Gx)` to target buckets. +5. Helpers climb cap→FULL and subtract `Gx` at FULL. + +The helper ranks are 1,15,1, and both operands in every addition use +the identical actual frame. Data paths and K children are unchanged. +The forward output is + +`y-De+Kx+D(e+Gx)=y+(K+DG)x=y+x`, + +and each helper returns to e. This proves every independent dirt column +cancels. Its **physical** endpoint is FULL applied to e, not its physical +entrance e. Any wrapper restoring literal physical entrance, copied-total +erasure or recursive reserve remains a separately paid inherited obligation. + +Dualize every scalar addition in the same order, replacing +`a+=c*b` by `b-=c*a`, keeping the frame history. Initially the prefix +gives `h=e+D^T y`, capture subtracts `G^T(e+D^T y)` from x, K subtracts +`K^T y`, scatter removes `D^T y` from h, and cleanup adds `G^T e` to x. +Thus `x -> x-(K+DG)^T y=x-y`, y is unchanged, and helpers return to e. +The complete K interface, including arbitrary sources, targets, dirt and +private erasure, is essential in both orientations. + +`word.py` checks all source/target/helper basis columns in one seed 83 fixture +using exact sparse rationals and source-line/cap chronology. K is an +explicit exact macro contract there, not an implemented native K tape. +The full phasewise proof above is separate from that finite replay. + +## 5. Exhaustive reduced census and complete scalar invoice + +For every root line, among 120 root lines exactly 63 are orthogonal, +56 have odd pairing, and one is the same line. Every root has 72 compatible +pure target-label buckets. Each pure source has 64 compatible root lines, +64 pure-label buckets, 448 pure-port pairings of magnitude 1 and 64 of +magnitude 3. The two enumerations check the complete tables, including every +one of the 1,166,400 pure/pure entries. Products of these checked degrees, +with section 3's complete class split, give full-network counts. + +For each mixed source label: + +| Target caps | Number | Old helpers/cap | New helpers/cap | +| --- | ---: | ---: | ---: | +| Mixed rank 1 | 2*63*56=7056 | 2 | 1 | +| Mixed rank 2 | 2*56=112 | 2 | 2 | +| Pure rank 1 | 2*72=144 | 2 | 1 | + +Old helpers per mixed label are 14,624; new are 7,424. Thus removed helpers +are `M=14400*7200=103680000`. Pure-source helpers remain +`270*8*(120*64+64)=16727040`. Total helper counts are +`227312640 -> 123632640`. + +Each removed mixed-target helper removes 2 D entries, and each removed pure +target helper removes 8. Therefore removed D entries are +`14400*(7056*2+144*8)=219801600`, all of magnitude 1/16. +`D_nnz:480337920 -> 260536320`; the 3,363,840 entries of magnitude 5/16 +are retained. Crucially **G_nnz stays 227312640**: two reads feed one helper. +There is no halving of the G term or a free source-access operation. + +The pinned signed Horner tariff is 4 for ±1, 8 for ±1/16, 11 for ±5/16. +Each D entry occurs in prefix and scatter; each G entry in capture and +cleanup. Hence the complete component primitive allowance is + +`16*D_nnz + 6*D_5 + 8*G_nnz`. + +It falls from 9,524,090,880 to 6,007,265,280, saving 3,516,825,600. +This includes every changed capture, cleanup, prefix and scatter; helper +frame children are counted separately. Native coordinate passes, actual +address evaluation, tape movement and physical dispatch are not part of +this semantic scalar tariff. These are prescribed upper invoices, not +minimum gate counts or measured speedups. + +## 6. Conditional K and full-host deltas + +PR4027 at the exact head in CONTEXT.json supplies the unchanged asymmetric +K histogram and scalar bills. Conditionally reusing those inputs, the new +full local histogram is + +`{1:247265280,8:4336,9:32,15:123632640,16:59760,17:1600}`. + +Rank mass falls by `17M=1762560000` from 3,865,333,216 to 2,102,773,216. +The conditional combined scalar invoices are 6,250,865,392 forward and +6,250,867,840 dual. No ordinary or private K child is otherwise changed. + +The certificate also applies the unchanged fractional full-row convention +from the base pricing source: for L stages, `m=16L+1`, `q=floor(m/17)` +and `pad=m mod17`. Removing M helpers removes formal stock `ML/q`, and +mass/rank terms `(2ML,1)`, `(15ML,15)` and `(ML*pad/q,pad)` if pad>0. +Their mass sums to `mML/q`, so the formal coverage deficit is unchanged. +Stages 3,5,7 and all pad work are checked against the independently extracted +source function; repeated ranks are combined for comparison. This is a +conditional accounting identity, not a physical stock/reserve certificate. + +## 7. Range, coverage and open implementation obligations + +At the **forward logical capture cut**, `|e|<=E`, `|x_+|,|x_-|<=X` +give `|e+x_+ +sigma*x_-|<=E+2X`, previously E+X. Captures introduce no +new fractional denominator. One extra magnitude bit suffices relative to +that single old cut bound; this says nothing by itself about full-network +approximate-child precision, dual accumulation, or physical normalization. +Those must be propagated through every inherited child and adapter. + +The exhaustive domain is the fixed H6 geometry, all 16 mixed pairing classes +and its complete counts; seed 83 only selects a bounded all-column fixture. +There is no probabilistic search, parameter sweep or optimality claim. +Pure-source compression, native recipe regeneration, a complete materialized +tape, copied-total erasure, physical restoration/placement, actual reserve, +source-access complexity and the joint BIT/complex analytic admission remain +open. No new κ follows from a smaller unnormalized rank or scalar invoice. + +Credit: Dominik Scholz, DreamingOfClouds, the H6 compensation/compiler +contributors and Ross Richardson's PR4027. Prepared by Tekalign with +substantial OpenAI Codex assistance; Apache-2.0. Frozen sources are unchanged. diff --git a/research/h6-mixed-pair-capture/README.md b/research/h6-mixed-pair-capture/README.md new file mode 100644 index 0000000000..5306bf6e06 --- /dev/null +++ b/research/h6-mixed-pair-capture/README.md @@ -0,0 +1,108 @@ +# Signed mixed-pair capture in the H6 compensation factor + +The two sources `(u,v)` and `(u,-v)` share one actual H6 source frame. +Where their `C=I-K` columns are equal or opposite, one ordinary helper can +capture their sum or difference. This gives an exact `DG=C` factor with +**103,680,000 fewer helpers**, retaining both paid source reads. Full-rank +mixed buckets and all pure-source helpers remain unchanged. + +| Complete compensation invoice | Before | After | +| --- | ---: | ---: | +| Ordinary helpers | 227,312,640 | 123,632,640 | +| Nonzero scatter entries | 480,337,920 | 260,536,320 | +| Nonzero capture entries | 227,312,640 | 227,312,640 | +| Component primitive allowance | 9,524,090,880 | 6,007,265,280 | + +These are exact semantic counts and prescribed scalar upper allowances, +not measured wall-clock/tape costs. The helper reduction is 45.61%; the +compensation scalar allowance decreases 36.93%. Forward logical capture +range grows from `E+X` to `E+2X`. No complete physical precision, allocator, +restoration, all-size supplier or new multiplication exponent is claimed. + +The [proof](PROOF.md) specifies the complete factor, the rank-two exception, +same-representative frame legality, arbitrary-dirt forward/dual chronology, +counts and inherited limits. [CERTIFICATE.json](CERTIFICATE.json) records all +16 attainable mixed pairing classes, full reduced-geometry tables by digest, +complete invoices and an all-input-column seed 83 fixture. The entire +30,960-square matrix and multi-billion-event network are not materialized. + +## Independent evidence + +`verify.py` enumerates doubled E8 directly as an integer lattice and groups +pure fibers by pairing signatures. `independent.py` uses a separate pattern +enumeration and direct lattice cosets, never importing the primary geometry, +factor, invoice or lifecycle code. It extracts the coefficient, Horner tariff +and helper padding convention from authenticated frozen source ASTs. +The two implementations agree on all 120 roots, 1080 pure points, all 256 +cosets, 14,400 root/root, 129,600 root/pure and 1,166,400 pure/pure entries. +This is independent exact finite evidence, not a formal verification of the +full multiplication theorem or of the inherited native compiler. + +The complete-fiber fixture has 24 data ports and checks every 120 original +or 110 compressed source/target/helper entrance columns, forward and dual. +Its helpers decrease 72→62, scatter entries 216→160, and scalar allowance +4056→3160; capture entries stay 72. The 25 failure controls include matched +wrong capture/cleanup signs, full-rank compression, missing prefix/K/cleanup, +premature source-FULL frames, wrong coefficients, free source reads, typed +receipts and corrupted/removed source pins before execution. + +## Reproduce + +From the repository root with Python 3.12; no third-party dependencies: + +```sh +python3.12 -B scripts/research_package.py --package research/h6-mixed-pair-capture +``` + +Expected markers: `PASS_H6_MIXED_PAIR_CAPTURE`, +`PASS_INDEPENDENT_H6_PAIR_CAPTURE`, `PASS_H6_CAPTURE_CONTROLS` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. The command is read-only. Standalone scripts also +run from an exported package with its eight declared inputs, without Git. +Receipt generation requires removing the old receipt explicitly and running +`verify.py --write`; the generator refuses any existing destination. + +Exact canonical base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. +[SOURCES.json](SOURCES.json) pins every live input by Git blob and SHA256; +the verifier seals the inventory itself. The selected record and task +catalogue are historical provenance. [TASK.json](TASK.json) records OS seed 83, +domain, stopping rule and the refined independent-verification card. + +## Conditional asymmetric K comparison + +Ross Richardson's [PR4027](https://github.com/CrocSwap/integer-mult-bounds/pull/4027) +at `1bcc4f8261d2dc322c98fa9e44c4ced43cd1cd95` supplies the unchanged +asymmetric K histogram and scalar bills in [CONTEXT.json](CONTEXT.json). +Conditionally adding those bills gives 6,250,865,392 forward and 6,250,867,840 +dual component primitives, before real/imaginary doubling and native adapters. +The complete local rank mass becomes 2,102,773,216 +from 3,865,333,216. The certificate also gives formal removed row-stock, +rank mass and padding terms for stages 3,5,7 under the unchanged parent +row convention. Role counts and capture range change too, so these local +differences do not imply a joint moment or κ improvement. No pending K +implementation is imported or independently admitted by this package. + +## Open next questions + +Can one compress an eight-column pure-source fiber with an affordable capture +matrix? Those 16,727,040 helpers are unchanged; first factor one fiber exactly +and price dense capture, scatter and range before expanding the search. + +Can the reduced factor pass full approximate-child and physical admission? +First propagate error through the whole K splice, then bind source access, +restoration, bank placement and pads to actual reserve and the joint BIT +moment. The inherited copied-total/erasure and tape contracts remain blockers. +The structured questions and first steps are in [TASK.json](TASK.json). + +## Credit and license + +Dominik Scholz's [PR606](https://github.com/CrocSwap/integer-mult-bounds/pull/606) +supplies H6 geometry/factor; DreamingOfClouds supplies the H6 proposal. +The frozen [compensation network](../h6-compensation-network/README.md), +including PR1830's lineage, supplies the bucket, compiler and dirt contract. +Ross Richardson's PR4027 supplies the asymmetric K work and explicitly +identifies the remaining helper burden. Their native/compiler and upstream +attributions remain with the original sources, which are unchanged. + +Prepared by Tekalign (`tekuuu`), with substantial OpenAI Codex assistance in +the mathematics, implementations, proof, controls and packaging. Machine +checks are not human peer review. New work is Apache-2.0. diff --git a/research/h6-mixed-pair-capture/SOURCES.json b/research/h6-mixed-pair-capture/SOURCES.json new file mode 100644 index 0000000000..8c6466507d --- /dev/null +++ b/research/h6-mixed-pair-capture/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/h6-compensation-network/README.md", + "usage": "input", + "git_blob": "a7b5d4b0af813c09b485d5d906852a202f271466", + "sha256": "f7c74c4da5189762fcf837bb657d44fbd9f3b1dd3273bdc60c17bbcbc066f315" + }, + { + "path": "research/h6-compensation-network/construction/network.py", + "usage": "input", + "git_blob": "608bce2ddd49fbef1fb40aca566118eb791367f8", + "sha256": "e1bd9e43179835d16f9ec561ecd61585cf320a71550da49646f5d62da744b4f1" + }, + { + "path": "research/h6-compensation-network/contract/THEOREM.md", + "usage": "input", + "git_blob": "74832d898b6993b677a3c6fbfb30d03e509accaf", + "sha256": "9752a525d22d815341b70143a06221ad4b3aec0ae8a6447786d88d0291fef45f" + }, + { + "path": "research/h6-compensation-network/pricing/verify.py", + "usage": "input", + "git_blob": "f9434ab83e11a4e93d92fdf1b2a9d7f008b41232", + "sha256": "56f273853bd7089c3721bc023713993ac79e961d535694624cbb60dd7dcdd454" + }, + { + "path": "research/h6-compensation-network/routes/BUCKETED-SCHEMA.json", + "usage": "input", + "git_blob": "eaf913b998b01d0728e7fe4f52ee6f764cc74e9f", + "sha256": "376b0fe2128c12a1409792de7d0917da86f27e933b4d010c5a8322689b24ac8f" + }, + { + "path": "research/niemeier-lattices/code/e8_cubed.py", + "usage": "input", + "git_blob": "d4444d142fb370498bcd9a0abec45e2f5ea0b0c5", + "sha256": "ce24f397053c0ef5b26881bb7ccfab53fb0a3d762f2de04086fed8f7b41e8234" + }, + { + "path": "research/e8-complex-gauge-kernel/code/emit_gk.py", + "usage": "input", + "git_blob": "0dd1853bb58f55cccdeb92cee4566d1f5a4792e5", + "sha256": "4e415bff1d9f154496ed38e6889929b600aa0f3d583a375e8ca257ad8f51fa23" + }, + { + "path": "research/h6-compensation-network/physical_compiler/universal.py", + "usage": "input", + "git_blob": "42d877aa4ee8c1398fe3e2576a41afde43311881", + "sha256": "165555cf3d84b28a1a555120ec597ae55098ccdf56c7ecef01f54c12a37bdcfe" + } + ] +} diff --git a/research/h6-mixed-pair-capture/TASK.json b/research/h6-mixed-pair-capture/TASK.json new file mode 100644 index 0000000000..bd5938409c --- /dev/null +++ b/research/h6-mixed-pair-capture/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently reconstruct H6 mixed-source compensation columns, replace equal/opposite columns by one same-frame signed capture, and account for every changed helper and scalar entry.", + "scope_change_reason": "The card explicitly permits source-ledger reconstruction. Current PR4027 identifies the unchanged 227312640 compensation helpers as its dominant missing improvement; its exact U9 work is kept as a conditional interface, while this package checks a distinct DG=I-K factor.", + "bottleneck_link": "Mixed-source same-frame capture reduces the dominant ordinary-helper and scatter burden, preserving both source reads and the full arbitrary-dirt K chronology.", + "budget_minutes": 90, + "stop_rule": "Complete all E8 root/root, root/pure and pure/pure tables, all16 attainable mixed pairing classes, one seed83 complete-fiber all-input fixture in both orientations, independent direct-coset reconstruction and semantic failure controls. Do not extend to pure-source compression or infer kappa.", + "outcome": "completed", + "evidence": "CERTIFICATE.json; PROOF.md; verify.py; independent.py; controls.py. Exact domain counts, coverage and invoices are recorded in the certificate.", + "author": "Tekalign (tekuuu), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in deriving the factor, implementing both exact checks, proof writing, controls and packaging. Machine checks are not human peer review or a formal proof of the multiplication theorem.", + "open_questions": [ + { + "question": "Can the unchanged pure-source buckets also admit a lower-cost same-frame factor?", + "why_it_matters": "Pure-source helpers contribute16727040 roles and are untouched here.", + "first_step": "Factor one complete eight-column pure-source fiber over exact rationals, requiring every source to share its actual native representative and pricing dense capture as well as scatter.", + "blocked_by": "A new scoped claim and complete range/scalar/child accounting; this package makes no assertion about pure-source optimality." + }, + { + "question": "Can the reduced helper factor be admitted as a complete approximate recursive physical supplier?", + "why_it_matters": "Exact scalar savings alone do not establish a faster implementation or improve kappa.", + "first_step": "Propagate approximate-child error and the signed two-source capture range through the complete K splice, then bind helper bank layout, source access, pads and restoration to the outer joint moment.", + "blocked_by": "Inherited copied-total erasure, actual physical reserve, full precision, tape routing and joint BIT admission contracts remain unresolved." + } + ], + "assignment_seed": 83, + "assignment_seed_source": "Operating-system randomness; recorded2026-10-19T10:27:29.150446+00:00 before object selection." +} diff --git a/research/h6-mixed-pair-capture/VERIFICATION.md b/research/h6-mixed-pair-capture/VERIFICATION.md new file mode 100644 index 0000000000..04ea1c3dde --- /dev/null +++ b/research/h6-mixed-pair-capture/VERIFICATION.md @@ -0,0 +1,46 @@ +# Verification handoff + +Scientific freeze: `569d719d954367b7f941ec8f23321b3c3a8f62ca`. +Canonical base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. +Python 3.12.14, Linux, standard library only; checked 2026-10-19. +Later packaging commits edit prose/context only; mathematical code, receipt, +source inventory and registered commands are unchanged from this freeze. + +The registered replay passes all three commands: + +```sh +python3.12 -B scripts/research_package.py --package research/h6-mixed-pair-capture +``` + +Expected final marker: +`PASS_REGISTERED_RESEARCH_PACKAGE research/h6-mixed-pair-capture outcome=completed`. + +* Primary: complete recursive E8 shells and pairing tables; all 16 mixed + factors; complete helper, capture, scatter, scalar and formal pad invoices; + original/compressed forward/dual all-input-column lifecycle fixtures. +* Independent: separate pattern shells and direct lattice cosets; exact frozen + coefficient, tariff and host-term oracles; all counts and 16 minor ranks. +* Controls: 25 expected rejections, including matched capture/cleanup sign + errors that restore helper dirt but corrupt data, full-rank compression, + arbitrary-dirt omissions, different actual source frames, weakened source + inventory before execution, typed receipt mutations and overwrite refusal. + +The official exporter produced and checked a 23-file scientific bundle. +All three scripts then passed with `-I -O -B` in its Git-free copy, with +read-only file/directory modes, PATH pointing to a nonexistent directory, +and a failing `json.py` shadow trap in the working directory. All 25 files +(23 exported files, the export receipt and shadow trap) were byte-for-byte +unchanged afterward. This checks portable replay; it is not a formal kernel. + +The published package adds this handoff and prose/context corrections. It +does not include local exploratory scripts, downloaded parent trees or +multi-billion-event generated tapes. Frozen predecessors are unchanged. + +Remaining obligations: inherited native recipe correctness and complete +arbitrary-input K admission; copied-total erasure; literal physical helper +restoration; approximate-child composite precision; placement, source/tape +access and actual physical reserve; joint BIT/complex analytic admission. +The conditional asymmetric K totals are a comparison pinned to PR4027, +not an independent certification of that pending implementation. + +Prepared by Tekalign with substantial OpenAI Codex assistance; Apache-2.0. diff --git a/research/h6-mixed-pair-capture/VERIFY.json b/research/h6-mixed-pair-capture/VERIFY.json new file mode 100644 index 0000000000..96ec8caecf --- /dev/null +++ b/research/h6-mixed-pair-capture/VERIFY.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/h6-compensation-network/README.md", + "research/h6-compensation-network/construction/network.py", + "research/h6-compensation-network/contract/THEOREM.md", + "research/h6-compensation-network/pricing/verify.py", + "research/h6-compensation-network/routes/BUCKETED-SCHEMA.json", + "research/niemeier-lattices/code/e8_cubed.py", + "research/e8-complex-gauge-kernel/code/emit_gk.py", + "research/h6-compensation-network/physical_compiler/universal.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact recursive E8 geometry, all16 factors, complete invoices and forward/dual all-input-column dirty lifecycle fixture; strict typed receipt comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate pattern enumeration and direct E8 cosets, frozen-source coefficient/tariff/helper-term oracles, complete pair counts and determinant ranks; no primary geometry, factor, invoice or word imports." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/controls.py" + ], + "timeout_seconds": 120, + "checks": "25 expected failures covering matched wrong signs, full-rank compression, missing prefix/K/cleanup, source frame chronology and representatives, DG entries, source reads, typed receipts, sealed live inputs and overwrite refusal." + } + ] +} diff --git a/research/h6-mixed-pair-capture/census.py b/research/h6-mixed-pair-capture/census.py new file mode 100644 index 0000000000..67e279097f --- /dev/null +++ b/research/h6-mixed-pair-capture/census.py @@ -0,0 +1,89 @@ +"""Complete reduced-geometry census, not a 30960-square matrix replay.""" +from collections import Counter +from hashlib import sha256 +import json +from fractions import Fraction as F +from e8_exact import dot,need +from pair_factor import mixed_block,rank,factor_columns,product,invoice + + +def digest(data): + return sha256(json.dumps(data,separators=(',',':')).encode()).hexdigest() + + +def compute(roots,pure,root_sig,buckets): + root_rows=[];root_pairings=Counter() + for u in roots: + row=[dot(u,v)//4 for v in roots] + need(all(dot(u,v)%4==0 for v in roots),'integral complete root table') + c=Counter(abs(v) for v in row) + need(c=={0:63,1:56,2:1},'every root association degree') + root_rows.append(row);root_pairings.update(row) + pure_compat=[] + for u in roots: + number=0 + for members in buckets.values(): + values=[dot(u,pure[i])//4 for i in members] + need(all(dot(u,pure[i])%4==0 for i in members),'integral complete root/pure table') + need(len({v%2 for v in values})==1,'whole pure fiber has one compatibility parity') + if values[0]%2: + need(all(abs(v)==1 for v in values),'compatible pure targets have only unit pairing') + number+=1 + need(number==72,'every root has72 compatible pure-label buckets') + pure_compat.append(number) + pure_rows=[];pure_label_degrees=[];pure_root_degrees=[] + representatives=[pure[m[0]] for m in buckets.values()] + for v in pure: + row=Counter(abs(dot(v,w)//4) for w in pure) + need(all(dot(v,w)%4==0 for w in pure),'integral complete pure table') + need(row[1]==448 and row[3]==64 and row[4]==1,'every pure source has512 edges,64 of magnitude5/16') + pure_rows.append(dict(sorted(row.items()))) + degree=sum((dot(v,w)//4)&1 for w in representatives) + need(degree==64,'pure target-label degree') + root_degree=sum((dot(v,w)//4)&1 for w in roots) + need(root_degree==64,'pure-to-root label degree') + pure_label_degrees.append(degree);pure_root_degrees.append(root_degree) + classes=[] + for A in (-1,0,1,2): + for B in (-1,0,1,2): + matrix=mixed_block(A,B) + r=rank(matrix) + sigma=(1 if B==0 and A%2 else -1 if A==0 and B%2 else None) + if not r:need((A+B)%2==0,'zero mixed block is incompatible') + elif sigma is not None:need(r==1,'signed capture has rank1') + else: + need(r==2 and (A==2 or B==2) and (A+B)%2==1,'full-rank mixed exception') + need(abs(matrix[0][0]*matrix[1][1]-matrix[0][1]*matrix[1][0])==F(3,32),'full-rank exception determinant') + G,D=factor_columns(matrix,sigma) + need(product(D,G)==matrix,'every attainable two-by-two factor identity') + classes.append({'A':A,'B':B,'rank':r,'sigma':sigma,'C':[[str(c) for c in row] for row in matrix]}) + # Counts are products of the fully verified association degrees above. + mixed_caps=2*64*56 + pure_caps=2*72 + R_mixed=120**2*2*(mixed_caps+pure_caps) + R_pure=2*135*8*(120*64+64) + E_mm=120**2*mixed_caps*4 + E_mp=120**2*pure_caps*16 + E_pp=2*1080*(448+64) + E5_mm=120**2*(2*56)*2 + E5_pp=2*1080*64 + need(R_mixed+R_pure==227312640,'independently reconstructed baseline helper count') + need(E_mm+2*E_mp+E_pp==480337920 and E5_mm+E5_pp==3363840,'independently reconstructed complete coefficient census') + bill=invoice() + need(bill['capture_entries_old_and_new']==R_mixed+R_pure,'new capture entries are not helper count') + return {'root_lines':120,'pure_lines_per_block':1080,'pure_labels_per_block':135,'pure_label_multiplicity':8, + 'full_E8_cosets':256,'H6_ports':30960,'mixed_labels':14400,'all_labels':14670, + 'root_pair_table_entries':120**2,'root_pure_table_entries':120*1080,'pure_pair_table_entries':1080**2, + 'root_points_sha256':digest(roots),'pure_points_sha256':digest(pure), + 'root_pair_table_sha256':digest(root_rows),'pure_pair_count_rows_sha256':digest(pure_rows), + 'root_signature_sha256':digest(root_sig),'pure_fibers_sha256':digest(list(buckets.values())), + 'pure_fiber_partition_sha256':digest(sorted(sorted(v) for v in buckets.values())), + 'mixed_cap_degree':mixed_caps,'pure_cap_degree_from_mixed':pure_caps, + 'rank1_mixed_caps_per_mixed_source_label':2*63*56, + 'rank2_mixed_caps_per_mixed_source_label':2*56, + 'new_helpers_per_mixed_source_label':2*63*56+2*2*56+2*72, + 'mixed_block_classes':classes, + 'baseline_helper_parts':{'mixed_source':R_mixed,'pure_source':R_pure}, + 'baseline_scatter_parts':{'mixed_mixed':E_mm,'mixed_pure_each_orientation':E_mp,'pure_pure':E_pp}, + 'baseline_abs5_over16_parts':{'mixed_mixed':E5_mm,'pure_pure':E5_pp}, + 'invoice':bill} diff --git a/research/h6-mixed-pair-capture/controls.py b/research/h6-mixed-pair-capture/controls.py new file mode 100644 index 0000000000..555c1dac48 --- /dev/null +++ b/research/h6-mixed-pair-capture/controls.py @@ -0,0 +1,102 @@ +#!/usr/bin/env python3 +"""Semantic factor, chronology, invoice and input-integrity failure controls.""" +from copy import deepcopy +from fractions import Fraction as F +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +import h6_inputs +from h6_inputs import need +from e8_exact import geometry +from pair_factor import factor_columns,mixed_block,product +from word import fixture,replay,factor_check,captures +from verify import read,validate + + +def check(): + passed=[] + def rejected(name,fn,message): + try:fn() + except ValueError as error: + need(message in str(error),'wrong rejection for '+name+': '+str(error)) + passed.append(name) + else:raise ValueError('accepted negative control '+name) + geo=geometry();_,(indices,old,new)=fixture(geo) + for dual in (False,True): + suffix='dual' if dual else 'forward' + rejected('matched-wrong-sign-'+suffix, + lambda:replay(new,indices,geo,dual,wrong_sigma=True),'all data and helper-dirt columns') + for phase in ('dirt_prefix','cleanup','K'): + rejected('omit-'+phase+'-'+suffix, + lambda:replay(new,indices,geo,dual,omit=phase), + 'helper entrance returned' if (dual and phase=='dirt_prefix') or (not dual and phase=='cleanup') + else 'all data and helper-dirt columns') + rejected('premature-source-FULL-'+suffix, + lambda:replay(new,indices,geo,dual,early_full=True),'complete K receives actual source lines') + full=mixed_block(2,1) + rejected('compress-full-rank-bucket',lambda:factor_columns(full,1),'exact signed column relation') + false_D=[[r[0]] for r in full];false_G=[[F(1),F(1)]] + need(product(false_D,false_G)!=full,'independent full-rank DG counterexample') + for name,mutate in ( + ('missing-D-entry',lambda row:row['D'].pop(next(iter(row['D'])))), + ('wrong-D-coefficient',lambda row:row['D'].__setitem__(next(iter(row['D'])),F(7,16))), + ): + rows=deepcopy(new);mutate(rows[0]) + rejected(name,lambda:factor_check(rows,indices,indices,geo),'complete DG=C') + mixed=next(p for p in indices if p>=2160) + bad=[p for p in indices if p!=mixed] + rejected('incomplete-mixed-source-fiber',lambda:list(captures(bad,indices,geo)),'complete actual mixed source pair') + rows=deepcopy(new);row=next(r for r in rows if len(r['G'])==2) + source=next(iter(row['G']));weight=row['G'].pop(source) + # A pure source has a different actual label from every mixed source. + row['G'][next(p for p in indices if p<2160)]=weight + rejected('different-actual-source-frame',lambda:replay(rows,indices,geo),'actual same-frame operands at capture') + receipt=read(HERE/'CERTIFICATE.json') + for name,path,value in ( + ('false-deleted-source-read',('invoice','capture_entries_old_and_new'),123632640), + ('wrong-helper-count',('invoice','new_helpers'),123632639), + ('boolean-integer-receipt',('full_E8_cosets',),True), + ('float-integer-receipt',('root_lines',),120.0), + ('unaccounted-capture-range',('invoice','capture_range_new'),'E+X'), + ): + bad=deepcopy(receipt);cursor=bad + for key in path[:-1]:cursor=cursor[key] + cursor[path[-1]]=value + rejected(name,lambda:validate(receipt,bad),'complete typed H6 capture certificate') + bad=deepcopy(receipt);bad.pop('fixture') + rejected('missing-whole-fixture',lambda:validate(receipt,bad),'complete typed H6 capture certificate') + with tempfile.TemporaryDirectory(prefix='h6-capture-controls-') as temp: + root=Path(temp);package=root/'research/h6-mixed-pair-capture';package.mkdir(parents=True) + inventory=(HERE/'SOURCES.json').read_bytes();(package/'SOURCES.json').write_bytes(inventory) + for row in json.loads(inventory)['files']: + if row['usage']!='input':continue + target=root/row['path'];target.parent.mkdir(parents=True,exist_ok=True) + shutil.copyfile(h6_inputs.ROOT/row['path'],target) + saved_here,saved_root=h6_inputs.HERE,h6_inputs.ROOT + try: + h6_inputs.HERE,h6_inputs.ROOT=package,root + h6_inputs.authenticate() + target=root/'research/e8-complex-gauge-kernel/code/emit_gk.py' + target.write_text("def primitive_bound(op):\n raise RuntimeError('UNAUTHENTICATED_EXECUTION')\n") + rejected('source-corruption-before-execution',h6_inputs.oracles,'source SHA256') + manifest=json.loads(inventory) + manifest['files']=[r for r in manifest['files'] if r['path']!='research/e8-complex-gauge-kernel/code/emit_gk.py'] + (package/'SOURCES.json').write_text(json.dumps(manifest)) + rejected('manifest-removal-before-execution',h6_inputs.oracles,'sealed source inventory') + finally:h6_inputs.HERE,h6_inputs.ROOT=saved_here,saved_root + duplicate=root/'duplicate.json';duplicate.write_text('{"root_lines":120,"root_lines":121}') + rejected('duplicate-receipt-key',lambda:read(duplicate),'unique certificate keys') + before=(HERE/'CERTIFICATE.json').read_bytes() + proc=subprocess.run([sys.executable,'-I','-B',str(HERE/'verify.py'),'--write'],capture_output=True,text=True,timeout=10) + need(proc.returncode!=0 and 'refuse certificate overwrite' in proc.stderr,'write refusal before recomputation') + need((HERE/'CERTIFICATE.json').read_bytes()==before,'write refusal preserves receipt') + passed.append('CLI-overwrite-refusal') + print('PASS_H6_CAPTURE_CONTROLS '+json.dumps({'count':len(passed),'rejected':passed},sort_keys=True)) + + +if __name__=='__main__':check() diff --git a/research/h6-mixed-pair-capture/e8_exact.py b/research/h6-mixed-pair-capture/e8_exact.py new file mode 100644 index 0000000000..37c68367d5 --- /dev/null +++ b/research/h6-mixed-pair-capture/e8_exact.py @@ -0,0 +1,72 @@ +"""Independent recursive enumeration of doubled E8, exact integers only.""" +from collections import defaultdict +from math import isqrt + + +def need(ok,message): + if not ok:raise ValueError(message) + + +def dot(a,b): + return sum(x*y for x,y in zip(a,b)) + + +def shell(norm): + result=[] + def visit(prefix,left,parity): + if len(prefix)==8: + if left==0 and sum(prefix)%4==0 and next((v for v in prefix if v),0)>0: + result.append(tuple(prefix)) + return + for v in range(-isqrt(left),isqrt(left)+1): + if v%2==parity:visit(prefix+(v,),left-v*v,parity) + for parity in (0,1):visit((),norm,parity) + answer=sorted(result) + need(len(answer)==len(set(answer)),'unique recursive lattice shell') + return answer + + +def signature(vector,roots): + result=0 + for i,r in enumerate(roots): + p=dot(vector,r) + need(p%4==0,'integral E8 lattice pairing') + result|=((p//4)&1)<0 and all(len(row)==2 for row in matrix),'complete two-column bucket') + if not any(any(row) for row in matrix):return [],[[] for _ in matrix] + if sigma is not None: + need(sigma in (-1,1) and all(row[1]==sigma*row[0] for row in matrix),'exact signed column relation') + return [[F(1),F(sigma)]],[[row[0]] for row in matrix] + return [[F(1),F(0)],[F(0),F(1)]],[list(row) for row in matrix] + + +def product(D,G): + return [[sum((D[i][k]*G[k][j] for k in range(len(G))),F(0)) for j in range(2)] for i in range(len(D))] + + +def primitive(value): + q=F(value) + if not q:return 0 + a=abs(q.numerator) + return 3+(a.bit_length()-1)+a.bit_count()+(q.denominator.bit_length()-1) + + +def invoice(): + old_R=14400*2*7312+270*8*7744 + removed=14400*(2*63*56+2*72) + new_R=old_R-removed + D_removed=14400*(2*63*56*2+2*72*8) + old_D=480337920;new_D=old_D-D_removed;D5=3363840 + G_entries=old_R # Two captures into one bank: no deleted source read. + old_scalar=16*old_D+6*D5+8*G_entries + new_scalar=16*new_D+6*D5+8*G_entries + histogram={1:2*new_R,8:4336,9:32,15:new_R,16:59760,17:1600} + need(old_R==227312640 and new_R==123632640,'exact helper invoice') + need(old_scalar-new_scalar==2*primitive(F(1,16))*D_removed,'complete changed scalar invoice') + hosted=[] + for stages in (3,5,7): + m=16*stages+1;q,pad=divmod(m,17) + stock=F(stages*removed,q) + terms=[(F(2*stages*removed),1),(F(15*stages*removed),15)] + if pad:terms.append((F(stages*removed*pad,q),pad)) + mass=sum(v for v,r in terms) + need(mass==m*stock,'removed complete helper mass equals m times formal stock') + hosted.append({'stages':stages,'m':m,'replication_q':q,'pad':pad, + 'formal_stock_removed':str(stock),'rank_mass_removed':str(mass), + 'mass_rank_terms_removed':[[str(v),r] for v,r in terms], + 'coverage_deficit_change':'0', + 'scope':'Existing fractional row-stock/padding convention only; not a physical reserve proof.'}) + return {'old_helpers':old_R,'new_helpers':new_R,'helpers_removed':removed, + 'old_scatter_entries':old_D,'new_scatter_entries':new_D,'scatter_entries_removed':D_removed, + 'capture_entries_old_and_new':G_entries,'abs5_over16_entries_old_and_new':D5, + 'old_compensation_component_primitives':old_scalar,'new_compensation_component_primitives':new_scalar, + 'component_primitive_saving':old_scalar-new_scalar, + 'new_asymmetric_combined_forward':new_scalar+243600112, + 'new_asymmetric_combined_dual':new_scalar+243602560, + 'new_full_local_histogram':{str(k):v for k,v in histogram.items()}, + 'old_full_local_rank_mass':3865333216, + 'new_full_local_rank_mass':sum(k*v for k,v in histogram.items()), + 'helper_path':[1,15,1],'positive_rank_helper_transitions_removed':3*removed, + 'conditional_hosted_helper_deltas':hosted,'new_fractional_denominator':False, + 'capture_range_old':'E+X','capture_range_new':'E+2X', + 'capture_range_scope':'Forward logical mixed-source capture cut only; full and dual precision remain open.', + 'physical_precision_allocator_tape_stock_joint_kappa':'unresolved, not inferred from semantic invoices'} diff --git a/research/h6-mixed-pair-capture/verify.py b/research/h6-mixed-pair-capture/verify.py new file mode 100644 index 0000000000..85a8a219bb --- /dev/null +++ b/research/h6-mixed-pair-capture/verify.py @@ -0,0 +1,59 @@ +#!/usr/bin/env python3 +"""Exact reduced-geometry/capture factor and arbitrary-dirt lifecycle replay.""" +import argparse +from hashlib import sha256 +import json +from pathlib import Path +import sys +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +from h6_inputs import authenticate,need,ROOT +from e8_exact import geometry +from census import compute +from word import fixture + + +def canonical(value): + return json.dumps(value,sort_keys=True,separators=(',',':'),allow_nan=False).encode() + + +def read(path): + def unique(rows): + result={} + for k,v in rows: + need(k not in result,'unique certificate keys');result[k]=v + return result + return json.loads(path.read_text(),object_pairs_hook=unique) + + +def result(): + pins=authenticate() + geo=geometry();data=compute(*geo) + schema=read(ROOT/'research/h6-compensation-network/routes/BUCKETED-SCHEMA.json') + need(schema['helper_count']==data['invoice']['old_helpers'] and + schema['actual_nonzero_source_target_entries']==data['invoice']['old_scatter_entries'], + 'actual source bucket baseline binding') + data['source_pins']=pins + data['fixture']=fixture(geo)[0] + data['base_commit']='20ecf2891d80b5acf18d980b2164fb44ea7faa90' + data['status']='PASS_H6_MIXED_PAIR_CAPTURE' + return data + + +def validate(actual,expected): + need(canonical(actual)==canonical(expected),'complete typed H6 capture certificate') + + +def main(): + parser=argparse.ArgumentParser(description=__doc__);parser.add_argument('--write',action='store_true');args=parser.parse_args() + target=HERE/'CERTIFICATE.json' + if args.write:need(not target.exists(),'refuse certificate overwrite') + data=result() + if args.write: + need(not target.exists(),'refuse certificate overwrite') + with target.open('x') as stream:stream.write(json.dumps(data,indent=2,sort_keys=True)+'\n') + else:validate(data,read(target)) + print('PASS_H6_MIXED_PAIR_CAPTURE helpers=227312640->123632640 capture_entries_unchanged=227312640') + + +if __name__=='__main__':main() diff --git a/research/h6-mixed-pair-capture/word.py b/research/h6-mixed-pair-capture/word.py new file mode 100644 index 0000000000..0730f742c9 --- /dev/null +++ b/research/h6-mixed-pair-capture/word.py @@ -0,0 +1,162 @@ +"""Lazy bucket factors and a complete sparse all-input-column lifecycle replay. + +The supplied K macro is an explicit inherited contract, not a free native gate. +""" +from fractions import Fraction as F +from collections import defaultdict +import random +from e8_exact import vector,label,dot,need,mixed_port +from pair_factor import coefficient,factor_columns,primitive,product + + +def add_row(dst,src,c): + for k,v in src.items(): + dst[k]=dst.get(k,F(0))+c*v + if not dst[k]:del dst[k] + + +def group_ports(indices,geo): + roots,pure,sig,buckets=geo + result=defaultdict(list) + for p in sorted(indices):result[label(p,roots,pure,sig,buckets)].append(p) + return dict(sorted(result.items())) + + +def captures(source_indices,target_indices,geo,compressed=True): + """Compile-time fixed H6 indices only; full outputs may be iterated lazily.""" + roots,pure,sig,buckets=geo + source_groups=group_ports(source_indices,geo);targets=group_ports(target_indices,geo) + for cap,ts in targets.items(): + for line,ss in source_groups.items(): + if line[0] and line[1]: + need(len(ss)==2 and ss[0]>=2160 and ss[1]==ss[0]+1 and (ss[0]-2160)%2==0, + 'complete actual mixed source pair') + C=[[coefficient(vector(t,roots,pure),vector(s,roots,pure),t==s) for s in ss] for t in ts] + sigma=None + if compressed: + if all(r[1]==r[0] for r in C):sigma=1 + elif all(r[1]==-r[0] for r in C):sigma=-1 + G,D=factor_columns(C,sigma) + need(product(D,G)==C,'compiled local factor identity') + for j,weights in enumerate(G): + yield {'line':line,'cap':cap,'source_pair':list(ss), + 'G':{s:v for s,v in zip(ss,weights) if v}, + 'D':{t:D[i][j] for i,t in enumerate(ts) if D[i][j]}} + else: + for s in ss: + D={t:coefficient(vector(t,roots,pure),vector(s,roots,pure),t==s) for t in ts} + D={t:v for t,v in D.items() if v} + if D:yield {'line':line,'cap':cap,'source_pair':[s], 'G':{s:F(1)},'D':D} + + +def factor_check(records,sources,targets,geo): + roots,pure,_,_=geo + found={(t,s):F(0) for t in targets for s in sources} + for row in records: + for t,d in row['D'].items(): + for s,g in row['G'].items():found[t,s]+=d*g + need(all(found[t,s]==coefficient(vector(t,roots,pure),vector(s,roots,pure),t==s) + for t in targets for s in sources),'complete DG=C factor on every fixture entry') + + +def replay(records,indices,geo,dual=False,omit=None,wrong_sigma=False,early_full=False): + roots,pure,_,_=geo + groups=group_ports(indices,geo) + representative={g:vector(m[0],roots,pure) for g,m in groups.items()} + labels={p:g for g,m in groups.items() for p in m} + x={p:{('x',p):F(1)} for p in indices};y={p:{('y',p):F(1)} for p in indices} + h=[{('e',j):F(1)} for j in range(len(records))] + xf={p:('line',labels[p]) for p in indices};yf={p:('zero',) for p in indices} + hf=[('zero',) for _ in records];paths=[[] for _ in records] + def plus(dst,src,c,df,sf,phase): + need(df==sf,'actual same-frame operands at '+phase) + if phase==omit:return + if dual:add_row(src,dst,-c) + else:add_row(dst,src,c) + def climb(j,kind,target,increment): + if kind=='line':need(hf[j]==('zero',),'helper starts at ZERO') + if kind=='cap': + need(hf[j]==('line',records[j]['line']),'captured helper source line') + a,b=representative[records[j]['line']],representative[target] + need(dot(a,b)%4==0 and (dot(a,b)//4)%2==1,'source line lies in bucket cap') + if kind=='full':need(hf[j]==('cap',records[j]['cap']),'helper reaches its cap before FULL') + hf[j]=(kind,target) if kind!='full' else ('full',);paths[j].append(increment) + for j,row in enumerate(records): + for t,d in row['D'].items():plus(y[t],h[j],-d,yf[t],hf[j],'dirt_prefix') + for j,row in enumerate(records): + climb(j,'line',row['line'],1) + for at,(s,g) in enumerate(row['G'].items()): + if wrong_sigma and g==-1:g=1 + plus(h[j],x[s],g,hf[j],xf[s],'capture') + if early_full: + xf={p:('full',) for p in indices} + # Exact full K contract from4027/legacy theorem: it accepts arbitrary + # current source/target values, advances its own sources and targets, + # restores its unrelated auxiliary dirt, and has its own separately paid bill. + need(all(xf[p]==('line',labels[p]) and yf[p]==('zero',) for p in indices), + 'complete K receives actual source lines and ZERO targets') + if omit!='K': + if dual: + for s in indices: + for t in indices: + k=F(int(s==t))-coefficient(vector(t,roots,pure),vector(s,roots,pure),s==t) + if k:add_row(x[s],y[t],-k) + else: + for t in indices: + for s in indices: + k=F(int(s==t))-coefficient(vector(t,roots,pure),vector(s,roots,pure),s==t) + if k:add_row(y[t],x[s],k) + xf={p:('full',) for p in indices};yf={p:('cap',labels[p]) for p in indices} + for j,row in enumerate(records): + climb(j,'cap',row['cap'],15) + for t,d in row['D'].items():plus(y[t],h[j],d,yf[t],hf[j],'scatter') + for j,row in enumerate(records): + climb(j,'full',None,1) + for s,g in row['G'].items(): + if wrong_sigma and g==-1:g=1 + plus(h[j],x[s],-g,hf[j],xf[s],'cleanup') + # Check dirt first: a matched wrong capture/cleanup sign can restore every + # helper and nevertheless compute the wrong data map. + need(all(row=={('e',j):F(1)} for j,row in enumerate(h)),'every arbitrary logical helper entrance returned') + need(all(f==('full',) and p==[1,15,1] for f,p in zip(hf,paths)),'complete helper frame paths') + for p in indices: + X={('x',p):F(1)};Y={('y',p):F(1)} + if dual:X[('y',p)]=F(-1) + else:Y[('x',p)]=F(1) + need(x[p]==X and y[p]==Y,'all data and helper-dirt columns at complete endpoint') + return {'dual':dual,'data_ports':len(indices),'helper_roles':len(records), + 'all_input_columns':2*len(indices)+len(records),'helper_path':[1,15,1], + 'logical_dirt_return':True,'physical_helper_endpoint':'FULL applied to its original dirt, not literal physical entrance'} + + +def choose_fixture(geo,seed=83): + roots,pure,sig,buckets=geo + rng=random.Random(seed);i,j=rng.randrange(120),rng.randrange(120) + odd=lambda v:[k for k,r in enumerate(roots) if (dot(v,r)//4)%2] + zero=lambda v:[k for k,r in enumerate(roots) if dot(v,r)==0] + a=rng.choice(odd(roots[i]));b=rng.choice(zero(roots[j])) + c=rng.choice(zero(roots[i]));d=rng.choice(odd(roots[j])) + pair_indices={(i,j),(a,b),(c,d),(i,d)} # plus, minus, full-rank cases + selected=[] + for x,y in sorted(pair_indices):selected.extend((mixed_port(x,y),mixed_port(x,y,True))) + for block,root in ((0,roots[i]),(1,roots[j])): + groups=[g for g,m in buckets.items() if (dot(root,pure[m[0]])//4)%2] + chosen=rng.choice(groups) + selected.extend(p+1080*block for p in buckets[chosen]) + return sorted(set(selected)),{'seed':seed,'source_pair':[i,j],'mixed_label_pairs':sorted(map(list,pair_indices))} + + +def fixture(geo): + indices,domain=choose_fixture(geo) + old=list(captures(indices,indices,geo,False));new=list(captures(indices,indices,geo,True)) + factor_check(old,indices,indices,geo);factor_check(new,indices,indices,geo) + def counts(rows): + return {'helpers':len(rows),'capture_entries':sum(len(r['G']) for r in rows), + 'scatter_entries':sum(len(r['D']) for r in rows), + 'component_primitives':2*sum(primitive(v) for r in rows for v in r['G'].values())+ + 2*sum(primitive(v) for r in rows for v in r['D'].values())} + need(counts(old)['capture_entries']==counts(new)['capture_entries'],'sharing retains both charged source reads') + need(len(new)