Owned-centre wire floor on #4470: retiming the C wire cannot lower the centre charge (answers #4534's retiming question; no new κ)

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.

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.

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"
+}

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"
+    }
+  ]
+}