diff --git a/research/helper300-eight-field-floor/PROOF.md b/research/helper300-eight-field-floor/PROOF.md new file mode 100644 index 0000000000..6720c912fe --- /dev/null +++ b/research/helper300-eight-field-floor/PROOF.md @@ -0,0 +1,221 @@ +# Exact ten-H1 floor for one eight-field backward block + +This is a local mathematical obstruction, not an improved kappa or a +complete multiplication theorem. It concerns arbitrary ADD/SCALE +refactorizations in the fixed eight-field, monotone-frame, no-warp model +specified below. It is stronger than an adjacent-swap failure, but is not a +barrier to a larger native redesign. + +## Sources and exact interval + +Canonical repository checkpoint: `32890bc5de034ab8fc93ac88ead7279a6a416d04`. + +Actual backward provider: + +`research/coupled-helper-neutral-completion/capsule/workspace/swarm-provider-audit-sol-high-20261024/repository/research/native-rank8-helper-provider/WORD.json.gz` + +- Container SHA256: `7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc`. +- Decompressed payload SHA256: `05490717144b3e6c69c0cc9e5c5df5c69d841ca13bf29aabd1b0db180628f038`. +- Its source payload pin is `cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd`. + +That source payload is the decompressed +`research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz`, also copied as +`.../repository/research/native-center-free-code/SOURCE-WORD.json.gz` in +the selected capsule. Both compressed copies have SHA256 +`7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05`. + +The interval is **[9044, 9116)**, with zero-based native event indices. +Starting from roles {19,300,301}, its exact closure under every scalar +contact inside this interval is + +`[19,40,288,289,295,299,300,301]`. + +It contains no warp, cache COPY, owned CLEAR, or zero retag on these roles. +Every instruction inside the interval that touches a role in this set touches +only roles in this set. Thus the intervening other-role instructions commute +with an isolated replacement of the block. The emitted `RESULT.json` +contains every retained event and the exact rational matrix. + +The fixed boundary charts are: + +| Role | Entry frame | Exit frame | +|---|---:|---:| +|19|21|423| +|40|42|422| +|288|103|422| +|289|103|423| +|295|57|430| +|299|42|419| +|300|0|430| +|301|0|419| + +Frame 0 is the zero subspace. Frames 21,42,57,103 are lines. The four exit +frames 419,422,423,430 are pairwise distinct planes in F_2^9. +In particular 419=span(273,51), 423=span(273,102), and +430=span(273,85). All fixed entry frames lie in their respective exit planes. + +The source block uses exactly ten rank-one climbs, so has paid cost 10 in +the normalized moment sum. This statement is about this isolated block, +not the complete local provider invoice. + +## Replacement model + +A replacement uses exactly these eight whole fields, with independent +arbitrary entering values, and the same field capacities and boundary charts. +It may use any finite number of rational scalar ADD and nonzero SCALE gates, +any coefficients, any order, and any temporary basis changes. ADD operands +must occupy the identical actual frame. It may choose any intermediate +binary subspaces, not merely frames appearing in the source catalogue. +Every field's frame moves by strict nested ascent from its entry to its fixed +exit. A paid climb from E to F has positive integer rank dim(F)-dim(E). + +No auxiliary field, new warp, descent, chart-changing exchange, cross-column conversion, new input +relation, or changed boundary is permitted. No approximation or packing of +multiple arbitrary fields into a field of smaller capacity is permitted. +These are explicit restrictions of this small optimization instance. + +Since each final frame is a plane, an intermediate frame for that field is +a subspace of that plane. A field at one exit plane cannot later contact a +field whose exit plane is different: equal frames at such a contact would +force the different plane to contain the first plane, impossible in dimension +two. This fact is independent of the ordering or scalar coefficients. + +## Exact local identity criterion + +Use the repository's native chart semantics: a climb changes a field's chart +and preserves its formal row; a coframed ADD/SCALE acts on those rows by its +ordinary rational elementary matrix. This is the convention explicitly used +by `research/kappa-rebuild/complex/native_extensions.py:84-142`. + +In a warp-free window, let G_E and G_F be the block diagonal invertible chart +maps at entry and exit. A legal scalar factorization with rational transfer +matrix T induces the physical map + + G_F (T tensor I) G_E^{-1}. + +Consequently, with the same boundary charts, equality of rational transfer +matrices is necessary and sufficient for exact local physical equality at +every positive width under the inherited native chart contract. Scalar +coefficients remain exterior coefficients; they are not raised to the width. +This conclusion does not excuse checking frame legality or admitting a new +physical primitive. It also does not apply to an unmodelled warp: such a +window would require its operator labels and phases, or segmentation at the +warp boundaries, instead of an unlabelled rational matrix. + +There is no hidden zero-input assumption. The actual native prefix through +event 9043 consists only of invertible persistent ADD/SCALE, warp and climb +operations, plus annotations. The source audit checks that there is no +destructive scalar operation in this prefix. Under the inherited native +contract, each of its warps and climbs is invertible. Thus all 632 persistent +values at this cut can vary arbitrarily; in particular these eight values are +independent. The provider's exterior input basis and monomial/scalar wrappers +are themselves invertible and do not impose an input relation. + +## A two-input, one-carrier lemma + +Consider two independent entering field values a,b, initially the only fields +at the zero frame. Assume one of them jumps directly from zero to its final +plane P. Call it the direct field, allowing any prior changes of basis between +the two zero-frame fields. + +Then the collection of outputs on fields whose final plane differs from P +has dependence of rank at most one on (a,b) in formal scalar-row coordinates. +Equivalently, its physical rank on these two full input fields is at most one +field's capacity. + +Proof. Before either zero-frame field leaves zero, only those two fields can +interact with a or b: all other fields start at nonzero frames and cannot +descend. Arbitrary scalar operations at zero may replace a,b by arbitrary +linear combinations. Once one of these two fields departs zero it cannot +return. The direct field never visits an intermediate line; after its jump +to P, it can contact only fields whose final plane is P. Such fields also +cannot carry a subsequent message to another exit plane once they have +reached P. Thus all dependence of the other exit-plane outputs on (a,b) +must pass through the *other* zero-frame field at its single departure from +zero. At that moment it holds one linear combination alpha*a+beta*b. +Subsequent ADD/SCALE operations and legal climbs can distribute or cancel +this value but cannot create a second independent dependence on (a,b). +This reasoning permits feedback, arbitrarily many scalar gates, either +departure order, and arbitrary initial temporary bases. End proof. + +The conclusion fails if extra zero-frame fields, descending transport, +new inter-plane warps, or modified final planes are admitted. They are +outside this lemma's use here. + +## Applying the lemma to both potential H2 replacements + +Let a and b denote the entering values of roles 300 and 301. In the exact +backward transfer matrix, the following coefficients on (a,b) occur: + +| Output | Final plane | Coefficient row on (a,b) | +|---|---:|---| +|19|423|(0,1)| +|300|430|(1,0)| +|301|419|(-1,-1)| + +Other entering values occur in these outputs but do not affect this rank +calculation. These three rows can be read directly from the exact eight-field +matrix in `RESULT.json`. + +If role 300 jumped directly 0 -> 430, outputs 19 and 301 are outside plane +430, and their two coefficient rows have determinant 1. Their dependence on +(a,b) therefore has rank two, contradicting the lemma's rank-one bound. + +If role 301 jumped directly 0 -> 419, outputs 19 and 300 are outside plane +419; their two coefficient rows have determinant -1. Again rank two +contradicts the lemma. + +Hence neither zero-start role may make a direct rank-two climb in an exact +replacement. Each must visit a line and use two rank-one climbs. Each of the +other six roles starts at a line and ends at a plane, so requires one rank-one +climb. The total cost is therefore at least + + 2 + 2 + 6 = 10 H1. + +The original block attains this cost. The minimum is exactly ten H1 for +every exponent 0 < t < 1, not merely for a sampled value of t. In fact the +rank-count statement itself is independent of t. There is no positive +recursive moment saving in this fixed-boundary, eight-field model. + +## Protected interfaces and limitations + +Restoring all eight rows and frames at event 9116 preserves every later +instruction, including the cached-centre copies at source event indices +11207,11222,11237,11252,11267,11282,11297,11322. Their sources and frames are +listed in `RESULT.json`, as are all eight later exact-zero retags. This is +a compositional statement, not a fresh full cached-centre or phase replay. + +The illustrative h300 motif in PR5465 is forward-oriented. Its x19-to-plane430 +coefficient is not a valid backward witness: the actual backward outputs at +plane430 have no x19 coefficient. The rank-two witnesses above use the actual +selected backward tape and remain valid under arbitrary initial bases. + +This does not rule out a rewrite extending past the chosen boundary. The +same seed's closure in [9044,9137) has twenty fields, not eight. Other routes +include auxiliary fields with their complete bill, changed warps or charts, +a larger helper factorization, or a genuinely changed caller interface. +No global optimality, whole-provider lower bound, improved kappa, compiler +funding, or formal-kernel acceptance is claimed. + +## Evidence and predecessor credit + +`verify.py` and the separately authored `check_window.py` independently read +the frozen inputs and compute the small rational matrix, fixed boundary frames, +source paid histogram, closed role set and source bindings. The primary checker +also records the prefix grammar and later cache checkpoints. Both run read-only +against the repository by default; the primary checker compares its recomputed +certificate with `RESULT.json`. +The executable computation is finite exact evidence. The carrier lemma and +the resulting arbitrary-factorization floor are the written mathematical +argument above, not an exhaustive program enumeration or proof-assistant +result. + +Credit Cao Yifan's native word, Dillon's coupled provider, the cached-centre +relations of Ali Romman, the selected completion and source validation of +Clear1nsight, and the native/compiler lineage retained in those sources. +PR5465 (`b123ff44a211b9fc96b9f8fd1538e9965a95b34e`), especially R13 sections +3-4, supplied the h300 bottleneck and motivation to go beyond one-step swaps. +This note is an independent AI-assisted local mathematical audit and does not +claim independent human review or priority for elementary cut-rank arguments. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/helper300-eight-field-floor/README.md b/research/helper300-eight-field-floor/README.md new file mode 100644 index 0000000000..5215762d9d --- /dev/null +++ b/research/helper300-eight-field-floor/README.md @@ -0,0 +1,102 @@ +# An exact ten-H1 floor for one backward helper block + +The proposed `H1 + H1 -> H2` saving cannot be realized inside one precise +eight-field block of the selected backward provider. Every exact replacement +in the model below needs **ten rank-one climbs**, and the existing block +attains that bill. This is a local obstruction with an attaining construction; +it does not improve kappa or exclude a larger redesign. + +The block is the dependency closure of roles `{19,300,301}` within zero-based +provider events **[9044,9116)**. It has eight fields and 28 relevant events: +ten H1 climbs, sixteen ADDs and two SCALEs. Intervening events on disjoint +fields remain unchanged. + +## Result and scope + +Allow any finite rational ADD/SCALE factorization, including temporary basis +changes and arbitrary intermediate binary subspaces. Keep the eight fields, +arbitrary entering values, entry/exit frames and monotone climbs. No new warp, +auxiliary field, descent, chart-changing exchange, cross-column conversion or +changed output contract is allowed. + +Six fields start at lines and end at planes, requiring six H1 climbs. Fields +300 and 301 start at frame zero and end at distinct planes. If either jumped +directly to its exit plane, only the other zero-frame field could carry its +initial two-dimensional information to the other exit planes. Those outputs +require rank-two dependence, while one carrier supplies rank at most one. +Both helpers therefore need two H1 climbs: the minimum is `6 + 2 + 2 = 10` +for every `0 < t < 1`. See [the proof](PROOF.md). + +This permits a changed ADD graph, beyond the fixed-word reorder and adjacent +swap searches in [PR #5465](https://github.com/CrocSwap/integer-mult-bounds/pull/5465). +Its R13 sections 3–4 motivate the experiment, but illustrate the forward word. +The forward x19-to-plane430 witness is zero backward; this package uses the +actual backward tape and two different rank witnesses. + +Base: canonical main `32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority 7. +Selected conditional kappa remains `0.003027288235`. The provider's decompressed +source hash binds the canonical frames. [SOURCES.json](SOURCES.json) pins exact +inputs at the canonical base. The pending [#5465 R13 note](https://github.com/GamingPuzzled/integer-mult-bounds/blob/b123ff44a211b9fc96b9f8fd1538e9965a95b34e/research/frontier-word-reorder-ceilings/r13-reorder/README.md) +is a motivation/overlap reference, not a proof premise or replay input. Its +SHA256 is `f5da8c86df033f0697d305ac4a9798ba60ab1a765e5701648560628a36ad1f62`; +no unmerged Git object is required for verification. +[TASK.json](TASK.json) records the narrowed historical card and stopping rule; +the card's 5% supplier-expansion gate is not claimed satisfied. + +## Reproduction and evidence + +Python 3.12 and the standard library suffice. From the repository root: + +```sh +python3 -B scripts/research_package.py --package research/helper300-eight-field-floor +``` + +The primary verifier reconstructs the local operator and tests the source-bound +rank-cut hypotheses. The separately authored source checker reconstructs the +matrix without importing the primary verifier. Both include semantic failure +controls; normal and optimized executions are registered. The primary checker +also evaluates the inherited forward window as an orientation control; the +claimed selected-provider result is backward. It compares recomputed evidence +with `RESULT.json`; use `verify.py --write-result` only to regenerate that file. Exact finite checks +support the written arbitrary-factorization proof; they are not a program +enumeration or proof-assistant certificate. + +Physical all-width interpretation is conditional on the inherited native chart +contract. No complete provider/caller replay, new phase construction, compiler +funding, Lean audit, independent human review or new exponent is claimed. +Restoring the block's rows and charts preserves the unchanged continuation, +including later cached-centre checkpoints, by composition. + +The [canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/5470) +records the claim and handoff. Targeted live PR and Discussion searches found +no matching submitted scope; hidden comments and unpublished work are outside +that coverage. The selected source-binding baseline passed; historical ceiling +arithmetic is not transferred to the current supplier. + +## Open next questions + +1. Extending the same seed through `[9044,9137)` yields twenty fields. Extract + its entry/exit geometry and rank cuts before synthesis. It could expose + another zero-frame carrier or useful changed output plane; its full bill + and protected contacts remain to be checked. +2. For a changed transport or auxiliary field, specify the complete producer + and consumer contract and price it first. One extra H1 already costs more + than the proposed single merge saves, so a profitable escape needs another + compensating saving. No such transport or larger construction is supplied. + +Structured questions and blockers are in [TASK.json](TASK.json). + +## Credit + +Credit Cao Yifan's #4610 native word, Dillon Amburgey's #5402 coupled provider, +Ali Romman's cached-centre relations, Chris R/Clear1nsight's #5413 completion +and source validation, GamingPuzzled's #5465 bottleneck analysis, and the +retained native/compiler lineage. Historical helper-basis screens by tomdif +on the older #1286 provider are related predecessors, not the same local +obstruction. The cut-rank argument uses elementary linear algebra; no priority +claim is made for that general method. + +Prepared by **apoursh**, with substantial OpenAI Codex assistance from one +coordinator and three workers for synthesis, mathematical audit, and independent +source reconstruction. AI-worker separation is not independent human review. +New work is Apache-2.0; predecessor notices are retained. diff --git a/research/helper300-eight-field-floor/RESULT.json b/research/helper300-eight-field-floor/RESULT.json new file mode 100644 index 0000000000..4443a900ff --- /dev/null +++ b/research/helper300-eight-field-floor/RESULT.json @@ -0,0 +1,2445 @@ +{ + "attainment": "the exact retained local tape", + "backward_obstructions": [ + { + "collapsed_helpers": [ + 301 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 300, + 301 + ], + "output_fields": [ + 19, + 300 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 1, + "cut_edges": [ + [ + "0", + "0,85", + 1 + ] + ], + "source_side": [ + "0", + "0,51,273,290", + "SOURCE" + ] + }, + "required_minor": [ + [ + "0", + "1" + ], + [ + "1", + "0" + ] + ], + "required_rank": 2 + }, + { + "collapsed_helpers": [ + 301 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 273 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 300, + 301 + ], + "output_fields": [ + 19, + 300 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 1, + "cut_edges": [ + [ + "0", + "0,273", + 1 + ] + ], + "source_side": [ + "0", + "0,51,273,290", + "SOURCE" + ] + }, + "required_minor": [ + [ + "0", + "1" + ], + [ + "1", + "0" + ] + ], + "required_rank": 2 + }, + { + "collapsed_helpers": [ + 301 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 324 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 300, + 301 + ], + "output_fields": [ + 19, + 300 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 1, + "cut_edges": [ + [ + "0", + "0,324", + 1 + ] + ], + "source_side": [ + "0", + "0,51,273,290", + "SOURCE" + ] + }, + "required_minor": [ + [ + "0", + "1" + ], + [ + "1", + "0" + ] + ], + "required_rank": 2 + }, + { + "collapsed_helpers": [ + 300 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 300, + 301 + ], + "output_fields": [ + 19, + 301 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 1, + "cut_edges": [ + [ + "0", + "0,51", + 1 + ] + ], + "source_side": [ + "0", + "0,85,273,324", + "SOURCE" + ] + }, + "required_minor": [ + [ + "0", + "1" + ], + [ + "-1", + "-1" + ] + ], + "required_rank": 2 + }, + { + "collapsed_helpers": [ + 300 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 273 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 300, + 301 + ], + "output_fields": [ + 19, + 301 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 1, + "cut_edges": [ + [ + "0", + "0,273", + 1 + ] + ], + "source_side": [ + "0", + "0,85,273,324", + "SOURCE" + ] + }, + "required_minor": [ + [ + "0", + "1" + ], + [ + "-1", + "-1" + ] + ], + "required_rank": 2 + }, + { + "collapsed_helpers": [ + 300 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 290 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 300, + 301 + ], + "output_fields": [ + 19, + 301 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 1, + "cut_edges": [ + [ + "0", + "0,290", + 1 + ] + ], + "source_side": [ + "0", + "0,85,273,324", + "SOURCE" + ] + }, + "required_minor": [ + [ + "0", + "1" + ], + [ + "-1", + "-1" + ] + ], + "required_rank": 2 + }, + { + "collapsed_helpers": [ + 300, + 301 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 300, + 301 + ], + "output_fields": [ + 19, + 301 + ], + "paid_profile": { + "1": 6, + "2": 2 + }, + "rank_cut": { + "capacity": 1, + "cut_edges": [ + [ + "0", + "0,51,273,290", + 1 + ] + ], + "source_side": [ + "0", + "0,85,273,324", + "SOURCE" + ] + }, + "required_minor": [ + [ + "0", + "1" + ], + [ + "-1", + "-1" + ] + ], + "required_rank": 2 + } + ], + "block": { + "fields": [ + 19, + 40, + 288, + 289, + 295, + 299, + 300, + 301 + ], + "indexing": "zero-based half-open", + "start": 9044, + "stop": 9116 + }, + "complete_trajectory_assignments_per_orientation": 16, + "controls": [ + "zero-prefix-scale-rejected", + "restore-helper-300-line21-rank-flow-admitted", + "restore-helper-301-line21-rank-flow-admitted", + "delete-required-b-coefficient-destroys-obstruction", + "changed-provider-source-rejected" + ], + "cost_saving_trajectories_rejected_per_orientation": 7, + "first_later_protected_cache_copy": 11207, + "forward_obstructions": [ + { + "collapsed_helpers": [ + 301 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 19 + ], + "output_fields": [ + 301 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 0, + "cut_edges": [], + "source_side": [ + "0,102,273,375", + "0,273", + "SOURCE" + ] + }, + "required_minor": [ + [ + "1/2" + ] + ], + "required_rank": 1 + }, + { + "collapsed_helpers": [ + 301 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 273 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 19 + ], + "output_fields": [ + 301 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 0, + "cut_edges": [], + "source_side": [ + "0,102,273,375", + "0,273", + "0,85,273,324", + "SOURCE" + ] + }, + "required_minor": [ + [ + "1/2" + ] + ], + "required_rank": 1 + }, + { + "collapsed_helpers": [ + 301 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 324 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 19 + ], + "output_fields": [ + 301 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 0, + "cut_edges": [], + "source_side": [ + "0,102,273,375", + "0,273", + "SOURCE" + ] + }, + "required_minor": [ + [ + "1/2" + ] + ], + "required_rank": 1 + }, + { + "collapsed_helpers": [ + 300 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 19 + ], + "output_fields": [ + 300 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 0, + "cut_edges": [], + "source_side": [ + "0,102,273,375", + "0,273", + "SOURCE" + ] + }, + "required_minor": [ + [ + "1/2" + ] + ], + "required_rank": 1 + }, + { + "collapsed_helpers": [ + 300 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 273 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 19 + ], + "output_fields": [ + 300 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 0, + "cut_edges": [], + "source_side": [ + "0,102,273,375", + "0,273", + "0,51,273,290", + "SOURCE" + ] + }, + "required_minor": [ + [ + "1/2" + ] + ], + "required_rank": 1 + }, + { + "collapsed_helpers": [ + 300 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 290 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 19 + ], + "output_fields": [ + 300 + ], + "paid_profile": { + "1": 8, + "2": 1 + }, + "rank_cut": { + "capacity": 0, + "cut_edges": [], + "source_side": [ + "0,102,273,375", + "0,273", + "SOURCE" + ] + }, + "required_minor": [ + [ + "1/2" + ] + ], + "required_rank": 1 + }, + { + "collapsed_helpers": [ + 300, + 301 + ], + "helper_paths": { + "300": [ + [ + 0 + ], + [ + 0, + 85, + 273, + 324 + ] + ], + "301": [ + [ + 0 + ], + [ + 0, + 51, + 273, + 290 + ] + ] + }, + "input_fields": [ + 19 + ], + "output_fields": [ + 300 + ], + "paid_profile": { + "1": 6, + "2": 2 + }, + "rank_cut": { + "capacity": 0, + "cut_edges": [], + "source_side": [ + "0,102,273,375", + "0,273", + "SOURCE" + ] + }, + "required_minor": [ + [ + "1/2" + ] + ], + "required_rank": 1 + } + ], + "frame_bases": { + "0": [], + "103": [ + 375 + ], + "21": [ + 273 + ], + "419": [ + 273, + 51 + ], + "42": [ + 290 + ], + "422": [ + 290, + 85 + ], + "423": [ + 273, + 102 + ], + "430": [ + 273, + 85 + ], + "57": [ + 324 + ] + }, + "inherited_forward": { + "entry_frames": { + "19": 21, + "40": 42, + "288": 103, + "289": 103, + "295": 57, + "299": 42, + "300": 0, + "301": 0 + }, + "exit_frames": { + "19": 423, + "40": 422, + "288": 422, + "289": 423, + "295": 430, + "299": 419, + "300": 430, + "301": 419 + }, + "local_events": [ + [ + 9044, + [ + "climb", + "warp_retimed", + 300, + 0, + 21, + 1 + ] + ], + [ + 9045, + [ + "scalar", + [ + "add", + [ + "L", + 300 + ], + [ + "L", + 19 + ], + 1, + 1 + ], + 21 + ] + ], + [ + 9046, + [ + "climb", + "warp_retimed", + 301, + 0, + 21, + 1 + ] + ], + [ + 9047, + [ + "scalar", + [ + "add", + [ + "L", + 301 + ], + [ + "L", + 19 + ], + 1, + 1 + ], + 21 + ] + ], + [ + 9056, + [ + "scalar", + [ + "add", + [ + "L", + 40 + ], + [ + "L", + 299 + ], + 1, + 1 + ], + 42 + ] + ], + [ + 9057, + [ + "scalar", + [ + "add", + [ + "L", + 299 + ], + [ + "L", + 40 + ], + -1, + 1 + ], + 42 + ] + ], + [ + 9058, + [ + "scalar", + [ + "add", + [ + "L", + 40 + ], + [ + "L", + 299 + ], + 1, + 1 + ], + 42 + ] + ], + [ + 9059, + [ + "scalar", + [ + "scale", + [ + "L", + 299 + ], + -1, + 1 + ], + 42 + ] + ], + [ + 9060, + [ + "scalar", + [ + "add", + [ + "L", + 19 + ], + [ + "L", + 301 + ], + 1, + 1 + ], + 21 + ] + ], + [ + 9061, + [ + "scalar", + [ + "add", + [ + "L", + 301 + ], + [ + "L", + 19 + ], + -1, + 1 + ], + 21 + ] + ], + [ + 9062, + [ + "scalar", + [ + "add", + [ + "L", + 19 + ], + [ + "L", + 301 + ], + 1, + 1 + ], + 21 + ] + ], + [ + 9063, + [ + "scalar", + [ + "scale", + [ + "L", + 301 + ], + -1, + 1 + ], + 21 + ] + ], + [ + 9072, + [ + "climb", + "warp_retimed", + 288, + 103, + 422, + 1 + ] + ], + [ + 9073, + [ + "climb", + "warp_retimed", + 40, + 42, + 422, + 1 + ] + ], + [ + 9074, + [ + "scalar", + [ + "add", + [ + "L", + 288 + ], + [ + "L", + 40 + ], + 1, + 1 + ], + 422 + ] + ], + [ + 9075, + [ + "scalar", + [ + "add", + [ + "L", + 40 + ], + [ + "L", + 288 + ], + -1, + 2 + ], + 422 + ] + ], + [ + 9076, + [ + "climb", + "warp_retimed", + 289, + 103, + 423, + 1 + ] + ], + [ + 9077, + [ + "climb", + "warp_retimed", + 19, + 21, + 423, + 1 + ] + ], + [ + 9078, + [ + "scalar", + [ + "add", + [ + "L", + 289 + ], + [ + "L", + 19 + ], + 1, + 1 + ], + 423 + ] + ], + [ + 9079, + [ + "scalar", + [ + "add", + [ + "L", + 19 + ], + [ + "L", + 289 + ], + -1, + 2 + ], + 423 + ] + ], + [ + 9104, + [ + "climb", + "warp_retimed", + 295, + 57, + 430, + 1 + ] + ], + [ + 9105, + [ + "climb", + "warp_retimed", + 300, + 21, + 430, + 1 + ] + ], + [ + 9106, + [ + "scalar", + [ + "add", + [ + "L", + 295 + ], + [ + "L", + 300 + ], + 1, + 1 + ], + 430 + ] + ], + [ + 9107, + [ + "scalar", + [ + "add", + [ + "L", + 300 + ], + [ + "L", + 295 + ], + -1, + 2 + ], + 430 + ] + ], + [ + 9112, + [ + "climb", + "warp_retimed", + 299, + 42, + 419, + 1 + ] + ], + [ + 9113, + [ + "climb", + "warp_retimed", + 301, + 21, + 419, + 1 + ] + ], + [ + 9114, + [ + "scalar", + [ + "add", + [ + "L", + 299 + ], + [ + "L", + 301 + ], + 1, + 1 + ], + 419 + ] + ], + [ + 9115, + [ + "scalar", + [ + "add", + [ + "L", + 301 + ], + [ + "L", + 299 + ], + -1, + 2 + ], + 419 + ] + ] + ], + "matrix": [ + [ + "1/2", + "0", + "0", + "-1/2", + "0", + "0", + "0", + "1/2" + ], + [ + "0", + "0", + "-1/2", + "0", + "0", + "1/2", + "0", + "0" + ], + [ + "0", + "0", + "1", + "0", + "0", + "1", + "0", + "0" + ], + [ + "1", + "0", + "0", + "1", + "0", + "0", + "0", + "1" + ], + [ + "1", + "0", + "0", + "0", + "1", + "0", + "1", + "0" + ], + [ + "1", + "1", + "0", + "0", + "0", + "0", + "0", + "0" + ], + [ + "1/2", + "0", + "0", + "0", + "-1/2", + "0", + "1/2", + "0" + ], + [ + "1/2", + "-1/2", + "0", + "0", + "0", + "0", + "0", + "0" + ] + ], + "paid_profile": { + "1": 10 + }, + "retained_paths": { + "19": [ + 21, + 423 + ], + "40": [ + 42, + 422 + ], + "288": [ + 103, + 422 + ], + "289": [ + 103, + 423 + ], + "295": [ + 57, + 430 + ], + "299": [ + 42, + 419 + ], + "300": [ + 0, + 21, + 430 + ], + "301": [ + 0, + 21, + 419 + ] + } + }, + "later_zero_retags": [ + [ + 15608, + [ + "zero_retag", + 92, + 254, + 1 + ] + ], + [ + 15894, + [ + "zero_retag", + 9, + 624, + 1 + ] + ], + [ + 15900, + [ + "zero_retag", + 11, + 621, + 1 + ] + ], + [ + 17269, + [ + "zero_retag", + 240, + 280, + 1 + ] + ], + [ + 17280, + [ + "zero_retag", + 81, + 619, + 1 + ] + ], + [ + 17288, + [ + "zero_retag", + 57, + 274, + 1 + ] + ], + [ + 17604, + [ + "zero_retag", + 288, + 281, + 1 + ] + ], + [ + 17746, + [ + "zero_retag", + 224, + 279, + 1 + ] + ] + ], + "local_minimum_invoice": { + "H1": 10 + }, + "moment_exponent_interval": "0(u-v,(u+v)/2) butterflies, rather than serial row replay. +EXPECTED_TWICE = [ + [0,0,0,-2,0,0,0,2], [0,0,-2,0,0,2,0,0], + [0,0,1,0,0,1,0,0], [0,0,0,1,0,0,0,1], + [0,0,0,0,1,0,1,0], [1,1,0,0,0,0,-1,-1], + [0,0,0,0,-2,0,2,0], [2,-2,0,0,0,0,-2,-2], +] + +def require(ok, message): + if not ok: + raise ValueError(message) + +def sha(b): + return hashlib.sha256(b).hexdigest() + +def load_pinned(path, expected): + raw = path.read_bytes() + data = gzip.decompress(raw) + require(sha(data) == expected, 'source payload hash mismatch') + return json.loads(data), {'path':path.relative_to(ROOT).as_posix(), 'compressed_sha256':sha(raw), + 'payload_sha256':sha(data), 'payload_bytes':len(data)} + +def touched(event): + if event[0] == 'climb': + return {event[2]} + if event[0] == 'scalar': + op = event[1] + require(op[0] in ('add','scale'), 'unexpected scalar in local window') + refs = op[1:3] if op[0] == 'add' else op[1:2] + require(all(x[0] == 'L' for x in refs), 'nonpersistent local owner') + return {x[1] for x in refs} + raise ValueError('unexpected event in local window') + +def closure(events): + fields = {19,300,301} + while True: + expanded = set(fields) + for _, event in events: + support = touched(event) + if support & fields: + expanded |= support + if expanded == fields: + return sorted(fields) + fields = expanded + +def span(basis): + result = {0} + for x in basis: + result |= {y ^ x for y in tuple(result)} + return result + +def prefix_frames(word, canonical): + """Source bookkeeping only; no coefficient/operator execution.""" + f = {('L',i):x for i,x in enumerate(canonical['start'])} + f.update({('C',i):0 for i in range(9)}) + for index,event in enumerate(word[:FIRST]): + kind=event[0] + if kind == 'climb': + _,_,owner,a,b,_=event + require(f[('L',owner)] == a, f'prefix climb chart at {index}') + f[('L',owner)] = b + elif kind == 'warp': + _,owner,_,a,b=event + require(f[tuple(owner)] == a, f'prefix warp chart at {index}') + f[tuple(owner)] = b + elif kind == 'scalar': + op, chart = event[1:] + owners=op[1:3] if op[0] in ('add','copy') else op[1:2] + for owner in owners: + # CLEAR resets an owned field to the declared chart; no CLEAR + # or COPY occurs before this window in the selected source. + require(f[tuple(owner)] == chart, f'prefix scalar chart at {index}') + elif kind in ('phase','adapter'): + pass + else: + raise ValueError(f'unhandled prefix event {kind}') + return [f[('L',x)] for x in FIELDS] + +def audit(events, frames): + require(closure(events) == FIELDS, 'dependency closure mismatch') + selected=[(i,e) for i,e in events if touched(e)&set(FIELDS)] + f=dict(zip(FIELDS,ENTRY)) + mat={r:[Q(int(j==k)) for j in range(8)] for k,r in enumerate(FIELDS)} + paid=[] + for index,event in selected: + require(touched(event)<=set(FIELDS),'external dependency') + if event[0]=='climb': + _,_,r,a,b,rank=event + require(f[r]==a,f'climb input chart at {index}') + sa,sb=span(frames[a]),span(frames[b]) + require(sa <= sb,f'nonmonotone climb at {index}') + require(len(sa)==2**len(frames[a]) and len(sb)==2**len(frames[b]),'dependent frame basis') + require(rank==len(frames[b])-len(frames[a]),f'wrong paid rank at {index}') + f[r]=b + paid.append({'event':index,'owner':r,'from':a,'to':b,'rank':rank}) + else: + op,chart=event[1:] + for r in touched(event): + require(f[r]==chart,f'scalar operand chart at {index}') + coefficient=Q(op[-2],op[-1]) + if op[0]=='add': + dest,source=op[1][1],op[2][1] + mat[dest]=[a+coefficient*b for a,b in zip(mat[dest],mat[source])] + else: + dest=op[1][1] + mat[dest]=[coefficient*a for a in mat[dest]] + require([f[x] for x in FIELDS]==EXIT,'exit charts mismatch') + require(Counter(x['rank'] for x in paid)=={1:10},'paid profile mismatch') + matrix=[mat[x] for x in FIELDS] + require(matrix==[[Q(a,2) for a in row] for row in EXPECTED_TWICE], 'all-input transfer mismatch') + require(len(selected)==28,'selected event count mismatch') + return selected,paid,matrix + +def replay_vector(selected, vector): + values=dict(zip(FIELDS,vector)) + for _,event in selected: + if event[0]!='scalar': + continue + op=event[1] + r=op[1][1] + if op[0]=='add': + values[r] += (values[op[2][1]]*op[3])/op[4] + else: + values[r] = (values[r]*op[2])/op[3] + return [values[x] for x in FIELDS] + +def inverse_matrix(matrix): + a=[row[:]+[Q(i==j) for j in range(8)] for i,row in enumerate(matrix)] + determinant=Q(1) + for col in range(8): + pivot=next(i for i in range(col,8) if a[i][col]) + if pivot!=col: + a[col],a[pivot]=a[pivot],a[col];determinant=-determinant + factor=a[col][col];determinant*=factor + a[col]=[x/factor for x in a[col]] + for i in range(8): + if i!=col: + factor=a[i][col] + a[i]=[x-factor*y for x,y in zip(a[i],a[col])] + inverse=[row[8:] for row in a] + for left,right in [(matrix,inverse),(inverse,matrix)]: + require(all(sum(left[i][k]*right[k][j] for k in range(8))==int(i==j) + for i in range(8) for j in range(8)), 'two-sided inverse failure') + return determinant,inverse + +def main(): + parser=argparse.ArgumentParser() + parser.add_argument('--output', type=Path) + args=parser.parse_args() + word,word_pin=load_pinned(WORD,WORD_PAYLOAD) + source,source_pin=load_pinned(SOURCE,SOURCE_PAYLOAD) + require(word['direction']=='backward' and word['source_sha256']==SOURCE_PAYLOAD,'source binding') + canonical=source['canonical'];require(prefix_frames(word['word'],canonical)==ENTRY,'entry charts') + events=list(enumerate(word['word']))[FIRST:STOP] + selected,paid,matrix=audit(events,canonical['frames']) + # Separate scalar-value implementation: each of eight arbitrary-input basis + # columns and a signed rational vector, all compared with the matrix map. + samples=[[Q(i==j) for i in range(8)] for j in range(8)] + samples.append([Q((-1)**i*(i+1),i+2) for i in range(8)]) + for vector in samples: + require(replay_vector(selected,vector)==[sum(a*b for a,b in zip(row,vector)) for row in matrix], + 'literal vector versus matrix disagreement') + determinant,inverse=inverse_matrix(matrix) + controls=[] + def mutation(name,mutate): + bad=deepcopy(events);mutate(bad) + try: + audit(bad,canonical['frames']) + except (ValueError,IndexError,KeyError,ZeroDivisionError): + controls.append(name) + else: + raise ValueError('accepted mutant: '+name) + def item(events,index): + return next(e for i,e in events if i==index) + mutation('wrong_add_sign_9045',lambda e:item(e,9045)[1].__setitem__(3,1)) + mutation('wrong_half_butterfly_9079',lambda e:item(e,9079)[1].__setitem__(4,1)) + mutation('missing_dirty_partner_9114',lambda e:item(e,9114)[1].__setitem__(2,['L',300])) + mutation('deleted_swap_scale_9063',lambda e:e.__setitem__(slice(None),[(i,x) for i,x in e if i!=9063])) + mutation('undercharged_climb_9044',lambda e:item(e,9044).__setitem__(5,0)) + mutation('wrong_scalar_frame_9078',lambda e:item(e,9078).__setitem__(2,422)) + mutation('outside_dependency_9114',lambda e:item(e,9114)[1].__setitem__(2,['L',302])) + mutation('short_window_missing_9115',lambda e:e.pop()) + mutation('reversed_swap_order',lambda e:e.__setitem__(slice(16,18),list(reversed(e[16:18])))) + report={'status':'PASS_INDEPENDENT_EIGHT_FIELD_WINDOW', + 'scope':'Exact normalized-row transfer with source-bound charts; physical native semantics inherited.', + 'source_pins':[word_pin,source_pin],'interval':[FIRST,STOP], + 'closure_seed':[19,300,301],'fields':FIELDS,'interval_events':len(events), + 'selected_events':selected,'paid_climbs':paid,'paid_profile':{'1':10}, + 'entry_frames':dict(zip(FIELDS,ENTRY)),'exit_frames':dict(zip(FIELDS,EXIT)), + 'frame_bases':{i:canonical['frames'][i] for i in sorted(set(ENTRY+EXIT))}, + 'matrix':[[str(a) for a in row] for row in matrix], + 'determinant':str(determinant),'inverse':[[str(a) for a in row] for row in inverse], + 'basis_columns_checked':8,'signed_rational_vectors_checked':1, + 'mutation_controls_rejected':controls} + if args.output: + args.output.write_text(json.dumps(report,indent=2)+'\n') + print(json.dumps(report,indent=2)) + +if __name__=='__main__': + main() diff --git a/research/helper300-eight-field-floor/verify.py b/research/helper300-eight-field-floor/verify.py new file mode 100644 index 0000000000..c022b1435b --- /dev/null +++ b/research/helper300-eight-field-floor/verify.py @@ -0,0 +1,396 @@ +#!/usr/bin/env python3 +"""Exact eight-field ADD-resynthesis obstruction; standard library only. + +The optimistic linear information-flow network permits arbitrary scalar mixing +at every shared frame. Its unit-capacity wires give necessary rank conditions, +never sufficient implementability claims. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Source construction credit: Cao Yifan, Dillon Amburgey, Ali Romman, +Chris R/Clear1nsight, GamingPuzzled and the retained native/compiler lineage. +""" +import argparse +from collections import Counter, deque +from fractions import Fraction as Q +from hashlib import sha256 +import gzip +import itertools +import json +from pathlib import Path + +CANONICAL = "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz" +PROVIDER = ("research/coupled-helper-neutral-completion/capsule/workspace/" + "swarm-provider-audit-sol-high-20261024/repository/research/" + "native-rank8-helper-provider/WORD.json.gz") +PINS = { + CANONICAL: "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05", + PROVIDER: "7dc356001ed597ad6fc9fd3e0bc6ff7e3ec3a580a579a956827aa17fccfdd2dc", +} +START, STOP = 9044, 9116 +FIELDS = [19, 40, 288, 289, 295, 299, 300, 301] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def reject(operation, label): + try: + operation() + except ValueError: + return label + raise ValueError("negative control unexpectedly accepted: " + label) + + +def span(vectors): + result = {0} + for v in vectors: + result |= {x ^ v for x in result} + return frozenset(result) + + +def dimension(space): + need(len(space) and len(space) & (len(space) - 1) == 0, "power-of-two subspace size") + return len(space).bit_length() - 1 + + +def frame_state(program, canonical, stop): + current = {("L", i): f for i, f in enumerate(canonical["start"])} + current[("C", 0)] = None + for event in program[:stop]: + if event[0] == "climb": + _, _, i, a, b, _ = event + need(current[("L", i)] == a, "chronological climb entrance") + current[("L", i)] = b + elif event[0] == "warp": + _, field, _, a, b = event + need(current[tuple(field)] == a, "chronological warp entrance") + current[tuple(field)] = b + elif event[0] == "center": + _, i, a, b, _ = event + need(current[("C", i)] == a, "chronological centre entrance") + current[("C", i)] = b + elif event[0] == "scalar": + operation, f = event[1:] + if operation[0] == "clear": + current[tuple(operation[1])] = f + return current + + +def participants(event): + if event[0] == "scalar": + return {tuple(x) for x in event[1][1:] if isinstance(x, list)} + if event[0] == "climb": + return {("L", event[2])} + if event[0] == "warp": + return {tuple(event[1])} + if event[0] == "center": + return {("C", event[1])} + return set() + + +def closed_fields(program, stop=STOP): + selected = {("L", i) for i in (19, 300, 301)} + while True: + enlarged = selected | set().union(*(participants(e) for e in program[START:stop] + if selected & participants(e))) + if enlarged == selected: + break + selected = enlarged + need(all(kind == "L" for kind, _ in selected), "no owned centre/scratch inside closure") + return sorted(i for _, i in selected) + + +def invertible_prefix(program): + """Audit the prefix grammar; native climb/warp invertibility is inherited.""" + for event in program[:START]: + need(event[0] in ("scalar", "warp", "climb", "phase", "adapter", "residual_adapter"), + "prefix has only invertible persistent operations and annotations") + if event[0] == "scalar": + op = event[1] + need(op[0] in ("add", "scale") and op[1][0] == "L", + "prefix has no destructive scalar operation") + if op[0] == "add": + need(op[2][0] == "L" and op[1] != op[2] and op[4] != 0, + "prefix has only invertible ADDs") + else: + need(op[2] != 0 and op[3] != 0, "prefix has only nonzero SCALEs") + elif event[0] == "warp": + need(event[1][0] == "L", "prefix has only persistent warp targets") + + +def extract(program, canonical): + fields = closed_fields(program) + need(fields == FIELDS, "exact eight-field dependency closure") + at_start = frame_state(program, canonical, START) + current = {i: at_start[("L", i)] for i in fields} + entry = dict(current) + rows = {i: [Q(int(i == j)) for j in fields] for i in fields} + paid, events = Counter(), [] + paths = {i: [current[i]] for i in fields} + spaces = [span(x) for x in canonical["frames"]] + for index in range(START, STOP): + event = program[index] + touched = participants(event) + if not touched.intersection({("L", i) for i in fields}): + continue + need(touched <= {("L", i) for i in fields}, "closed input/output fields") + events.append([index, event]) + if event[0] == "climb": + _, _, i, a, b, r = event + need(current[i] == a and spaces[a] < spaces[b], "strict nested local climb") + need(r == dimension(spaces[b]) - dimension(spaces[a]), "exact paid climb rank") + current[i] = b + paths[i].append(b) + paid[r] += 1 + elif event[0] == "scalar": + operation, f = event[1:] + need(operation[0] in ("add", "scale"), "only reversible ADD/scale in local block") + target = operation[1][1] + need(current[target] == f, "receiver is at scalar frame") + if operation[0] == "add": + source = operation[2][1] + need(current[source] == f and source != target, "co-framed distinct ADD fields") + q = Q(operation[3], operation[4]) + rows[target] = [a + q * b for a, b in zip(rows[target], rows[source])] + else: + q = Q(operation[2], operation[3]) + need(q != 0, "invertible scale") + rows[target] = [q * a for a in rows[target]] + else: + raise ValueError("no warp/centre/retag admitted inside local block") + need(paid == {1: 10}, "retained local ten-H1 invoice") + return {"fields": fields, "entry": entry, "exit": current, "matrix": [rows[i] for i in fields], + "paths": paths, "events": events, "paid": paid} + + +def rank(matrix): + rows = [list(row) for row in matrix] + count = 0 + for j in range(len(rows[0]) if rows else 0): + pivot = next((i for i in range(count, len(rows)) if rows[i][j]), None) + if pivot is None: + continue + rows[count], rows[pivot] = rows[pivot], rows[count] + value = rows[count][j] + rows[count] = [a / value for a in rows[count]] + for i in range(len(rows)): + if i != count: + value = rows[i][j] + rows[i] = [a - value * b for a, b in zip(rows[i], rows[count])] + count += 1 + return count + + +def interval_spaces(a, b): + need(a <= b and dimension(b) <= 2, "bounded rank-two frame interval") + found, todo = {a}, [a] + while todo: + current = todo.pop() + for x in sorted(b - current): + nxt = span([*current, x]) + if nxt not in found: + found.add(nxt) + todo.append(nxt) + need(b in found and all(a <= u <= b for u in found), "complete subspace interval endpoints") + return sorted(found, key=lambda u: (len(u), tuple(sorted(u)))) + + +def all_paths(a, b): + choices = interval_spaces(a, b) + + def descend(u): + if u == b: + return [(u,)] + return [(u,) + path for v in choices if u < v for path in descend(v)] + return descend(a) + + +def label(space): + return ",".join(map(str, sorted(space))) + + +def rank_cut(paths, inputs, outputs): + """Exact max-flow bound for unrestricted linear mixing at frame stations. + + Each ascending field edge transports one arbitrary data column. Co-framed + fields may mix without restrictions, including time order and invertibility; + relaxing these constraints can only increase the possible transfer rank. + """ + source, sink = "SOURCE", "SINK" + capacities = Counter() + for path in paths.values(): + for a, b in zip(path, path[1:]): + need(a < b, "acyclic strictly ascending station edge") + capacities[(label(a), label(b))] += 1 + for field in inputs: + capacities[(source, label(paths[field][0]))] += 1 + for field in outputs: + capacities[(label(paths[field][-1]), sink)] += 1 + residual = Counter(capacities) + neighbors = {} + for a, b in capacities: + neighbors.setdefault(a, set()).add(b) + neighbors.setdefault(b, set()).add(a) + flow = 0 + while True: + previous = {source: None} + todo = deque([source]) + while todo and sink not in previous: + a = todo.popleft() + for b in sorted(neighbors.get(a, set())): + if b not in previous and residual[(a, b)] > 0: + previous[b] = a + todo.append(b) + if sink not in previous: + reachable = set(previous) + break + path, b = [], sink + while b != source: + a = previous[b] + path.append((a, b)) + b = a + amount = min(residual[e] for e in path) + for a, b in path: + residual[(a, b)] -= amount + residual[(b, a)] += amount + flow += amount + cut = [(a, b, c) for (a, b), c in sorted(capacities.items()) if a in reachable and b not in reachable] + need(sum(c for _, _, c in cut) == flow, "independently summed exact min-cut capacity") + return {"capacity": flow, "source_side": sorted(reachable), "cut_edges": cut} + + +def minor(block, inputs, outputs): + indices = {field: k for k, field in enumerate(block["fields"])} + return [[block["matrix"][indices[o]][indices[i]] for i in inputs] for o in outputs] + + +def evaluate(block, direction, spaces): + options = {i: all_paths(spaces[block["entry"][i]], spaces[block["exit"][i]]) for i in FIELDS} + need({i: len(p) for i, p in options.items()} == {i: (4 if i in (300, 301) else 1) for i in FIELDS}, + "exhaustive sixteen trajectory assignments") + rejected, neutral = [], [] + for selections in itertools.product(*(options[i] for i in FIELDS)): + paths = dict(zip(FIELDS, selections)) + profile = Counter(dimension(b) - dimension(a) for path in paths.values() for a, b in zip(path, path[1:])) + need(sum(r * c for r, c in profile.items()) == 10, "fixed boundary rank mass") + collapsed = [i for i in (300, 301) if len(paths[i]) == 2] + if not collapsed: + neutral.append(paths) + continue + # These two-column minors survive arbitrary pre-basis changes at frame0. + chosen = collapsed[0] + inputs = [300, 301] if direction == "backward" else [19] + outputs = ([19, 301] if chosen == 300 else [19, 300]) if direction == "backward" else [chosen] + desired = minor(block, inputs, outputs) + desired_rank = rank(desired) + cut = rank_cut(paths, inputs, outputs) + need(desired_rank > cut["capacity"], "every saving assignment violates necessary transfer-rank cut") + rejected.append({"collapsed_helpers": collapsed, + "helper_paths": {str(i): [sorted(u) for u in paths[i]] for i in (300, 301)}, + "paid_profile": dict(profile), "input_fields": inputs, "output_fields": outputs, + "required_minor": [[str(x) for x in row] for row in desired], + "required_rank": desired_rank, "rank_cut": cut}) + need(len(rejected) == 7 and len(neutral) == 9, "seven improving and nine neutral trajectories") + return rejected, neutral + + +def run(root): + raw = {} + for path, expected in PINS.items(): + raw[path] = (root / path).read_bytes() + need(sha256(raw[path]).hexdigest() == expected, "exact source hash: " + path) + canonical_payload, provider_payload = (gzip.decompress(raw[p]) for p in (CANONICAL, PROVIDER)) + word, provider = json.loads(canonical_payload), json.loads(provider_payload) + need(provider["source_sha256"] == sha256(canonical_payload).hexdigest(), "provider source binds canonical decompressed payload") + need(provider["direction"] == "backward", "selected provider direction") + invertible_prefix(provider["word"]) + need(provider["word"][START:STOP] == word["programs"]["backward"][START:STOP], + "selected provider local tape equals inherited backward local tape") + canonical = word["canonical"] + spaces = [span(b) for b in canonical["frames"]] + backward = extract(provider["word"], canonical) + forward = extract(word["programs"]["forward"], canonical) + need(backward["entry"] == forward["entry"] and backward["exit"] == forward["exit"], + "same eight-field endpoint frame contract in both orientations") + need(rank(backward["matrix"]) == rank(forward["matrix"]) == 8, "invertible exact eight-field transfer") + back_rejected, _ = evaluate(backward, "backward", spaces) + forward_rejected, _ = evaluate(forward, "forward", spaces) + original_paths = {i: tuple(spaces[f] for f in backward["paths"][i]) for i in FIELDS} + controls = [] + controls.append(reject(lambda: invertible_prefix([["scalar", ["scale", ["L", 0], 0, 1], 0]]), + "zero-prefix-scale-rejected")) + for helper, outputs in ((300, [19, 301]), (301, [19, 300])): + broken_paths = dict(original_paths) + broken_paths[helper] = (original_paths[helper][0], original_paths[helper][-1]) + need(rank_cut(broken_paths, [300, 301], outputs)["capacity"] == 1, + "deleting the line21 visit loses a transfer channel") + repaired_paths = dict(broken_paths) + repaired_paths[helper] = original_paths[helper] + cut = rank_cut(repaired_paths, [300, 301], outputs) + need(cut["capacity"] == rank(minor(backward, [300, 301], outputs)) == 2, + "restored original line21 path admits necessary rank-two flow") + controls.append("restore-helper-" + str(helper) + "-line21-rank-flow-admitted") + changed = [list(row) for row in minor(backward, [300, 301], [19, 301])] + need(changed == [[Q(0), Q(1)], [Q(-1), Q(-1)]], "named determinant-one target minor") + changed[0][1] = Q(0) + broken_paths = dict(original_paths) + broken_paths[300] = (original_paths[300][0], original_paths[300][-1]) + need(rank(changed) == rank_cut(broken_paths, [300, 301], [19, 301])["capacity"] == 1, + "deleted target coefficient removes this necessary-rank contradiction") + controls.append(reject(lambda: need(rank(changed) == 2, "required minor rank changed"), "delete-required-b-coefficient-destroys-obstruction")) + controls.append(reject(lambda: need(sha256(raw[PROVIDER] + b"x").hexdigest() == PINS[PROVIDER], "changed source"), "changed-provider-source-rejected")) + # Full closure restoration occurs well before the first protected cache copy. + cache = [(i, e) for i, e in enumerate(provider["word"]) if e[0] == "scalar" and e[1][0] == "copy" and e[1][1][0] == "C"] + first_later = next(i for i, _ in cache if i >= STOP) + need(first_later == 11207 and not any(START <= i < STOP for i, _ in cache), "protected cache checkpoint untouched") + protected_copies = [[i, e] for i, e in cache if e[1][1][1] in range(1, 9)] + zero_retags = [[i, e] for i, e in enumerate(provider["word"]) if e[0] == "zero_retag"] + need(len(protected_copies) == 8 and sorted(e[1][1][1] for _, e in protected_copies) == list(range(1, 9)), + "eight protected cached centres") + need(len(zero_retags) == 8 and all(i >= STOP for i, _ in zero_retags), "eight later zero-retags outside block") + next_fields = closed_fields(provider["word"], 9137) + need(len(next_fields) == 20, "larger next closure has twenty fields") + def record(block): + return {"entry_frames": block["entry"], "exit_frames": block["exit"], + "matrix": [[str(x) for x in row] for row in block["matrix"]], + "paid_profile": dict(block["paid"]), "retained_paths": block["paths"], + "local_events": block["events"]} + return {"status": "PASS_EIGHT_FIELD_MONOTONE_ADD_FLOOR_NO_NEW_KAPPA", "schema_version": 1, + "block": {"start": START, "stop": STOP, "indexing": "zero-based half-open", "fields": FIELDS}, + "source_inputs": [{"path": p, "sha256": h, "decompressed_sha256": sha256(gzip.decompress(raw[p])).hexdigest()} for p, h in PINS.items()], + "selected_backward": record(backward), "inherited_forward": record(forward), + "prefix_events_checked_for_invertible_grammar": START, + "frame_bases": {str(f): canonical["frames"][f] + for f in sorted(set(backward["entry"].values()) | set(backward["exit"].values()))}, + "next_closure_not_optimized": {"interval": [START, 9137], "fields": next_fields}, + "complete_trajectory_assignments_per_orientation": 16, + "cost_saving_trajectories_rejected_per_orientation": 7, + "neutral_trajectories_not_claimed_feasible": 9, + "backward_obstructions": back_rejected, "forward_obstructions": forward_rejected, + "moment_exponent_interval": "0