Prove the sharp fixed-line Whitehead crossing floor (no κ)

research/fixed-line-crossing-floor/PROOF.md

@@ -0,0 +1,104 @@
+# The fixed-line permutation theorem
+
+## Contract
+
+Let `V` be a finite-dimensional binary vector space and let `L_1,...,L_n`
+be distinct one-dimensional subspaces. The scalar payload space is over an
+arbitrary field `K`; the frame field and payload field need not agree.
+Register `X_i` has frame `L_i` and arbitrary independent initial payload `x_i`.
+All public register frames stay fixed. Other public registers have arbitrary
+independent initial payloads. There are no preloaded copies of any `x_i`.
+
+The circuit is finite, fixed and linear. A local operation can combine or
+scale registers only when their current frames agree. Owned registers can be
+initialized to zero at any frame and cleared at any time. Every owned MOVE
+changes a register's frame between strictly nested subspaces; its rank is the
+positive dimension difference. MOVEs carry the payload unchanged in the
+common-chart convention. Arbitrarily many carriers, feedback, intermediate
+frames, repeated visits and interleaved reads and writes are permitted.
+No control flow or scalar side channel communicates payload between frames.
+
+For a permutation `pi` and nonzero scalars `a_i`, require the checkpoint
+endpoint `X_{pi(i)} = a_i x_i`. All other public registers are restored and
+all owned registers are cleared. Let `s` be the number of indices with
+`pi(i) != i`. The checkpoint is before releasing the fixed public frames.
+
+## Theorem
+
+Every such circuit has at least `2s` owned MOVEs. A circuit with exactly `2s`
+rank-one MOVEs exists. Consequently its minimum owned MOVE tariff is `2s`
+for every tariff `c(r)` with `c(1)=1` and `c(r)>=1` for positive integer `r`.
+
+### Lower bound
+
+For a designated line `L_i`, call the set of registers whose current frame
+equals `L_i` its region. An INIT contributes zero, a CLEAR discards data,
+and local operations cannot communicate across its boundary. The only ways
+data enter or leave this region are MOVEs whose arrival or departure frame
+equals `L_i`. This statement includes every owned carrier currently there.
+
+If no MOVE ever leaves `L_i`, the coefficient of the independent input `x_i`
+remains zero in every register outside the region. This follows by induction
+on events. Local operations outside see zero coefficients; INIT is zero;
+CLEAR cannot introduce one; and every MOVE not leaving the region carries
+a zero coefficient from an outside register or remains within it. But for
+`pi(i) != i`, the endpoint outside the region contains `a_i x_i` with
+`a_i != 0`. Therefore a departure from `L_i` is required.
+
+Likewise, if no MOVE ever enters `L_i`, every register there stays independent
+of all initial `x_j` with `j != i`. The same event induction proves this,
+even if outside registers have previously received `x_i`. For a moved line,
+its final register requires `x_{pi^{-1}(i)}` from a different line, with a
+nonzero coefficient. Therefore an arrival at `L_i` is required.
+
+There are `s` departure requirements and `s` arrival requirements. A single
+MOVE can serve at most one of them. Its departure frame and arrival frame
+cannot be two different designated lines, since distinct lines are
+incomparable and every MOVE is strictly nested. Nor can both endpoints be
+the same designated line, since the inclusion is strict. Each MOVE thus
+contributes at most one item to these `2s` requirements. This proves the
+lower bound without a read-once, two-phase or independent-carrier premise.
+
+### Attainment
+
+For each moved index `i`, initialize a zero owned register `C_i` at `L_i`,
+copy `X_i` into it, and set `X_i := X_i - C_i`. These are local operations;
+now `C_i=x_i` and all moved public registers are zero. Scale any fixed-point
+register `X_i` by `a_i` locally.
+
+For each moved source `i`, put `j=pi(i)` and `H=L_i+L_j`. The two distinct
+binary lines span a plane. MOVE `C_i` from `L_i` UP to `H` and DOWN to `L_j`,
+then perform `X_j := X_j + a_i C_i` and CLEAR `C_i`. Both MOVEs have rank one.
+Every moved destination receives exactly one source. Therefore the endpoint
+is the required scaled permutation and all owned registers are cleared.
+Other public registers are untouched. There are exactly `2s` MOVEs.
+
+All scalar copying, subtraction, scaling and owned erasure are part of this
+local circuit, but only its MOVEs are counted in the stated tariff. The
+construction uses `s` owned registers; it does not claim minimum peak storage.
+
+## Application and limits
+
+PR #6939 section 1.3 specifies a perfect-matching exchange on the 104 distinct
+P104 lines before its Y bounce. Each of its X registers exchanges its x payload
+with its partner while both public frames stay fixed. Taking `s=104` proves
+an owned-MOVE floor of `208` for that preprocessing contract. The predecessor's
+two rank-one transfers per port attain it. This is an application of the new
+all-circuit lower bound, not a new construction of the predecessor's native.
+
+In particular, sharing runs, allowing more intermediate frames or tolerating
+temporary junk cannot save an owned MOVE while preserving this contract.
+Merely checking the endpoint's shadow matrix would not establish this floor;
+the separation of line regions is the additional invariant.
+
+The application does not assert that every proposed shared-landing native
+contains this checkpoint. Allowing a public register to leave its line, using
+a different endpoint, or interleaving with the later changing Y frames removes
+a hypothesis. The full common-chart versus physical phase interface, the
+complete signed invoice and every all-size framework assumption remain open.
+The checker's changed-frame control permits public descent as well as ascent.
+It demonstrates the necessity of the fixed-frame premise in this abstract
+model; it does not supply a native under monotone public-frame rules.
+For `0 <= C <= 1`, `r^(1-C)>=1` at every positive integer rank, so the tariff
+corollary applies on its stated range. Nothing is asserted for cheaper
+positive-rank tariffs.

research/fixed-line-crossing-floor/README.md

@@ -0,0 +1,97 @@
+# Exact transport cost for a fixed-line permutation
+
+For a permutation moving `s` public registers on distinct fixed lines, the
+minimum number of owned MOVEs is **`2s`**. Every MOVE can have rank one in an
+attaining schedule. Thus the minimum owned tariff is also `2s` whenever a
+rank-one MOVE costs one and every positive-rank MOVE costs at least one,
+including `r^(1-C)` for `0 <= C <= 1`.
+
+This is a **scoped written proof with exact finite corroboration**. It permits
+arbitrarily many shared owned carriers, feedback, interleaved reads and writes,
+intermediate subspaces and owned erasure. The public registers stay on their
+distinct lines throughout the exchange, and scalar gates only join registers
+on equal frames. [PROOF.md](PROOF.md) states the complete contract and proof.
+The universal result rests on that proof, not on a finite census.
+
+## Connection to the Whitehead question
+
+DreamingOfClouds's [PR #6939](https://github.com/CrocSwap/integer-mult-bounds/pull/6939)
+asks whether shared owned runs can carry the beta crossings of its window
+native more cheaply. Its existing matching exchange moves all 104 public X
+registers while they remain on distinct lines. The theorem gives an exact
+**208-MOVE floor for that exchange**, even with arbitrary carrier sharing and
+interleaving. Its rank-one exchange attains the floor. We cite that construction
+and the port count; we do not replay or claim credit for them.
+
+This closes sharing as a way to improve that fixed-line preprocessing contract.
+It does not exclude changing public frames during the exchange, mixing the
+exchange with the later Y bounce, Gamma coupling, or a different native.
+No kappa improvement, supplier admission, full physical native replay or
+complete multiplication theorem is claimed. The tariff counts owned MOVEs
+only. Scalar operations, allocation, storage and physical delivery remain
+separate costs.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/fixed-line-crossing-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B research/fixed-line-crossing-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fixed-line-crossing-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fixed-line-crossing-floor --check-source-history
+```
+
+The marker is `PASS_FIXED_LINE_CROSSING_FLOOR`. The checker enumerates every
+permutation through six registers over Q and three prime fields, checks a
+104-register exchange, enumerates all nested MOVE edges in the binary subspace
+lattices through dimension four, and exercises rejected circuits and a changed
+public-frame control. Its stdout receipt binds the package bytes by SHA256.
+It writes no generated files. Exact counts appear in the generated output.
+An export can run the direct verifier without Git or predecessor executables.
+The changed-frame control permits public ascent and descent; it is a boundary
+test, not a proposed legal native.
+
+[SOURCES.json](SOURCES.json) pins the predecessor text, catalogue and selected
+record as historical provenance. There are no external runtime inputs or
+dependencies. The selected metadata orientation passed; the selected cold
+replay, predecessor scientific suites, Lean and Docker were not run.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Can a public-frame change or an exchange interleaved with the Y bounce
+  reduce the complete Whitehead bill? This escapes a specific hypothesis of
+  the floor. Start with one literal shared-carrier schedule and record its
+  complete endpoint, frame changes and both public and owned charges. A legal
+  schedule with restored outputs and a favorable complete bill is missing.
+- What is the smallest peak owned storage among schedules attaining `2s`
+  MOVEs? The construction here uses one carrier per moved source. Start with
+  a single permutation cycle and permit interleaving; a matching storage
+  lower bound is not supplied here.
+
+## Credit
+
+The new fixed-line theorem, general attaining schedule and checker were
+produced by Nick Petalas. DreamingOfClouds supplies the Whitehead window
+construction, matching exchange and shared-landing question in #6939.
+Retain its credit to Ali Romman #5599, CubeJerry #6912/#6914/#6916,
+unpaidmoon #6930, icekylinx #104 and their native/caller predecessors.
+New work is Apache-2.0; predecessor files remain unchanged.
+
+## Checker bounds
+
+The finite checker caps inputs at 104 ports and 832 events, with at most 211
+symbolic rows of 107 integer coefficients. It enumerates at most 720
+permutations at a given size and four payload fields. The lattice check uses
+at most 67 subspaces with 16 elements each. Every loop has an explicit finite
+corpus or enforced input bound; no recursion, subprocess or network call is
+used. Each function is under 60 lines. Explicit checks remain enabled under
+optimized Python.
+
+Python's managed runtime allocates rows, sets and integers during replay,
+which is a deviation from fixed allocation under Power of Ten rule 3. The
+stated finite capacities bound live collections; fixture coefficients have
+absolute value at most 104. This is a bounded offline verifier, not a real-time
+implementation. Revisit allocation and coefficient bounds before expanding
+its input domain. Warnings are errors in both registered commands.

research/fixed-line-crossing-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/p104-whitehead-native-objects/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "4956b7e63f50870b3fd0a1ed3162224e876ead6c",
+      "sha256": "d01547cfeeec205af989999b00f4e7a59c827aaff6a5a86c182fd151f0bd0d73"
+    },
+    {
+      "path": "research/p104-whitehead-native-objects/README.md",
+      "usage": "provenance",
+      "git_blob": "9fcc0292a7c6ec24c447d45791e010797e75ab58",
+      "sha256": "42c8b1f7a5b6561e206fdd06a4b942a7bebce10f0cb082f34b55268371893c4f"
+    }
+  ]
+}

research/fixed-line-crossing-floor/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 8,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "productive helper",
+      "target refinement",
+      "5599",
+      "5614"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp 2s owned-MOVE lower bound and rank-one attainment for scaled permutations moving s public registers on distinct fixed binary lines, with arbitrary shared carriers and local linear feedback. Application to the 104-port matching preprocessing contract of PR6939 gives 208 owned MOVEs.",
+  "scope_change_reason": "Replace helper-inventory construction with one exact transport obstruction for the shared-landing question in DreamingOfClouds PR6939. The fixed-line preprocessing contract is essential; no full native exclusion follows.",
+  "bottleneck_link": "Eliminates carrier sharing alone as a way to lower the Whitehead beta-crossing preprocessing bill while public X frames stay fixed. A promising continuation must change that boundary or combine it with the Y bounce and pay the full bill.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first sharp local theorem after exact attainers, frame-edge checks and rejection controls; do not extend to a changed native.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md; verify.py: 3492 small exact matrix cases, 1008 nested frame edges, one generic 104-port exchange, 18 rejection controls, and one changed-public-frame escape control.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a public-frame change or an exchange interleaved with the Y bounce reduce the complete Whitehead bill?",
+      "why_it_matters": "These changes escape the fixed-frame checkpoint and can change the native construction decision.",
+      "first_step": "Write one literal shared-carrier schedule, then record its complete endpoint, all public and owned frame changes, and full charges.",
+      "blocked_by": "No legal schedule with restored outputs and a favorable complete bill is supplied."
+    },
+    {
+      "question": "What is the smallest peak owned storage at the minimum 2s MOVE count?",
+      "why_it_matters": "The general attainer uses one carrier per moved source; storage is separate from its MOVE optimum.",
+      "first_step": "Analyze one permutation cycle with interleaved carrier transport and overwrite.",
+      "blocked_by": "A matching storage lower bound and complete physical storage price are not supplied."
+    }
+  ],
+  "environment": {
+    "python": "3.12.15",
+    "dependencies": "standard library only"
+  },
+  "predecessor": {
+    "pr": 6939,
+    "author": "DreamingOfClouds",
+    "question": "README Open next question 2; PROOF section 6 item 2",
+    "input_status": "Cited predecessor text and matching construction; no scientific executable replayed."
+  }
+}

research/fixed-line-crossing-floor/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact scaled-permutation endpoints and scratch clearing over integers and F2/F3/F5; all nested frame edges through dimension four; sharp move/rank/peak counts; 18 rejection controls; changed-public-frame escape; generated package hash receipt."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Repeat all exact checks with Python assertions disabled; explicit contracts must remain active."
+    }
+  ]
+}