From acca579e01a32f205c88714a1dfc82df7cd1676e Mon Sep 17 00:00:00 2001 From: Matarener Date: Fri, 23 Oct 2026 10:36:32 +0300 Subject: [PATCH] Add owned-centre wire floor on #4470 (answers #4534 retiming question; no new kappa) Co-Authored-By: Claude Opus 5.5 (1M context) --- research/owned-centre-wire-floor/PROOF.md | 35 ++ research/owned-centre-wire-floor/README.md | 33 ++ research/owned-centre-wire-floor/RESULT.json | 160 ++++++ research/owned-centre-wire-floor/SOURCES.json | 84 ++++ research/owned-centre-wire-floor/TASK.json | 72 +++ research/owned-centre-wire-floor/VERIFY.json | 28 ++ .../owned-centre-wire-floor/search/SEARCH.md | 12 + .../search/cwire_joint.py | 459 ++++++++++++++++++ research/owned-centre-wire-floor/verify.py | 336 +++++++++++++ 9 files changed, 1219 insertions(+) create mode 100644 research/owned-centre-wire-floor/PROOF.md create mode 100644 research/owned-centre-wire-floor/README.md create mode 100644 research/owned-centre-wire-floor/RESULT.json create mode 100644 research/owned-centre-wire-floor/SOURCES.json create mode 100644 research/owned-centre-wire-floor/TASK.json create mode 100644 research/owned-centre-wire-floor/VERIFY.json create mode 100644 research/owned-centre-wire-floor/search/SEARCH.md create mode 100644 research/owned-centre-wire-floor/search/cwire_joint.py create mode 100644 research/owned-centre-wire-floor/verify.py diff --git a/research/owned-centre-wire-floor/PROOF.md b/research/owned-centre-wire-floor/PROOF.md new file mode 100644 index 0000000000..e6033ac5dd --- /dev/null +++ b/research/owned-centre-wire-floor/PROOF.md @@ -0,0 +1,35 @@ +# Floor for the owned-centre wire of #4470 + +## Setting + +Frames are subspaces of F_2^9; a register in frame U is physically in the chart of U. As in `native.synthesize`, the chronological scalar word, every coefficient, every native warp (with its fixed input and output frames) and every helper entrance and exit stay fixed. A persistent L role may change frame only by a nested ascent U ⊂ V, priced at rank dim V − dim U. Following #4534's owned-wire retiming theorem (`research/frame-aware-native/OWNED-C-RETIMING.md`), the frame of every scalar contact, including every contact of the owned register C, may be retimed. Every C transition must be paid. Here C may move along nested frames in either direction, priced |dim V − dim U|. The original centre transport is such a move (frame of dimension 8 to frame 0 forward, the reverse backward). After CLEAR, the frame of C is free. A two-register contact needs both registers in one common frame. + +Non-nested C transitions (a general Clifford transport priced by its actual Fourier rank) are outside this model. + +## Lemma 1 (interval propagation) + +Process the word forward. Start each L role at its start frame, take the join of the participants' running bounds at every scalar contact, and reset at each warp output. The result is a frame Low(i) contained in the chart of contact i under every legal retiming. Process the word backward, take the meet of running bounds, and reset at warp inputs and final frames. The result is a frame Up(i) containing that chart. + +*Proof.* Along an L role, frames only ascend between contacts and warps. A contact's chart therefore contains the role's chart at its previous contact, or the fixed output frame of its previous warp, or its start frame. It is contained in the role's next chart, next warp input or final frame. Both participants of a contact share its chart. Induction over the chronology gives both claims. ∎ + +`verify.py` checks Low(i) ⊆ Up(i) at every contact in both orientations, and that every warp input and final frame lies above its running lower bound. + +## Lemma 2 (path bound) + +For nested moves g_0 → g_1 → … → g_n with move cost |dim g_j − dim g_{j+1}|, the total cost is at least dim g_0 − dim(g_0 ∩ g_1 ∩ … ∩ g_n). + +*Proof.* Let I_k = g_0 ∩ … ∩ g_k. Then I_k/(I_k ∩ g_{k+1}) injects into g_k/(g_k ∩ g_{k+1}). So dim I_k − dim I_{k+1} ≤ dim g_k − dim(g_k ∩ g_{k+1}), and the right side is at most the cost of a nested move between g_k and g_{k+1}. Sum over k. ∎ + +Moreover, if A ⊆ g_0 then dim g_0 − dim(g_0 ∩ X) ≥ dim A − dim(A ∩ X), because A/(A ∩ X) injects into g_0/(g_0 ∩ X). + +## Theorem + +In every one of the 8 centre blocks of #4470, in both orientations, the owned C wire pays rank mass at least 8 under every retiming in this model. Its moment is therefore at least 8^t for 0 < t ≤ 1, which is the current charge of one rank-8 job. + +*Proof.* In a block, the C wire visits the source contact (forward COPY, or its dual ADD) and the 22 target contacts in some chronological order. Its frames there satisfy g_src ⊇ Low(src) and g_i ⊆ Up(t_i). Forward, the path starts at g_src. Backward, it ends there, and reversing a path leaves its cost unchanged. By Lemma 2 and the remark after it, the cost is at least dim Low(src) − dim(Low(src) ∩ Up(t_1) ∩ … ∩ Up(t_22)). `verify.py` computes dim Low(src) = 8 and a zero intersection in all 16 cases. Splitting a mass of 8 into several jobs only raises the moment, because r^t is subadditive. ∎ + +The joint intersection is essential. For any single target, dim(Low(src) ∩ Up(t_i)) is 1 or 2, so a one-target bound gives only 7. A nonzero line of Low(src) lies in Up(t_i) for at most 8 of the 22 targets. + +## Consequence for #4534's rejected candidate + +The candidate replaces, in each of the 18 full calls, 56 rank-1 and 56 rank-4 paid jobs by 56 rank-5 jobs, with unchanged rank mass. On #4470's complete invoice (`research/joint-helper-lattice/RESULT.json`) its certified raw root is 0.0030511780, against the baseline 0.0030201659 (+1.03%). Adding 0.42 rank-1 C jobs per full call keeps the root above the baseline; adding 0.43 drops it below. A net extra C charge of half a rank unit per call removes the gain. By the theorem, the C wire cannot give back any mass to pay for it. Any such shape gain must come entirely from L-side merges with an unchanged C wire. The search in `search/` found none. diff --git a/research/owned-centre-wire-floor/README.md b/research/owned-centre-wire-floor/README.md new file mode 100644 index 0000000000..ffd10d3c43 --- /dev/null +++ b/research/owned-centre-wire-floor/README.md @@ -0,0 +1,33 @@ +# Owned-centre wire floor on #4470 (no new κ) + +This package gives a negative answer to the open question of #4534 (`research/frame-aware-native`) for #4470's selected native word. Retiming the owned C wire, which #4534's theorem allows when every C transition is paid, cannot make the eight rank-8 centre transports cheaper. It also cannot fund #4534's rejected rank-5 merge candidate. + +**Claim type:** a written floor with an exact finite check, plus search evidence. **No new κ.** + +## Results + +- **Floor.** Every scalar contact may be retimed: L roles climb along nested frames, and C moves along nested frames in either direction. Under these rules the C wire of each of the 8 centre blocks pays rank mass at least 8, in both orientations. That equals the current single rank-8 job, so the centre charge of #4470 is already optimal in this model. The proof (`PROOF.md`) combines interval propagation of the lowest and highest legal chart of every contact with the path bound "cost ≥ dim g_0 − dim(g_0 ∩ … ∩ g_n)" for nested moves. In every block, the source contact is forced into a frame of dimension 8, and the 22 targets' upper frames meet that frame only in 0. A single target alone would give only 7, and at most 8 of the 22 targets share any nonzero line. +- **Rejected candidate.** #4534's candidate replaces 56 rank-1 + 56 rank-4 jobs by 56 rank-5 jobs per full call. On #4470's complete invoice it nominally raises the raw root from 0.0030201659 to 0.0030511780 (+1.03%). A net extra C charge between 0.42 and 0.43 rank-1 jobs per full call cancels that gain (certified roots). By the floor, the C wire has nothing to give back. +- **Search.** A joint retiming search with the C wire as a variable (`search/`) covers all units, adjacent pairs and connected triples in two unit models, plus about 3.5 M annealing steps. It finds no improving move. + +## Verification + +```sh +python3.12 -B scripts/research_package.py --package research/owned-centre-wire-floor --check-only +python3.12 -B scripts/research_package.py --package research/owned-centre-wire-floor +``` + +`verify.py` uses only the standard library and takes about 10 s. It rebuilds #4470's word with `research/joint-helper-lattice/native_joint.py` and recovers the local paid profile `{1:2237,2:388,3:494,4:147,5:36,8:8}` from contact charts in both orientations. It then checks the centre structure (8 blocks, 22 targets, one rank-8 transport each), the propagation and the floor in all 16 block-orientations, and certified roots of the candidate variants with `mixed_target_probe`'s interval series. The controls are the weaker single-target bound (7), the 8-of-22 line count, a corrupted frame that propagation must reject, and one extra rank-8 transport per call lowering the root. It also checks that `RESULT.json` is reproduced exactly. + +## Scope + +The floor is for nested transports, the fixed chronological scalar word, fixed warps and fixed helper boundaries. A non-nested C transition priced by its actual Clifford rank, a changed scalar order or warp word, and joint changes of helper entrances and exits are not covered and stay open. The search is evidence only. The floor does not depend on it. + +## Open next questions + +1. Can a non-nested owned-C transition, priced by its exact Clifford rank, beat the nested floor of 8 per block? Start by enumerating C charts outside the nested lattice between Low(source) and the targets' Up frames, then lower those transports exactly. +2. Can helper entrances and exits move jointly with the C-contact charts? #4470's own gain came from moving helper boundaries jointly. Add them as variables to `search/cwire_joint.py`, with whole-job productive credit. + +## Credit + +Dugongue's #4534 owned-C retiming theorem and its rejected candidate. Cinna Davis's #4470 / #4440 / #4441 / #4447 native word and invoice, with zxv's native supplier and the scalar, Clifford, geometry and outer-ledger lineage retained there. The interval engine comes from `research/kappa-rebuild/architecture/mixed_target_probe.py`. Prepared by Matarener with substantial Claude Code assistance. Apache-2.0. diff --git a/research/owned-centre-wire-floor/RESULT.json b/research/owned-centre-wire-floor/RESULT.json new file mode 100644 index 0000000000..c524080777 --- /dev/null +++ b/research/owned-centre-wire-floor/RESULT.json @@ -0,0 +1,160 @@ +{ + "candidate": { + "baseline_plus_one_rank8_per_call": [ + "28338214522200519531/11605989609380000000000", + "28338215682799480469/11605989609380000000000", + 0.0024416887724332858 + ], + "baseline_root": [ + "115326305490728981823/38185420363540000000000", + "115326309309271018177/38185420363540000000000", + 0.0030201659270155433 + ], + "break_even_extra_rank1_C_jobs_per_full_call": "(0.42, 0.43)", + "nominal_candidate_root": [ + "28183978333145943023/9237081139540000000000", + "28183979256854056977/9237081139540000000000", + 0.0030511779540944345 + ], + "nominal_gain_percent": 1.0268, + "with_0.42_rank1_per_call": [ + "293779863506577850159/97268442996820000000000", + "293779873233422149841/97268442996820000000000", + 0.0030202998470550456 + ], + "with_0.43_rank1_per_call": [ + "486051221971634267523/160967314649540000000000", + "486051238068365732477/160967314649540000000000", + 0.00301956470498294 + ] + }, + "centre_floor": { + "backward": [ + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + } + ], + "forward": [ + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + }, + { + "dim_low_and_all_target_ups": 0, + "dim_low_source": 8, + "joint_floor": 8, + "max_targets_sharing_a_line": 8, + "single_target_bound": 7 + } + ] + }, + "centre_floor_summary": "every one of 8 blocks in both orientations: C mass >= 8 under any retiming of all scalar contacts; current charge 8 (one rank-8 job) is optimal", + "model": "nested transports; L ascending only; owned C either way; chronology, coefficients, warps and helper boundaries fixed", + "paid_profile_both_orientations": { + "1": 2237, + "2": 388, + "3": 494, + "4": 147, + "5": 36, + "8": 8 + }, + "status": "PASS_OWNED_CENTRE_WIRE_FLOOR" +} diff --git a/research/owned-centre-wire-floor/SOURCES.json b/research/owned-centre-wire-floor/SOURCES.json new file mode 100644 index 0000000000..00589b3a11 --- /dev/null +++ b/research/owned-centre-wire-floor/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/frame-aware-native/OWNED-C-RETIMING.md", + "usage": "provenance", + "git_blob": "b12b34ae8d993b3a543d24107d5adec60975fec7", + "sha256": "82aa5be0e6f81fa74a52935c621e49347486908ab7c9e6d2bb7958827e257111" + }, + { + "path": "research/frame-aware-native/README.md", + "usage": "provenance", + "git_blob": "ab56b99a88a35dab0af5bd2d8dec89494cf12296", + "sha256": "151408fa9db6802fae2d80d6d7bee7053c21c76249fc4da9b6c2b4ab5574f78a" + }, + { + "path": "research/fresh-helper-boundary/CHANGES.json", + "usage": "input", + "git_blob": "45744fedd0e28967aa72586048b8bc0c72f419a9", + "sha256": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624" + }, + { + "path": "research/fresh-helper-boundary/native.py", + "usage": "input", + "git_blob": "1b36f6cb5f205c33bf48811e0b1b3621c55e8154", + "sha256": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29" + }, + { + "path": "research/joint-helper-lattice/PATCH.json", + "usage": "input", + "git_blob": "51304a6601061ed4e698f910b09135ef109555e3", + "sha256": "296d0e8c58cc70febe042c681ef30d6bb469818c0835fbcaac8aa8d330f5b727" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/joint-helper-lattice/native_joint.py", + "usage": "input", + "git_blob": "0315f80e2fdef5e0eef13e3e9b8f72066238164d", + "sha256": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "usage": "input", + "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "usage": "input", + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39" + }, + { + "path": "research/missing-join-frame/PATCH.json", + "usage": "input", + "git_blob": "f96d295d40014d4dd503f58eb3cdabcbb4b8e101", + "sha256": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e" + } + ] +} diff --git a/research/owned-centre-wire-floor/TASK.json b/research/owned-centre-wire-floor/TASK.json new file mode 100644 index 0000000000..6dfa99fa28 --- /dev/null +++ b/research/owned-centre-wire-floor/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Answer #4534's open owned-response question for #4470's native word: whether retiming the owned C wire (every C edge paid, nested transports) can lower the centre charge or fund #4534's rejected rank-5 merge candidate.", + "scope_change_reason": "The card asks for a new helper inventory; this package builds none. It closes the one new degree of freedom (owned-C retiming) that #4534 added to the fixed-inventory search space.", + "bottleneck_link": "The eight rank-8 owned-centre jobs are 0.5% of the paid moment but the only C-side freedom #4534 opened; their charge is optimal in this model, and the +1.03% shape candidate dies at a net C charge of 0.43 rank-1 jobs per full call.", + "budget_minutes": 240, + "stop_rule": "Stop after the floor, the candidate break-even and a bounded joint search; no new supplier is constructed.", + "outcome": "negative-result", + "evidence": "verify.py (standard library, about 10 s) and RESULT.json; PROOF.md; search/SEARCH.md with the search script.", + "author": "Matarener (Mark), with Claude Code assistance", + "ai_assistance": "Substantial Claude Code assistance in analysis, code and writing; exact finite checks; no independent human review.", + "open_questions": [ + { + "question": "Can a non-nested owned-C transition, priced by its exact Clifford rank, beat the nested floor of 8 per centre block?", + "why_it_matters": "It is the only part of #4534's retiming theorem not covered by this floor.", + "first_step": "For each block, enumerate C charts outside the nested lattice between Low(source) and the targets' Up frames and lower the transports exactly.", + "blocked_by": "Exact Fourier-rank lowering of non-nested transports." + }, + { + "question": "Does a joint change of helper entrances/exits and C-contact charts help?", + "why_it_matters": "#4470 gained by moving helper boundaries jointly with contact frames; this package keeps helper boundaries fixed.", + "first_step": "Add helper boundaries as variables to search/cwire_joint.py with whole-job productive credit.", + "blocked_by": "Nonlinear productive-credit objective." + } + ] +} diff --git a/research/owned-centre-wire-floor/VERIFY.json b/research/owned-centre-wire-floor/VERIFY.json new file mode 100644 index 0000000000..d255f59a59 --- /dev/null +++ b/research/owned-centre-wire-floor/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/fresh-helper-boundary/CHANGES.json", + "research/fresh-helper-boundary/native.py", + "research/joint-helper-lattice/PATCH.json", + "research/joint-helper-lattice/RESULT.json", + "research/joint-helper-lattice/native_joint.py", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/missing-join-frame/PATCH.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Rebuild the #4470 native word and its local paid profile in both orientations; 8 centre blocks x 22 targets; interval propagation of legal contact charts; owned-C mass floor 8 in all 16 block-orientations (controls: single-target bound 7, at most 8 of 22 targets share a line, corrupted frame rejected); certified raw roots of #4534's rejected candidate (+1.03% nominal) with break-even C charge between 0.42 and 0.43 rank-1 jobs per full call; one extra rank-8 transport per call lowers the root; RESULT.json reproduced exactly." + } + ] +} diff --git a/research/owned-centre-wire-floor/search/SEARCH.md b/research/owned-centre-wire-floor/search/SEARCH.md new file mode 100644 index 0000000000..9ab9251a65 --- /dev/null +++ b/research/owned-centre-wire-floor/search/SEARCH.md @@ -0,0 +1,12 @@ +# Joint retiming search with a movable owned-C wire (evidence only) + +`cwire_joint.py` extends the earlier joint frame-retiming model: every scalar contact that touches C becomes a variable, and each centre block's C wire gets its own chain. Pricing is the same as in `PROOF.md`. L roles may only climb, and C moves along nested frames in either direction. A move is accepted only if the paid moment falls in both orientations at both t = 0.997 and t = 0.9999. The script reproduces #4470's local paid profile `{1:2237,2:388,3:494,4:147,5:36,8:8}` in both orientations before it searches. + +Units are maximal groups of variable contacts that share a frame consecutively along an L role. Two unit models were run, each for 45 minutes on one process. + +| Unit model | Units | Level 1 | Level 2 (adjacent pairs) | Level 3 (connected triples) | Annealing steps | Model improvements | +|---|---:|---:|---:|---:|---:|---:| +| C contacts glued into units | 1,012 | 1,012 | 2,871 | 91,223 | ≈1.6 M | 0 | +| every C contact its own unit (`--c-single`) | 1,210 | 1,210 | 3,320 | 103,315 | ≈1.9 M | 0 | + +The best annealing state never improved on the baseline (best gain +0.0000). With no model improvement, no exact literal replay was needed. The search is not exhaustive beyond triples, and it does not move helper entrances or exits. diff --git a/research/owned-centre-wire-floor/search/cwire_joint.py b/research/owned-centre-wire-floor/search/cwire_joint.py new file mode 100644 index 0000000000..d85fd9518a --- /dev/null +++ b/research/owned-centre-wire-floor/search/cwire_joint.py @@ -0,0 +1,459 @@ +"""Stage B: joint frame retiming WITH a movable owned-C wire, on the #4470 native word. + +Extends a joint frame-retiming search of the #4447/#4470 contact graph (which kept every C contact pinned) by #4534 lemma 3 +(OWNED-C-RETIMING.md): every scalar contact that touches C becomes a variable, and the C wire of +each centre block gets its own chain. Pricing: + * L role edges: nested ascending climb, rank = dim b - dim a (else illegal) [native.synthesize] + * C wire edges: nested in either direction, rank = |dim b - dim a| (else not considered); + the original centre is such an edge (8 -> 0 forward, 0 -> 8 backward). After CLEAR the C chart + is free, so a block's C chain starts at its first contact. + * Objective: paid moment sum r^t, at t = 0.997 and 0.9999, in EACH orientation separately; a hit + must gain in both orientations at both t (the verifier demands equal profiles in both). +Search: level 1 every unit, level 2 adjacent pairs, level 3 connected triples (exhaustive over +candidate frames), then simulated annealing. Checkpoint: run/state.json; log: progress.log. +Run from the repository root: python3.12 research/owned-centre-wire-floor/search/cwire_joint.py [--c-single] [--hours H] +(output directory: $CWIRE_OUT, default ./cwire-search-out). Search evidence only; not part of verify.py. +Prepared by Matarener with Claude Code assistance. Apache-2.0. +""" +import argparse, ctypes, json, math, os, random, sys, time +from collections import Counter, defaultdict +from itertools import combinations, product +from pathlib import Path + +ROOT = Path.cwd() +sys.path.insert(0, str(ROOT / 'research/joint-helper-lattice')) +sys.path.insert(0, str(ROOT / 'research/fresh-helper-boundary')) +import native_joint as NJ # noqa: E402 +import native as F # noqa: E402 + +OUT = Path(os.environ.get('CWIRE_OUT', 'cwire-search-out')).resolve() +RUN = OUT / 'run' +TS = (0.997, 0.9999) +EPS = 1e-9 +POW = [[r ** t if r else 0.0 for r in range(10)] for t in TS] +DIRS = ('forward', 'backward') + + +def log(msg): + line = f'{time.strftime("%Y-%m-%d %H:%M:%S")} cwireB {msg}' + print(line, flush=True) + with (OUT / 'progress.log').open('a', encoding='utf-8') as fh: + fh.write(line + '\n') + + +def save(path, obj): + tmp = path.with_suffix('.tmp') + tmp.write_text(json.dumps(obj, indent=1), encoding='utf-8') + os.replace(tmp, path) + + +def low_priority(): + if os.name == 'nt': + try: + h = ctypes.windll.kernel32.GetCurrentProcess() + ctypes.windll.kernel32.SetPriorityClass(h, 0x4000) # BELOW_NORMAL + except Exception: + pass + + +def rref(vs): + piv = {} + for x in vs: + for b, v in piv.items(): + if x >> b & 1: + x ^= v + if x: + b = x.bit_length() - 1 + for k in list(piv): + if piv[k] >> b & 1: + piv[k] ^= x + piv[b] = x + return tuple(sorted(piv.values())) + + +def points(s): + p = {0} + for x in s: + p |= {v ^ x for v in tuple(p)} + return frozenset(p) + + +def meet(a, b): + return rref(points(a) & points(b)) + + +def c_role(e): + g = e[1] + return any(isinstance(r, list) and r[0] == 'C' for r in g[1:3]) + + +class Model: + """Edges: (dir, kind, a, b) with a/b = ('k', key) variable contact or ('f', frame) fixed.""" + + def __init__(self): + c, programs, _, _, _ = NJ.construct() + self.c = c + self.frames, self.spans, self.dims, self.index, self.pts = [], [], [], {}, [] + for b in c['frames']: + self.intern(rref(b)) + self.lab = {} + self.edges = [] # (d, kind, u, v) kind 'L' or 'C' + self.base_profile = {} + for d in DIRS: + prog = programs[d] + Lkeys = F.gates(prog) + inv = {i: k for k, i in Lkeys.items()} + # C contacts: per block ordinal; forward copy <-> backward final add (L_src) + blk, cnt, cinv = -1, 0, {} + last_clear = False + for i, e in enumerate(prog): + if e[0] == 'scalar' and e[1][0] == 'clear': + if not last_clear: + blk += 1 + cnt = 0 + last_clear = True + continue + if e[0] == 'scalar' and c_role(e): + last_clear = False + L = [r[1] for r in e[1][1:3] if r[0] == 'L'][0] + cinv[i] = ('C', blk, L) + cnt += 1 + elif e[0] == 'scalar': + last_clear = False + # NB the clear-pairs: forward 'clear@0, clear@274' close/open; backward 'clear@254, clear@0' + for i, k in list(inv.items()) + list(cinv.items()): + f = prog[i][2] + if k in self.lab: + assert self.lab[k] == f, ('orientation frame mismatch', k) + self.lab[k] = f + lch = defaultdict(list) + cch = defaultdict(list) + for r, f in enumerate(c['start']): + lch[r].append(('f', f, f)) + for i, e in enumerate(prog): + if e[0] == 'scalar': + g = e[1] + roles = g[1:3] if g[0] in ('add', 'copy') else g[1:2] + k = inv.get(i) or cinv.get(i) + for r in roles: + if r[0] == 'L': + lch[r[1]].append(('k', k, k) if k else ('f', e[2], e[2])) + if i in cinv: + cch[cinv[i][1]].append(('k', cinv[i], cinv[i])) + elif e[0] == 'warp': + lch[e[1][1]].append(('f', e[3], e[4])) + for r, f in enumerate(c['final']): + lch[r].append(('f', f, f)) + for lst in lch.values(): + for x, y in zip(lst, lst[1:]): + self.edges.append((d, 'L', ('k', x[2]) if x[0] == 'k' else ('f', x[2]), + ('k', y[1]) if y[0] == 'k' else ('f', y[1]))) + for lst in cch.values(): + for x, y in zip(lst, lst[1:]): + self.edges.append((d, 'C', ('k', x[1]), ('k', y[1]))) + self.keys = sorted(self.lab, key=str) + self.inc = defaultdict(list) + for n, (d, kind, u, v) in enumerate(self.edges): + for w in (u, v): + if w[0] == 'k': + self.inc[w[1]].append(n) + self.base = dict(self.lab) + self.rk = {} + self.c_single = False + + def intern(self, s): + lab = self.index.get(s) + if lab is None: + self.frames.append(list(s)); self.spans.append(s); self.dims.append(len(s)) + self.pts.append(points(s)) + lab = self.index[s] = len(self.frames) - 1 + return lab + + def rank(self, kind, a, b): + if a == b: + return 0 + key = (kind, a, b) + r = self.rk.get(key) + if r is None: + pa, pb = self.pts[a], self.pts[b] + if pa < pb: + r = self.dims[b] - self.dims[a] + elif kind == 'C' and pb < pa: + r = self.dims[a] - self.dims[b] + else: + r = -1 + self.rk[key] = r + return None if r < 0 else r + + def fr(self, w, ov): + return w[1] if w[0] == 'f' else ov.get(w[1], self.lab[w[1]]) + + def profile(self): + prof = {d: Counter() for d in DIRS} + for d, kind, u, v in self.edges: + r = self.rank(kind, self.fr(u, {}), self.fr(v, {})) + assert r is not None, ('illegal edge in baseline', d, kind, u, v) + if r: + prof[d][r] += 1 + return prof + + def delta(self, ov): + """gain[d][t] of move ov {key: frame}; None if illegal.""" + es = set(n for k in ov for n in self.inc[k]) + gain = {d: [0.0, 0.0] for d in DIRS} + prof = {d: Counter() for d in DIRS} + for n in es: + d, kind, u, v = self.edges[n] + ro = self.rank(kind, self.fr(u, {}), self.fr(v, {})) + rn = self.rank(kind, self.fr(u, ov), self.fr(v, ov)) + if rn is None: + return None, None + for t in (0, 1): + gain[d][t] += POW[t][ro] - POW[t][rn] + if ro: + prof[d][ro] -= 1 + if rn: + prof[d][rn] += 1 + return gain, {d: {k: v for k, v in p.items() if v} for d, p in prof.items()} + + # units: consecutive equal-frame variable contacts along L chains (C chains do not glue) + def units(self): + parent = {k: k for k in self.keys} + + def find(k): + while parent[k] != k: + parent[k] = parent[parent[k]] + k = parent[k] + return k + for d, kind, u, v in self.edges: + if kind == 'L' and u[0] == v[0] == 'k' and self.lab[u[1]] == self.lab[v[1]] \ + and not (self.c_single and (u[1][0] == 'C' or v[1][0] == 'C')): + a, b = find(u[1]), find(v[1]) + if a != b: + parent[a] = b + g = defaultdict(list) + for k in self.keys: + g[find(k)].append(k) + units = sorted(g.values(), key=lambda x: str(x[0])) + uid = {k: i for i, u in enumerate(units) for k in u} + adj = [set() for _ in units] + for d, kind, u, v in self.edges: + if u[0] == v[0] == 'k': + x, y = uid[u[1]], uid[v[1]] + if x != y: + adj[x].add(y); adj[y].add(x) + return units, [sorted(s) for s in adj], uid + + +class Search: + def __init__(self, M): + self.M = M + self.units, self.adj, self.uid = M.units() + self.ulab = [M.lab[u[0]] for u in self.units] + # boundary summary per unit: (neighbour unit or -1, fixed frame or -1, out?, kind, dir, mult) + nb = [Counter() for _ in self.units] + for d, kind, u, v in M.edges: + x = self.uid[u[1]] if u[0] == 'k' else None + y = self.uid[v[1]] if v[0] == 'k' else None + if x is not None and x == y: + continue + if x is not None: + nb[x][(-1 if y is None else y, v[1] if y is None else -1, 1, kind, d)] += 1 + if y is not None: + nb[y][(-1 if x is None else x, u[1] if x is None else -1, 0, kind, d)] += 1 + self.nb = [[k + (m,) for k, m in c.items()] for c in nb] + self.di = {d: i for i, d in enumerate(DIRS)} + + def cands(self, i, S, cap): + M = self.M + lo, hi = set(), set() + for j, f, out, kind, d, m in self.nb[i]: + if j in S: + continue + lab = f if j < 0 else self.ulab[j] + if kind == 'C': + lo.add(lab); hi.add(lab) + else: + (hi if out else lo).add(lab) + lo_l = sorted(f for f in lo) + res = [self.ulab[i]] + lower = rref([x for f in lo_l for x in M.spans[f]]) + res.append(M.intern(lower)) + upper = None + for f in sorted(hi): + upper = M.spans[f] if upper is None else meet(upper, M.spans[f]) + if upper is not None: + res.append(M.intern(upper)) + g = lower + for x in upper: + h = rref(g + (x,)) + if len(h) > len(g) and points(h) <= points(upper): + g = h + res.append(M.intern(g)) + res += sorted(lo | hi) + return list(dict.fromkeys(res))[:cap] + + def gain_of(self, assign): + """Exact gain per (dir, t) of moving units {i: frame}; None if illegal.""" + M = self.M + g = [[0.0, 0.0], [0.0, 0.0]] + for i, fnew in assign.items(): + for j, f, out, kind, d, m in self.nb[i]: + if j in assign and j < i: + continue + o = f if j < 0 else self.ulab[j] + n = f if j < 0 else assign.get(j, o) + a0, b0 = (self.ulab[i], o) if out else (o, self.ulab[i]) + a1, b1 = (fnew, n) if out else (n, fnew) + ro, rn = M.rank(kind, a0, b0), M.rank(kind, a1, b1) + if rn is None: + return None + di = self.di[d] + for t in (0, 1): + g[di][t] += m * (POW[t][ro] - POW[t][rn]) + return g + + def best(self, idx, cap): + S = set(idx) + cl = [] + for i in idx: + cs = list(self.cands(i, S, cap)) + if len(idx) > 1: + cs += [f for f in self.cands(i, {i}, cap) if f not in cs] + cl.append([f for f in cs if f != self.ulab[i]][:cap]) + if len(idx) == 2: + for a in (0, 1): + cl[a] += [f for f in cl[1 - a] if f not in cl[a] and f != self.ulab[idx[a]]] + bestv, besta = EPS, None + for combo in product(*cl): + assign = dict(zip(idx, combo)) + g = self.gain_of(assign) + if g is None: + continue + if min(g[0][0], g[0][1], g[1][0], g[1][1]) > EPS and g[0][0] + g[1][0] > bestv: + bestv, besta = g[0][0] + g[1][0], (assign, g) + return besta + + def apply(self, assign): + for i, f in assign.items(): + self.ulab[i] = f + for k in self.units[i]: + self.M.lab[k] = f + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--hours', type=float, default=1.0) + ap.add_argument('--cap', type=int, default=12) + ap.add_argument('--c-single', action='store_true', help='C contacts are their own units') + args = ap.parse_args() + low_priority() + global RUN + if args.c_single: + RUN = OUT / 'run-csingle' + OUT.mkdir(exist_ok=True) + RUN.mkdir(exist_ok=True) + st_path = RUN / 'state.json' + st = json.loads(st_path.read_text(encoding='utf-8')) if st_path.exists() else {'level': 1, 'pos': 0, 'hits': [], 'sa_step': 0} + log(f'stage B: launch (resume level {st["level"]} pos {st["pos"]}, {len(st["hits"])} hits)') + M = Model() + prof = M.profile() + log(f'stage B: baseline profile forward {dict(sorted(prof["forward"].items()))}') + log(f'stage B: baseline profile backward {dict(sorted(prof["backward"].items()))}') + want = {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8} + ok = all(dict(prof[d]) == want for d in DIRS) + log(f'stage B: self-test vs #4470 RESULT local_paid {want}: {"PASS" if ok else "FAIL"}') + if not ok: + sys.exit(1) + M.c_single = args.c_single + S = Search(M) + ncu = sum(1 for u in S.units if any(k[0] == 'C' for k in u)) + sizes = Counter(len(u) for u in S.units) + log(f'stage B: {len(S.units)} units ({ncu} contain C contacts), largest {max(sizes)}, C-wire edges {sum(1 for e in M.edges if e[1]=="C")}') + deadline = time.time() + args.hours * 3600 + for level in (1, 2, 3): + if st['level'] > level: + continue + if level == 1: + items = [(i,) for i in range(len(S.units))] + elif level == 2: + items = [(x, y) for x in range(len(S.units)) for y in S.adj[x] if x < y] + else: + items = [] + for y in range(len(S.units)): + for x, z in combinations(S.adj[y], 2): + tri = tuple(sorted((x, y, z))) + if z in S.adj[x] and y != tri[0]: + continue + items.append(tri) + cap = args.cap if level < 3 else max(6, args.cap // 2) + log(f'stage B: level {level}: {len(items)} items, cap {cap}') + t_log = time.time() + for n in range(st['pos'], len(items)): + h = S.best(list(items[n]), cap) + if h: + assign, g = h + rec = {'level': level, 'units': list(items[n]), 'sizes': [len(S.units[i]) for i in items[n]], + 'has_C': [any(k[0] == 'C' for k in S.units[i]) for i in items[n]], + 'frames': [[S.ulab[i], M.dims[S.ulab[i]], f, M.dims[f]] for i, f in assign.items()], + 'gain': g} + st['hits'].append(rec) + log(f'stage B: MODEL HIT level {level} {rec}') + if time.time() - t_log > 60: + st['level'], st['pos'] = level, n + save(st_path, st) + log(f'stage B: level {level}: {n}/{len(items)} ({100*n/len(items):.1f}%), hits {len(st["hits"])}') + t_log = time.time() + if time.time() > deadline: + st['level'], st['pos'] = level, n + save(st_path, st) + log('stage B: time budget used, state saved; rerun to continue') + return + st['level'], st['pos'] = level + 1, 0 + save(st_path, st) + log(f'stage B: level {level} done, hits so far {len(st["hits"])}') + # simulated annealing on unit moves (single / adjacent pair) + rng = random.Random(7 + st['sa_step']) + n = len(S.units) + gain = 0.0 + best_g = 0.0 + step0 = st['sa_step'] + t_log = time.time() + log('stage B: annealing start') + while time.time() < deadline: + st['sa_step'] += 1 + T = 1.0 * (0.02 / 1.0) ** (((st['sa_step'] - step0) % 200000) / 200000) + x = rng.randrange(n) + idx = [x] if rng.random() < 0.6 or not S.adj[x] else [x, rng.choice(S.adj[x])] + assign = {} + for i in idx: + f = rng.choice(S.cands(i, set(idx), 16)) + if f != S.ulab[i]: + assign[i] = f + if not assign: + continue + g = S.gain_of(assign) + if g is None: + continue + w = min(g[0][0], g[1][0]) + if w >= 0 or rng.random() < math.exp(w / T): + S.apply(assign) + gain += w + if gain > best_g + EPS: + best_g = gain + pr = M.profile() + if all(sum(v * r ** t for r, v in pr[d].items()) < sum(v * r ** t for r, v in want.items()) - EPS + for d in DIRS for t in TS): + st['hits'].append({'level': 'anneal', 'step': st['sa_step'], 'profile': {d: dict(pr[d]) for d in DIRS}, + 'changed': {str(k): M.lab[k] for k in M.keys if M.lab[k] != M.base[k]}}) + log(f'stage B: ANNEAL MODEL HIT gain {gain:+.4f}, profiles {[dict(sorted(pr[d].items())) for d in DIRS]}') + if time.time() - t_log > 300: + log(f'stage B: anneal step {st["sa_step"]}, T {T:.3f}, gain {gain:+.4f}, best {best_g:+.4f}, hits {len(st["hits"])}') + save(st_path, st) + t_log = time.time() + save(st_path, st) + log(f'stage B: finished; total model hits {len(st["hits"])}') + + +if __name__ == '__main__': + main() diff --git a/research/owned-centre-wire-floor/verify.py b/research/owned-centre-wire-floor/verify.py new file mode 100644 index 0000000000..49053e0d67 --- /dev/null +++ b/research/owned-centre-wire-floor/verify.py @@ -0,0 +1,336 @@ +#!/usr/bin/env python3 +"""Owned-centre wire floor on the #4470 native word (answers #4534's retiming question; no new kappa). + +#4534 (research/frame-aware-native, OWNED-C-RETIMING.md) allows the chart of every scalar contact, +including the owned C register, to be retimed provided every C transition is paid. This script asks +whether that freedom can make the eight rank-8 centre transports of #4470 cheaper. + +Model (as native.synthesize / joint-helper-lattice): chronological scalar order, coefficients, warps +and helper entrances/exits are fixed. A persistent L role only climbs along nested frames (rank = +dimension difference). The owned C wire may move along nested frames in either direction (rank = +|dimension difference|); the original centre is such a move (8 -> 0 forward, 0 -> 8 backward), and +after CLEAR its chart is free. Non-nested C transitions are outside this model. + +Checks: +1. Rebuild #4470's word with joint-helper-lattice/native_joint.construct and recover its complete + local paid profile {1:2237,2:388,3:494,4:147,5:36,8:8} from contact charts in both orientations. +2. Centre structure: per orientation 8 blocks, each one source contact (copy / its dual), 22 target + contacts in frame 0 and one rank-8 C transport. +3. Interval propagation over every scalar contact of every L role (any legal retiming): a forward + pass gives the lowest possible chart of each contact (join of participants' running lower bounds, + reset by warp outputs), a backward pass the highest (meet of running upper bounds, reset by warp + inputs and final frames). Every contact is consistent (low <= up). +4. Floor (PROOF.md): for a nested C path g_0 -> g_1 -> ... -> g_n the paid mass is at least + dim g_0 - dim(g_0 & g_1 & ... & g_n). With g_0 >= Low(source) and g_i <= Up(target i), and + Low(source) & Up(t_1) & ... & Up(t_22) = 0, every block pays C mass >= dim Low(source) = 8, in both + orientations; since r^t is subadditive for t < 1, its moment is >= 8^t, i.e. the current charge. + Control: the single-target bound alone only gives 7, so the joint intersection is needed. +5. #4534's rejected candidate (56 rank-1 + 56 rank-4 -> 56 rank-5 per full call, no C charge) on + #4470's complete invoice: certified raw roots of the baseline, the nominal candidate, and the + candidate with 0.42 resp. 0.43 extra rank-1 C jobs per full call (break-even between them). +Standard library only. Prepared by Matarener with Claude Code assistance. Apache-2.0. +""" +from collections import Counter, defaultdict +from fractions import Fraction as Q +from pathlib import Path +import importlib.util +import json +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(ROOT / 'research/joint-helper-lattice')) +sys.path.insert(0, str(ROOT / 'research/fresh-helper-boundary')) +DIRS = ('forward', 'backward') +WANT = {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8} + + +def need(ok, why): + if not ok: + raise SystemExit('FAIL: ' + why) + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +# ---------------------------------------------------------------- subspaces of F_2^9 as point sets +def points(basis): + out = {0} + for x in basis: + out |= {v ^ x for v in tuple(out)} + return frozenset(out) + + +def dim(p): + return len(p).bit_length() - 1 + + +def join(a, b): + if b <= a: + return a + if a <= b: + return b + out = set(a) + for x in b: + if x not in out: + out |= {v ^ x for v in tuple(out)} + return frozenset(out) + + +ALL = frozenset(range(512)) + + +def c_contact(e): + return e[0] == 'scalar' and any(isinstance(r, list) and r[0] == 'C' for r in e[1][1:3]) + + +def l_roles(e): + g = e[1] + roles = g[1:3] if g[0] in ('add', 'copy') else g[1:2] + return [r[1] for r in roles if r[0] == 'L'] + + +def blocks(prog): + """Centre blocks between CLEAR runs: (source contact index, [target contact indices]).""" + out, cur, last_clear = [], None, False + for i, e in enumerate(prog): + if e[0] == 'scalar' and e[1][0] == 'clear': + if not last_clear: + cur = {'src': None, 't': []} + out.append(cur) + last_clear = True + continue + last_clear = False + if c_contact(e): + if e[2] != 0: + need(cur['src'] is None, 'one source contact per block') + cur['src'] = i + else: + cur['t'].append(i) + return [b for b in out if b['src'] is not None or b['t']] + + +def paid_profile(c, prog, P): + """Local paid profile from contact charts: L climbs (nested up) and C moves (nested, either way).""" + prof = Counter() + cur = {r: f for r, f in enumerate(c['start'])} + + def step(a, b, two_way): + if a == b: + return + if P[a] < P[b]: + prof[dim(P[b]) - dim(P[a])] += 1 + elif two_way and P[b] < P[a]: + prof[dim(P[a]) - dim(P[b])] += 1 + else: + need(False, 'illegal transport in the rebuilt word') + cchart = None + for e in prog: + if e[0] == 'scalar': + for r in l_roles(e): + step(cur[r], e[2], False) + cur[r] = e[2] + if c_contact(e): + if e[1][0] == 'clear': + cchart = None + else: + if cchart is not None: + step(cchart, e[2], True) + cchart = e[2] + elif e[0] == 'warp': + r = e[1][1] + step(cur[r], e[3], False) + cur[r] = e[4] + for r, f in enumerate(c['final']): + step(cur[r], f, False) + return prof + + +def propagate(c, prog, P): + """Lowest / highest chart of every L-touching scalar contact over all legal retimings.""" + low, up = {}, {} + cur = {r: P[f] for r, f in enumerate(c['start'])} + for i, e in enumerate(prog): + if e[0] == 'scalar': + rs = l_roles(e) + lo = frozenset({0}) + for r in rs: + lo = join(lo, cur[r]) + for r in rs: + cur[r] = lo + low[i] = lo + elif e[0] == 'warp': + r = e[1][1] + need(cur[r] <= P[e[3]], 'warp input above every legal lower bound') + cur[r] = P[e[4]] + for r, f in enumerate(c['final']): + need(cur[r] <= P[f], 'final frame above every legal lower bound') + cur = {r: P[f] for r, f in enumerate(c['final'])} + for i in range(len(prog) - 1, -1, -1): + e = prog[i] + if e[0] == 'scalar': + rs = l_roles(e) + u = ALL + for r in rs: + u = u & cur[r] + for r in rs: + cur[r] = u + up[i] = u + elif e[0] == 'warp': + cur[e[1][1]] = P[e[3]] + return low, up + + +# ---------------------------------------------------------------- certified roots (as productive-lever-reprice) +E = load(ROOT / 'research/kappa-rebuild/architecture/mixed_target_probe.py', 'cwire_probe') +SCALE = 2**128 + + +def outward(x, upw): + n = x * SCALE + k = n.numerator // n.denominator + return Q(k + (1 if upw and k != n else 0), SCALE) + + +def h_interval(r, c): + if r in (0, 1): + return Q(r), Q(r) + a, b = E.log_interval(r) + low, _ = E.exp_interval(outward(c * a, False)) + _, high = E.exp_interval(outward(c * b, True)) + return outward(Q(r) / high, False), outward(Q(r) / low, True) + + +def moment(prof, c): + lo = hi = Q(0) + for r, n in prof.items(): + if n: + a, b = h_interval(r, c) + lo += n * (a if n >= 0 else b) + hi += n * (b if n >= 0 else a) + return lo, hi + + +def surplus(T, P, c): + a, b = moment(T, c), moment(P, c) + return a[0] - b[1], a[1] - b[0] + + +def root(T, P, width=Q(1, 10**10)): + lo, hi = 0.0, 1 / 6 + f = lambda c: sum(float(n) * r ** (1 - c) for r, n in T.items()) - sum(float(n) * r ** (1 - c) for r, n in P.items()) + for _ in range(80): + mid = (lo + hi) / 2 + lo, hi = (mid, hi) if f(mid) > 0 else (lo, mid) + guess = Q(lo).limit_denominator(10**13) + pos, neg = guess - width / 2, guess + width / 2 + need(surplus(T, P, pos)[0] > 0 and surplus(T, P, neg)[1] < 0, 'certified root bracket') + return pos, neg + + +def main(): + NJ = load(ROOT / 'research/joint-helper-lattice/native_joint.py', 'cwire_native_joint') + c, programs, _, _, _ = NJ.construct() + P = [points(b) for b in c['frames']] + result = {'status': None, 'model': 'nested transports; L ascending only; owned C either way; ' + 'chronology, coefficients, warps and helper boundaries fixed'} + + # 1. profile self-test + for d in DIRS: + prof = paid_profile(c, programs[d], P) + need(dict(prof) == WANT, f'{d} paid profile reproduces #4470: {dict(sorted(prof.items()))}') + rs = json.loads((ROOT / 'research/joint-helper-lattice/RESULT.json').read_text()) + need({int(k): v for k, v in rs['local_paid'].items()} == WANT, '#4470 RESULT local_paid') + result['paid_profile_both_orientations'] = {str(k): v for k, v in sorted(WANT.items())} + + # 2-4. centre structure and floor + floors = {} + for d in DIRS: + prog = programs[d] + bl = blocks(prog) + need(len(bl) == 8, f'{d}: eight centre blocks') + centres = [e for e in prog if e[0] == 'center'] + need(len(centres) == 8 and all(e[4] == 8 for e in centres), f'{d}: eight rank-8 centre transports') + low, up = propagate(c, prog, P) + need(all(low[i] <= up[i] for i in low), f'{d}: every contact has a legal chart interval') + rows = [] + for b in bl: + need(len(b['t']) == 22, f'{d}: 22 target contacts per block') + L = low[b['src']] + common = L + for t in b['t']: + common = common & up[t] + single = max(dim(L) - dim(L & up[t]) for t in b['t']) + share = Counter(x for t in b['t'] for x in (L & up[t]) if x) + rows.append({'dim_low_source': dim(L), 'dim_low_and_all_target_ups': dim(common), + 'single_target_bound': single, 'joint_floor': dim(L) - dim(common), + 'max_targets_sharing_a_line': max(share.values())}) + need(max(share.values()) == 8, f'{d}: at most 8 of 22 targets admit a common line') + need(dim(L) == 8 and dim(common) == 0, f'{d}: joint floor 8') + need(single == 7, f'{d}: control, single-target bound is weaker (7)') + floors[d] = rows + result['centre_floor'] = floors + result['centre_floor_summary'] = ('every one of 8 blocks in both orientations: C mass >= 8 under any ' + 'retiming of all scalar contacts; current charge 8 (one rank-8 job) is optimal') + + # negative control: the propagation rejects a word whose warp input is pushed below a forced chart + prog = [list(e) for e in programs['forward']] + zero = next(f for f, p in enumerate(P) if dim(p) == 0) + src = blocks(prog)[0]['src'] + S = l_roles(prog[src])[0] + nxt = next((i for i in range(src + 1, len(prog)) if prog[i][0] == 'warp' and prog[i][1][1] == S), None) + bad_c = json.loads(json.dumps(c)) + if nxt is None: + bad_c['final'][S] = zero + else: + prog[nxt] = list(prog[nxt]); prog[nxt][3] = zero + try: + propagate(bad_c, prog, P) + rejected = False + except SystemExit: + rejected = True + need(rejected, 'control: forcing the copy source back to frame 0 before its next warp is rejected') + + # 5. rejected #4534 candidate on the complete invoice + T = Counter({int(k): v for k, v in rs['targets'].items()}) + P0 = Counter({int(k): v for k, v in rs['paid'].items()}) + calls = rs['full_calls'] + cand = Counter(P0) + cand[1] -= 56 * calls + cand[4] -= 56 * calls + cand[5] += 56 * calls + base = root(T, P0) + nom = root(T, cand) + need(nom[0] > base[1], 'nominal candidate raises the raw root') + lo_extra, hi_extra = Q(42, 100), Q(43, 100) + c_lo = Counter(cand); c_lo[1] += lo_extra * calls + c_hi = Counter(cand); c_hi[1] += hi_extra * calls + r_lo, r_hi = root(T, c_lo), root(T, c_hi) + need(r_lo[0] > base[1] and r_hi[1] < base[0], 'break-even between 0.42 and 0.43 rank-1 C jobs per call') + c8 = Counter(P0); c8[8] += calls + r8 = root(T, c8) + need(r8[1] < base[0], 'one extra rank-8 transport per call lowers the root') + fmt = lambda b: [str(b[0]), str(b[1]), float(b[0])] + result['candidate'] = {'baseline_root': fmt(base), 'nominal_candidate_root': fmt(nom), + 'nominal_gain_percent': round(100 * (float(nom[0]) / float(base[0]) - 1), 4), + 'with_0.42_rank1_per_call': fmt(r_lo), 'with_0.43_rank1_per_call': fmt(r_hi), + 'baseline_plus_one_rank8_per_call': fmt(r8), + 'break_even_extra_rank1_C_jobs_per_full_call': '(0.42, 0.43)'} + result['status'] = 'PASS_OWNED_CENTRE_WIRE_FLOOR' + out = json.dumps(result, indent=1, sort_keys=True) + '\n' + if '--write' in sys.argv: + with open(HERE / 'RESULT.json', 'w', encoding='utf-8', newline='\n') as fh: + fh.write(out) + else: + need((HERE / 'RESULT.json').read_text(encoding='utf-8') == out, 'RESULT.json reproduced exactly') + print(json.dumps({'status': result['status'], 'candidate': result['candidate']['nominal_gain_percent']})) + + +if __name__ == '__main__': + main()