Contract seven separated staged544 A2 blocks

research/staged544-separated-a2/.gitattributes

@@ -0,0 +1,2 @@
+source/** -text whitespace=blank-at-eol,blank-at-eof,space-before-tab,cr-at-eol
+inputs/** -text

research/staged544-separated-a2/.gitignore

@@ -0,0 +1,2 @@
+__pycache__/
+*.pyc

research/staged544-separated-a2/LEDGER.json

@@ -0,0 +1,36 @@
+{
+  "scope": "two exact PR3734 words; seven separated inverse-A2 blocks plus credited PR3998 consecutive A1858 block",
+  "proved_or_exactly_recomputed": {
+    "local_maps": "Exact rational3x3 identities on arbitrary dirty values, proved compositionally under strictdisjointsupport; no nativeeventcrossing.",
+    "scalar_delta_vs_PR3998": {
+      "forward_ADDs": -7,
+      "cleanup_ADDs": -5
+    },
+    "scalar_delta_vs_PR3734": {
+      "forward_ADDs": -8,
+      "cleanup_ADDs": -6
+    },
+    "paid_profile": {
+      "1": 2440,
+      "2": 725,
+      "3": 224,
+      "4": 102,
+      "5": 20,
+      "8": 8
+    },
+    "rank_mass": 5134,
+    "children": 3519,
+    "native_descriptors": "All72nativewarps/operatorrecords perprovider retained in order; onlyBpositionsremapped for deleted gates withinfixedcuts.",
+    "allocation": "No new register/helper/buffer. Helperwidthinventory unchanged.",
+    "unchanged_fields": "All top-level fields except A,B,restore,warps positions and derivedcleanup mustcompareequal."
+  },
+  "unknown_or_inherited": {
+    "physical_implementation": "Native scalar realization and owner/holding/routing/control/tape costs not newly admitted.",
+    "precision": "Changed intermediate coefficientgrowth/signed-floor/error ledger is not certified by scalar algebra alone.",
+    "native_phases": "No fresh concrete Clifford/Gaussian globalphase or inverse-lowering replay; unchangedoperators are freeformal symbols in wholeword replay.",
+    "later_words": "No applicability toPR3945or later words is claimed.",
+    "full_supplier": "Uniformwidths, stock, allsizecompiler, outer/analytic/BIT and fullmultiplicationtheorem remain inherited/unproved here.",
+    "performance": "No measuredruntimeor practicalspeedup claim."
+  },
+  "decision": "Retain focused scalar simplification and exact unchangedrecursiveprofile. Stop dependent graph/native expansion; this does not improve recursive moment or kappa."
+}

research/staged544-separated-a2/PROOF.md

@@ -0,0 +1,196 @@
+# Fixed separated A2 contractions and their complete unchanged frame bill
+
+ToikY, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Statement and frozen domain
+
+This certificate supplies seven fixed nonconsecutive scalar contractions on
+each of the two PR3734 providers retained by PR3998. It also reproduces, and
+credits to PR3998, the existing consecutive contraction at A1858. Its input
+providers are PR3734 `fa041037a3374eaa08feeca0b26a5d6893194147`, exported
+byte-exactly by PR3998 `389268a6b5e0373a3125d5c6fcd6995f4ea324f5`.
+The package is based on canonical main
+`20ecf2891d80b5acf18d980b2164fb44ea7faa90`; none of these attribution pins
+asserts ancestry of a pending contribution. `SOURCES.json` binds the complete
+local source closure. The retained PR3945 notice supplies lineage, not
+applicability to the later PR3945 words.
+
+On arbitrary rational live inputs and dirty buffers, the changed word has the
+same full operator as its source. It uses the same registers, native maps,
+wrappers, target cut, initial corrections and helper entrance/exit frames. Its
+complete paid profile is unchanged. Relative to PR3998's one-site contraction,
+it removes seven forward scalar ADD records and five inverse-cleanup ADD
+records. This is a fixed constructive simplification, with no recursive-moment
+or kappa improvement. It is not an exhaustive separated-motif search, a graph
+normal-form theorem, a runtime result or fresh native/supplier admission.
+
+Original zero-based sites are:
+
+| Section | Selected indices | Removed central position | Credit |
+|---|---|---|---|
+| A | 1858,1859,1860 | last | PR3998 |
+| B | 4,53,54 | first | new fixed witness |
+| B | 7,49,50 | first | new fixed witness |
+| restore | 20,21,36 | last | new fixed witness |
+| restore | 22,23,38 | last | new fixed witness |
+| restore | 26,27,51 | last | new fixed witness |
+| restore | 30,31,62 | last | new fixed witness |
+| restore | 32,33,73 | last | new fixed witness |
+
+`data.json` retains every original gate, replacement, support and canonical
+word/cleanup digest. The seven new replacements retain the exact original
+ordered frame lists. For the credited old A1858 replacement only, the
+publication's basis order `[42,82]` is reproduced instead of the raw source's
+`[82,42]`; these span the same subspace. The old site's two canonical edited
+word hashes are checked against PR3998's publication before applying the seven
+additional changes.
+
+## Exact three-coordinate identity and legal gathering
+
+An ADD `(destination,source,c)` means
+`x_destination <- x_destination + c*x_source`. A chronological list acts in
+listed order, so its matrix product has the last event on the left.
+For three distinct registers `x,y,z`, put
+
+```
+S(a): y += a*z       T(b): x += b*y       U(c): x += c*z.
+```
+
+The two relevant chronological identities, valid over the rationals, are
+
+```
+[S(a), T(b), U(-ab)] = [T(b), S(a)]
+[U(ab), T(b), S(a)]  = [S(a), T(b)].
+```
+
+In the first identity both sides end at
+`(x+b*y, y+a*z, z)` in terms of the initial coordinates. In the second both end
+at `(x+b*y+ab*z, y+a*z, z)`. Thus these equalities preserve arbitrary dirty
+inputs, rather than assuming any operand is zero. The primary checker compares
+exact rational matrices; `independent.py` separately propagates the three
+independent coordinate columns with `Fraction` arithmetic. Equality of these
+three columns proves equality of the entire three-coordinate linear operator.
+
+At every selected site the three ADDs use one common frame. Every intervening
+unselected scalar event reads and writes registers outside the entire selected
+three-register support. Such an event commutes with every selected ADD as an
+operator on the full register space. The selected triple can therefore be
+gathered at its first old position, contracted by one of the identities above,
+and followed by the unchanged intervening events. The checker includes both
+reads and writes in the disjointness test; write-only independence would be
+insufficient.
+
+All eight supports are pairwise disjoint. This also permits the overlapping
+index windows of different sites to be contracted simultaneously. No selected
+window crosses the A prelude, a section boundary, the target cut or a B native
+warp cut. Reconstructed B warp indices change only to locate the same native
+event after the same surviving source events. Native lender registers, map
+columns, ordered entry/exit frames and native order remain identical.
+
+Each local identity embeds as that exact operator on its three registers and
+the identity on every other live or buffer coordinate. Composing these
+equalities with unchanged surrounding operators proves full operator equality
+on all 632 live coordinates plus 91 independent dirty buffers. This argument
+does not inspect or simplify a native map, commute across a native event, or
+assume a native phase convention. It holds with any common linear realization
+of the unchanged surrounding operators. Native realizability and their inherited
+signed phases are separate obligations.
+
+## Projected inverse cleanup
+
+The word contract's ordinary forward sequence is A after `prelude_events`,
+then B with its interleaved native events, then restore. No non-target scalar
+instruction reads a target. This hygiene rule makes the non-target subsystem
+autonomous: deleting target-writing events leaves its invertible operator
+`F_N`. Literal cleanup reverses that projected program, negating ADD
+coefficients, reciprocating nonzero scales and inverting native symbols.
+For each protected helper `r`, the fixed renaming `r -> r+704` applies to both
+sources and destinations of this inverse. It names the inherited private dirty
+buffer; it is not a new allocation by this construction.
+
+Equal full forward operators have equal autonomous non-target blocks.
+Consequently their projected inverses, under the same buffer renaming, are
+equal. Regenerating literal cleanup from the edited ordinary sequence therefore
+preserves its buffer action and every endpoint. The checker compares the entire
+regenerated cleanup list and its canonical digest, rather than retaining an old
+cleanup solely because the forward endpoint matches.
+
+For both new B sites, the first two original ADDs write a target, while the
+third writes a helper. Their contraction changes the target part but retains
+the same single helper ADD in the projection. These sites save two forward
+ADD records and no cleanup records. Each of the five restore sites is wholly
+non-target, saving one forward and one cleanup ADD record. Thus the new saving
+is exactly `7+5=12` scalar ADD records versus PR3998. The old A1858 site adds
+the separately credited `1+1`; against raw PR3734 the combined saving is
+`8+6=14` records.
+
+These are rational scalar ADD records. Some coefficients are `2` or `1/2`.
+The count is not an asserted unit-native instruction saving or physical tariff.
+No zero buffer, unchanged helper or caller-boundary assumption is introduced
+by the local identities.
+
+## Complete chronological frame bill
+
+Algebraic equality alone does not establish a legal or favorable framed
+program. The primary auditor recomputes the entire chronological bill and
+hygiene for each source, credited-only and final word. The independent checker
+implements a second binary trace using explicit immutable point sets in
+`F_2^9`, without importing the primary or retained executable. It authenticates
+the two compressed input byte strings before loading either provider.
+
+A frame is the XOR closure of its listed vectors. A scalar event requires
+every touched register's current frame to be contained in the event frame.
+Each positive dimension difference contributes one recursive child of that
+rank. The trace includes initial frames, the fixed target-cut levels, center
+entry and nested borrowed descents, every native entry and binary frame image,
+the restore stage, and all final successor climbs. Center descent views do
+not replace the persistent main register state. Native frame images are
+checked by enumerating all 512 binary vectors; this is a binary-frame check,
+not signed Clifford verification.
+
+The independent checker compares 149 complete live-register frame states for
+each source/credited/final word: entrance, A exit, both sides of all 72 B native
+events, B exit, restore exit and terminal. All agree. It separately recomputes
+every charge, including intermediate charges that those boundary comparisons
+alone would not determine. The full profile for both providers is
+
+```
+{1:2440, 2:725, 3:224, 4:102, 5:20, 8:8}.
+```
+
+There are 3,519 recursive children and rank mass 5,134. Helper widths remain
+`{4:26,5:2,6:18,7:53,8:96,9:213}`. No rank count changes, so the recursive
+moment agrees identically at every exponent where the inherited profile price
+is defined; no numerical optimization is required. Unchanged cleanup widths
+and native descriptors do not certify physical scheduling, finite precision,
+stock/tape, all-size compilation or outer/BIT obligations. Those remain
+inherited or unknown, rather than being assigned cost zero.
+
+## Evidence, controls and attribution
+
+The primary replay uses the authenticated, unchanged predecessor
+`audit_core.py`. For each provider it freshly checks all three words on the
+full 723-input ordinary and dual free-operator matrices, reverse pullback,
+cleanup boundaries, buffer identity and absence of buffer-to-live leakage.
+This is reuse of a credited interpreter, not a newly independent full-word
+interpreter. The independent checker proves the changes compositionally,
+reconstructs the complete edited word and cleanup, matches their canonical
+digests to `data.json`, and independently certifies the complete frame invoices.
+It does not claim a second full free-operator matrix replay.
+
+Seven in-memory controls per provider must reject: wrong A2 sign, an intervening
+read dependency, duplicate/overlapping support, a crossed native cut, a changed
+common ordered frame, stale cleanup, and an omitted retained gate. Rejection
+uses explicit exceptions and remains active under Python `-O`. These bounded
+controls supplement the exact certificate; they do not imply universal test
+coverage or independent human acceptance.
+
+Chris R / Clear1nsight PR3998 supplies the A2 identity, the old consecutive
+A1858 contraction, and retained proof/source exports. Dataisfire supplies the
+PR3734 literal words. Sagar Thakrar, roger-sato and Arham Tahir supply the
+retained auditor lineage. Jeremy Kothe and Dugongue supply rank-profile and
+paid-budget context, including PR3945/3863. PR1865 by 1337isnot1337 is earlier
+nonconsecutive commuting C3 work with a different identity and source; this
+certificate claims no general priority for commuting graph rewrites.
+Original notices remain under `source/`. This package neither merges a PR nor
+changes the selected frontier.

research/staged544-separated-a2/README.md

@@ -0,0 +1,106 @@
+# Seven separated A2 contractions with an unchanged paid profile
+
+On each exact PR3734 provider, seven separated three-ADD blocks contract to
+two ADDs without crossing a native event. Beyond PR3998's credited consecutive
+A1858 contraction, this removes **seven forward and five inverse-cleanup ADDs**.
+Against the original PR3734 words the combined saving is eight forward and six
+cleanup ADDs. The entire recursive histogram remains
+`{1:2440,2:725,3:224,4:102,5:20,8:8}`: 3,519 children and rank mass 5,134.
+There is **no recursive-moment or kappa gain**, and no measured runtime claim.
+
+The changed premise is a literal event-graph contraction across strictly
+disjoint scalar events. This is outside PR3998's consecutive domain and the
+fixed-graph retiming domains. The seven new blocks retain their exact original ordered frames;
+every intervening event must avoid all three selected registers. Prelude,
+centre and native-warp boundaries remain fixed. It allocates no register or
+buffer. The complete favorable frame bill already gives no recursive saving,
+so this result stops at the frozen scalar witness rather than opening another
+dependent optimization round.
+
+## Exact frozen scope
+
+Sources are PR3998 head `389268a6b5e0373a3125d5c6fcd6995f4ea324f5`,
+which retains the two PR3734 providers at
+`fa041037a3374eaa08feeca0b26a5d6893194147`. All source bytes, blobs and hashes
+are bound in `SOURCES.json`; package-local exports remove any pending-history
+dependency. Only those two old providers are certified. The retained PR3945
+notice is attribution, not an applicability claim about its later words.
+
+Seven new sites use original zero-based coordinates:
+
+| Section | Three ADD indices |
+|---|---|
+| B | 4, 53, 54 |
+| B | 7, 49, 50 |
+| restore | 20, 21, 36 |
+| restore | 22, 23, 38 |
+| restore | 26, 27, 51 |
+| restore | 30, 31, 62 |
+| restore | 32, 33, 73 |
+
+For example, at B4/B53/B54, all three frames are span(30):
+
+```
+196 += 518; 196 -= 588; 588 -= 518
+                 equals
+588 -= 518; 196 -= 588
+```
+
+The equality holds over the rationals on arbitrary dirty inputs. Selected
+events can be gathered because every intervening event is disjoint from all
+three registers. Every source gate, replacement, index and canonical edited
+word/cleanup digest is retained in `data.json`; full words are reconstructed
+in memory without modifying inputs. This is a fixed witness certificate,
+not a complete search or a graph-normal-form theorem.
+
+## Evidence and reproduction
+
+Python 3.12 or later, standard library only:
+
+```
+python3 -B scripts/research_package.py --package research/staged544-separated-a2
+```
+
+`PROOF.md` gives local composition, frame-boundary and projected inverse-cleanup
+arguments. The separate checker compares all 149 complete live-register frame
+states at fixed boundaries for source, credited and final words in each provider,
+and recomputes every intermediate charge. It supplies seven semantic rejection
+controls per provider, alongside 40 production API/CLI controls. The primary verifier reuses the authenticated, unchanged credited
+`audit_core.py` for the complete frame bill, hygiene and free-operator
+ordinary/dual/reverse/cleanup replay. This reuse is not a new independent
+interpreter. `independent.py` supplies separately implemented scoped checks;
+`test_verify.py` exercises semantic and damaged-input controls. Registered
+commands are read-only and Git-free. Exact measured validation and publication
+receipts are recorded in the PR and handoff; a PASS is not full supplier admission.
+
+All native descriptors and their order, helper entrances/exits, cut, wrappers,
+initial corrections and nonedited fields are retained. Warp event indices only
+account for deleted B instructions within their original cut. Physical owner
+scheduling, signed native lowering, finite-width precision/stock/tapes and
+all-size/outer/BIT obligations are inherited or unknown, never zero.
+
+## Open next questions
+
+- Can a different graph remove a paid frame transition? First specify the
+  replacement boundary and complete favorable bill. These seven sites leave
+  every rank count unchanged; another seed or larger separated scan is not
+  justified by this result alone.
+- Does one later exact source word admit these contractions? Pin it and recheck
+  every source index, boundary, cleanup and full invoice before claiming reuse.
+  No PR3945 or later-word applicability is established here.
+
+## Credit and status
+
+Chris R / Clear1nsight PR3998 supplies the A2 identity, consecutive A1858
+contraction, proof context and authenticated source exports. Dataisfire supplies
+the PR3734 literal providers. Sagar Thakrar, roger-sato and Arham Tahir supply
+the retained auditor lineage. Jeremy Kothe and Dugongue's PR3945/3863 supply
+rank-profile and complete-budget context. PR1865 by 1337isnot1337 is an earlier
+nonconsecutive commuting C3 fanout construction, with a different identity and
+source; no general priority for nonconsecutive commuting rewrites is claimed.
+Full native/compiler/owner/source lineage is retained unchanged under `source/`.
+
+New fixed-witness contraction and checks by ToikY with substantial OpenAI Codex
+assistance, including separate AI proof and test contexts. Apache-2.0. No
+independent human or formal-kernel acceptance, new supplier, merge, closure or
+selected-frontier change is claimed.