diff --git a/research/p104-controller-income-audit/PROOF.md b/research/p104-controller-income-audit/PROOF.md new file mode 100644 index 0000000000..9bd0616007 --- /dev/null +++ b/research/p104-controller-income-audit/PROOF.md @@ -0,0 +1,83 @@ +# Audit of PR6114: controller income bound + +Audited: PR #6114 (Matarener), head `3183c6553e5559df8807fde4fec27e2403f3040a`, +`research/p104-controller-income-bound/PROOF.md`, against the literal alphabet of +`research/p104-productive-controller/caller.py` on main `721c03822`. + +**Verdict.** The theorem is correct as stated for the literal alphabet: with a constant invertible right +boundary, `s` paid odd shears and `n_odd` outputs with zero even part, `n_odd ≤ s − 1`. The three retained +controllers attain it (33 shears, 32 twisted outputs, income 17 = 18 − 1); an independent engine reproduces every +number. There are two gaps in the written argument, both closable (A1, A2), and a cosmetic error (A3). The scope sentence +"a paid primitive that touches several banks or ports at once ... is the only way to escape the bound" is +overstated: one-bank paid primitives and non-constant boundaries also escape, while multi-source jobs that write +a single row do not (A4). + +Notation as in PR6114: every bank row is `a + Q·b` with `a, b ∈ R_even^n`, `R_even = ℚ[Q^{±2}] ⊗ ℚ[D_0, …, D_32]`; +`E` is the matrix of even parts and `B` the matrix of odd coefficients, so the state is `M = E + Q·B`. + +## A1. The left boundary (gap in step 4 / the theorem's last inequality) + +PR6114's PROOF.md says that the left boundary is applied at the end. It then uses "the `n_odd` zero rows give +`rank E_final ≤ n − n_odd`". But the zero rows belong to `L·M`, not to `M`. The repair below does not need `L` +to be invertible. Let `T` be the set of twisted outputs and `L_T` the corresponding rows of the constant matrix +`L`. The even part of `L_T·M` is `L_T·E = 0`, so the rows of `L_T` lie in the left kernel of `E`. The outputs +`Q^{±1}D^{S_i}e_i` (`i ∈ T`) are linearly independent, so `rank L_T ≥ rank(L_T M) = |T|`. Hence +`n − rank E ≥ |T|`. On the literal words `L` is invertible anyway (checked). + +## A2. Lift cancellation (unproved step of the invoice consequence) + +The consequence `income = Σ_i (1 + d|S_i|) − d·lifts − n_thin = n_out − n_thin` needs `Σ_i |S_i| = lifts`. +PR6114 asserts this ("every stage that appears in an output was paid once as a lift"). That assertion is +true, and it follows from the determinant for every word whose outputs form the full monomial diagonal. +Scalar `ADD`, swaps and shears have determinant `±1`, `Q_POWER` multiplies the determinant by `Q^{±2}`, and a +lift of row `r` by `D_s` multiplies it by `D_s`. So `det(L·M_final) = c·Q^{2k}·∏_s D_s^{ℓ_s}`, with `c ∈ ℚ^×` and +`ℓ_s` the number of row-lifts at stage `s`. For each output `i`, `S_i` is its stage set. The diagonal +`diag(Q^{q_i}D^{S_i})` has determinant `∏ Q^{q_i} ∏_s D_s^{#{i : s ∈ S_i}}`, and `ℚ[Q^{±1}, D]` is a UFD. Hence +`#{i : s ∈ S_i} = ℓ_s` for every stage `s`, and `Σ_i q_i = 2k`. The verifier checks both identities stage by +stage on all three controllers (`Σ|S_i| = 194` lifts, net `Q_POWER` = `Σ q_i`). If a word twists only some of its +outputs, this argument does not apply, and the consequence needs the untwisted outputs' targets to be stated. +The physical cost model in `caller.py` accepts only odd diagonal outputs. + +## A3. Cosmetic + +The stage markers are `D_0, …, D_32` (33 of them; `caller.py` exponent tuples have 1 + 33 entries). They are not +`D_0, …, D_33`. + +## A4. Which paid primitives escape + +Write a paid job as `M ← A·M` with `A = A_e + Q·A_o` (`A_e, A_o` over `R_even`). Then the new even part is +`E' = A_e·E + Q²·A_o·B`. Sylvester's rank inequality gives + + rank E' ≥ rank E − (n − rank A_e) − rank A_o , and, if B = 0, rank E' ≥ rank E − (n − rank A_e). + +Free events have `A_o = 0` and invertible `A_e`, so they preserve `rank E` and keep `B = 0` before the first paid +job. With a constant invertible entry this gives + + n_odd ≤ (n − rank A_e^(1)) + Σ_{k ≥ 2} [(n − rank A_e^(k)) + rank A_o^(k)] . + +PR6114's open question 1 asks for this bound ("twisted ≤ sum over paid jobs of their even-rank change"), and the +formula above computes it from the job matrices alone. Consequences: + +* **Positive (generalization).** A paid job that writes one row, `y ← u·y + Σ_{j≠y} f_j·x_j`, has `A_e` + invertible and `rank A_o ≤ 1` when `u ∈ R_even` is nonzero. This holds for any number of source banks and any + Laurent coefficients `f_j`. Such jobs obey PR6114's bound exactly, including the `− 1`. Touching several banks is + therefore not by itself an escape. +* **Escape 1: an odd one-bank job.** A paid odd translation `y ← Q·y` has `rank A_e = n − 1` and twists one output + even as the first job. So `s` such jobs can twist `s` outputs, which is one more than the bound. Control: + one job, one odd row. +* **Escape 2: a non-constant boundary.** If the entry rows already carry odd content, step 3 fails. Control + (2 banks): entry `x = e1 − Q·e2`, `y = e2`, then `y += Q^{-1}x` and `x += −Q·y` give the odd rows `−Q·e2` + and `Q^{-1}·e1`. That is 2 twisted outputs from 2 shears. The entry is one backward shear of the identity, so + a Laurent boundary can hide a paid shear. With a general entry the bound is `n_odd ≤ (n − rank E_entry) + s`. +* **Escape 3: a job that writes several rows.** This is the case PR6114 names. Control: the 2×2 composite of the + three Whitehead shears, taken as one paid job, drops the even rank by 2 from a constant entry. + +Within the literal alphabet (rational boundary programs, `Q_POWER ∈ {±2}`, one-pair shears with coefficient +`Q^{-1}` or `−Q`) none of these escapes is available, so PR6114's theorem and its 17 = 18 − 1 conclusion stand. + +## Not audited + +The surplus formula `M = v·income − n_thick·c` and the value `c = 56` on the PR5907 word (`760`) were not +rechecked against an invoice. The choice of rank mass rather than the moment as the objective was not audited +either; PR6114 itself defers the moment to PR5554 and `research/fragmentation-ceiling`. The random one-destination +test supports the A4 positive case, and the A4 proof is the evidence for it. diff --git a/research/p104-controller-income-audit/README.md b/research/p104-controller-income-audit/README.md new file mode 100644 index 0000000000..512325a0e1 --- /dev/null +++ b/research/p104-controller-income-audit/README.md @@ -0,0 +1,72 @@ +# Audit of PR6114's controller income bound + +**Independent adversarial audit; no new κ; the selected record is unchanged.** + +[PR #6114](https://github.com/CrocSwap/integer-mult-bounds/pull/6114) (Matarener, head `3183c655`) proves a +theorem about the literal p16 Laurent caller alphabet of +[`research/p104-productive-controller/caller.py`](../p104-productive-controller/caller.py). Starting from a +constant invertible boundary, a caller word with `s` paid odd shears (`LOCAL`, `QUERY_SHEAR`) twists at most +`s − 1` outputs. So the controller income per port is at most `thick calls − 1`, and the three retained controllers +attain this (17 = 18 − 1). This package checks that theorem independently. + +## Result + +* **The theorem holds** for the literal alphabet. I re-derived the proof, and a separate engine reproduces every + number. That engine is written here without importing `caller.py` or PR6114's code. It runs an exact symbolic + Laurent replay of all three controllers to the declared odd diagonal. It also tracks the even-part rank after + every event under a different specialization: `Q² → 13/7, 19/11`, with random nonzero stage values where + PR6114 sets `D_s → 1`. + + | Controller | thick + thin | twisted | even-rank trace | lifts = Σ\|S_i\| | income | + |---|---:|---:|---|---:|---:| + | `kappa-backward-controller-20261023` | 18 + 15 | 32 | 32, 32, 31, …, 0 | 194 | 17 | + | `joint-helper-lattice` | 18 + 15 | 32 | 32, 32, 31, …, 0 | 194 | 17 | + | `p104-productive-controller` | 18 + 15 | 32 | 32, 32, 31, …, 0 | 194 | 17 | + +* **Two gaps in the written proof, both closed** ([PROOF.md](PROOF.md) A1–A2). First, the last inequality uses + zero rows of `L·M`, not of `M`. A left-kernel argument repairs it, and `L` need not be invertible. Second, the + invoice step "every output stage was paid once as a lift" was asserted, not proved. It follows from the + determinant, stage by stage, for every word whose outputs form the full monomial diagonal. The verifier checks + all 33 stages and the central exponent on each controller. +* **The scope claim needs correcting** (A4). PR6114 says a paid primitive touching several banks or ports is + "the only way" to beat the bound. For a paid job `A = A_e + Q·A_o`, Sylvester's inequality bounds the even-rank + drop by `(n − rank A_e) + rank A_o`. When no odd content exists yet, the bound is `n − rank A_e`. From that: + * Every paid job that writes **one** row `y ← u·y + Σ f_j·x_j` obeys PR6114's bound exactly, including the + `− 1`. This needs the self-coefficient `u` to be nonzero and even. The sources can be any number of banks, + and the `f_j` can be any Laurent coefficients. + * Three escapes exist, each with an exact control: a paid **one-bank** odd translation `y ← Q·y` (1 twist from + 1 job); a **Laurent entry boundary** (2 twists from 2 shears); and a **two-row** job (2 twists from 1 job). + None of them is in the literal alphabet, so PR6114's conclusion stands. + +Not audited: the surplus formula `M = v·income − n_thick·c` and `c = 56`/`760` on the PR5907 word, and the +moment side. + +## Reproduce + +```sh +python3.12 -B research/p104-controller-income-audit/verify.py +python3.12 -B scripts/research_package.py --package research/p104-controller-income-audit +``` + +The run takes under a second and uses only the standard library. Engine: [audit.py](audit.py). Evidence: +[RESULT.json](RESULT.json), compared in full. The random one-destination words (n = 2, 4, 6; 3,909 paid jobs) +never exceed the bound. In 41 of them the even-rank deficit `n − rank E` equals `s − 1`. This counts the rank +deficit only; the test builds no twisted outputs. They support the A4 proof and do not replace it. + +## Open next questions + +1. **Can Escape 1 or 2 be realized physically at the P104 caller?** A legal paid odd translation `Q^{±1}`, or a + supplier boundary that already carries odd content, would lift the cap from `thick − 1` to `thick` per port. + That is up to 104 rank units on the PR5907 word, before the primitive's own charge is paid. First step: price + `Q^{±1}` as a native job in the terms of `caller.py`'s `physical()`. Blocker: the literal alphabet rejects it + as a free event, and no native realization is known here. +2. **What twist capacity do the available multi-row paid jobs have?** For any candidate job, compute + `(n − rank A_e, rank A_o)` before searching, and compare the result with its paid rank. Blocker: there is no + priced inventory of multi-bank primitives. + +## Credit + +PR6114 and its theorem: Matarener (prepared with Claude). The retained controllers come from Cinna Davis (p16/a7 +lattice) and Ali Romman (PR5398 replay, all-forward wrapper). The binary predecessor theorem is Cinna Davis's +`research/productive-controller-basis-search`. Audit by Josie Elliston, prepared with Claude Code (Opus 5.5). +Apache-2.0. diff --git a/research/p104-controller-income-audit/RESULT.json b/research/p104-controller-income-audit/RESULT.json new file mode 100644 index 0000000000..dad81ab98a --- /dev/null +++ b/research/p104-controller-income-audit/RESULT.json @@ -0,0 +1,354 @@ +{ + "audited_head": "3183c6553e5559df8807fde4fec27e2403f3040a", + "audited_pr": 6114, + "controllers": { + "joint_helper_lattice": { + "bound_s_minus_1": 32, + "events": 154, + "image_receipts": { + "13/7": { + "even_rank_trace": [ + 32, + 32, + 31, + 30, + 29, + 28, + 27, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ], + "stage_values_sha256": "7d879bfb031664f3c9aff0c3382435b8cb0f7ba0088345bf1d1ec3b25b60ad1c" + }, + "19/11": { + "even_rank_trace": [ + 32, + 32, + 31, + 30, + 29, + 28, + 27, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ], + "stage_values_sha256": "7af6f05e2364a128d07c6d63bf0d91646ccd7c74e3107de256789b715e972ef7" + } + }, + "income": 17, + "net_q_power": 0, + "odd_outputs": 32, + "output_stage_mass": 194, + "paid_lifts_rank": 1552, + "paid_shears": 33, + "path": "research/joint-helper-lattice/CONTROLLER.json", + "row_stage_lifts": 194, + "targets_rank_sum": 1584, + "thick": 18, + "thin": 15 + }, + "kappa_backward_controller": { + "bound_s_minus_1": 32, + "events": 162, + "image_receipts": { + "13/7": { + "even_rank_trace": [ + 32, + 32, + 31, + 30, + 29, + 28, + 27, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ], + "stage_values_sha256": "8813d68ecb0810c4c34e6a72483ad1a71df4a0f07b6dabd743c46fc973ab6dbd" + }, + "19/11": { + "even_rank_trace": [ + 32, + 32, + 31, + 30, + 29, + 28, + 27, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ], + "stage_values_sha256": "36ed2a8ae8833c353ce11e0acf32b0ff34fbce5dc128f507daf545a4e7943f97" + } + }, + "income": 17, + "net_q_power": 0, + "odd_outputs": 32, + "output_stage_mass": 194, + "paid_lifts_rank": 1552, + "paid_shears": 33, + "path": "research/kappa-backward-controller-20261023/CONTROLLER.json", + "row_stage_lifts": 194, + "targets_rank_sum": 1584, + "thick": 18, + "thin": 15 + }, + "p104_productive_controller": { + "bound_s_minus_1": 32, + "events": 218, + "image_receipts": { + "13/7": { + "even_rank_trace": [ + 32, + 32, + 31, + 30, + 29, + 28, + 27, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ], + "stage_values_sha256": "6dc67bfa47f8eb80d8bf4afa6fd6cef31a2fe39a872f56d2248d1a5ab300b6a6" + }, + "19/11": { + "even_rank_trace": [ + 32, + 32, + 31, + 30, + 29, + 28, + 27, + 26, + 25, + 24, + 23, + 22, + 21, + 20, + 19, + 18, + 17, + 16, + 15, + 14, + 13, + 12, + 11, + 10, + 9, + 8, + 7, + 6, + 5, + 4, + 3, + 2, + 1, + 0 + ], + "stage_values_sha256": "6438f45e33bfc3bd02b8266e43e5fe72cd1aa98745965b602c48b2baca0cf58a" + } + }, + "income": 17, + "net_q_power": 0, + "odd_outputs": 32, + "output_stage_mass": 194, + "paid_lifts_rank": 1552, + "paid_shears": 33, + "path": "research/p104-productive-controller/CONTROLLER.json", + "row_stage_lifts": 194, + "targets_rank_sum": 1584, + "thick": 18, + "thin": 15 + } + }, + "pinned_inputs": 3, + "scope_controls": { + "laurent_entry_boundary": { + "entry_even_rank": 2, + "exceeds_constant_entry_bound": true, + "final_rows": [ + [ + "0", + "0", + "0", + "-1" + ], + [ + "0", + "0", + "3/7", + "0" + ] + ], + "odd_monomial_rows": 2, + "paid_shears": 2 + }, + "one_destination_random": [ + { + "banks": 2, + "even_rank_drops_total": 70, + "length": 6, + "max_excess_over_bound": 0, + "paid_jobs_total": 1199, + "words": 400, + "words_even_rank_deficit_equals_bound": 37 + }, + { + "banks": 4, + "even_rank_drops_total": 39, + "length": 10, + "max_excess_over_bound": 0, + "paid_jobs_total": 1490, + "words": 300, + "words_even_rank_deficit_equals_bound": 4 + }, + { + "banks": 6, + "even_rank_drops_total": 30, + "length": 24, + "max_excess_over_bound": -6, + "paid_jobs_total": 1220, + "words": 100, + "words_even_rank_deficit_equals_bound": 0 + } + ], + "paid_odd_translation": { + "final_even_rank": 1, + "odd_rows": 1, + "paid_jobs": 1 + }, + "two_row_paid_job": { + "even_rank_after": 0, + "even_rank_before": 2, + "odd_rows": 2, + "paid_jobs": 1 + } + } +} diff --git a/research/p104-controller-income-audit/SOURCES.json b/research/p104-controller-income-audit/SOURCES.json new file mode 100644 index 0000000000..1c9b17add2 --- /dev/null +++ b/research/p104-controller-income-audit/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/joint-helper-lattice/CONTROLLER.json", + "usage": "input", + "git_blob": "49a2f0675819f9deeea27ed77be2c2b6ff2e87e5", + "sha256": "1f5d6aa267e4e66048818714b5d3b5eae17a58abe91d15deeaa34574f7391a5f" + }, + { + "path": "research/kappa-backward-controller-20261023/CONTROLLER.json", + "usage": "input", + "git_blob": "01775a36ae1238350bf8cd859b04cb8c4589873b", + "sha256": "60cc512b39cdb9ea2c2ac6c6634c8d3f9627d96ace08ffa659a9d9472444122b" + }, + { + "path": "research/p104-productive-controller/CONTROLLER.json", + "usage": "input", + "git_blob": "cc539db709cf7a6c42872c4380902736ad453af3", + "sha256": "a84f6bbd547379597464e56c420cc665f96bc43a9a1351eed4b7cd0fce3cc4b9" + } + ] +} diff --git a/research/p104-controller-income-audit/TASK.json b/research/p104-controller-income-audit/TASK.json new file mode 100644 index 0000000000..38af7212a2 --- /dev/null +++ b/research/p104-controller-income-audit/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "joint-query-controller", + "question": "Can a changed query demand or caller remove real work while satisfying native chronology and restoration?", + "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": "Choose an exact caller and a new demand/interface hypothesis. Read the scoped #5617/#5631/#5649/#5747 and #5720/#5745 objections before rebuilding an excluded schedule. Compare the complete matched source/consumer protocols including all retained helper outputs. For an active-mode injection, first check #5745: its canonical delivery claim repays the eight removed centre jobs. Audit that exact claim or change its channel/feedback hypothesis; do not repeat the same free-injection search. Stop if the full favorable budget fails or the required restored output is unobservable.", + "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": [ + "query demand", + "active mode", + "5720", + "5745", + "5747", + "caller" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "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": "Independent adversarial audit of PR6114 (head 3183c655): its theorem (constant invertible entry, literal p16 Laurent alphabet: twisted outputs <= paid odd shears - 1, income <= thick calls - 1) re-derived and replayed with a separate exact engine on the three retained controllers; two gaps in the written proof closed (left boundary, lift cancellation via the determinant); scope corrected with an explicit per-job Sylvester bound, one positive generalization (one-destination jobs y <- u y + sum f_j x_j with u nonzero and even and any Laurent f_j obey the bound) and three exact escape controls (paid odd translation, Laurent entry boundary, two-row job).", + "scope_change_reason": "Drawn from the adversarial-audit track (the overnight coordinator flagged it as under-served; its uniform-transfer and supplier-boundary cards are PR6030-adjacent and PR6030 already had six follow-ups tonight). The audited result belongs to the joint-query-controller card, so this package keeps that card and audits its newest unreviewed result instead of building a new controller.", + "bottleneck_link": "PR6114 argues that the controller rank-mass income per port is capped at thick calls minus one, leaving the owned centre and local-word fragmentation as the complex-side levers. The audit confirms the cap for the literal alphabet and states exactly which changed primitives or interfaces can exceed it, so a later controller search knows which hypothesis it must change.", + "budget_minutes": 60, + "stop_rule": "Stop at a confirmed or refuted theorem with an exact, independently replayed check of the three literal controllers and exact controls for each scope claim; do not audit the surplus formula M or the moment.", + "outcome": "completed", + "evidence": "research/p104-controller-income-audit/RESULT.json", + "author": "Josie Elliston", + "ai_assistance": "Prepared with Claude Code (Opus 5.5); optional read-only OpenAI Codex review.", + "open_questions": [ + { + "question": "Is there a legal physical primitive realizing Escape 1 (a paid odd central translation Q^{+-1} on one bank) or Escape 2 (a supplier boundary that already carries odd Q content) at the P104 caller, and what does it cost?", + "why_it_matters": "Either would raise the controller income from thick - 1 to thick per port (104 rank units on the PR5907 word) without the multi-bank primitive that PR6114 names as the only escape.", + "first_step": "Price Q^{+-1} as a native job in research/p104-productive-controller/caller.py physical() terms (it is a translation by the port axis q with a phase), and check whether its rank charge is below one unit per port.", + "blocked_by": "Native/physical realization of an odd translation; the literal alphabet rejects it as a free event." + }, + { + "question": "Which multi-row paid jobs (rank A_o >= 2 or singular A_e) are physically available, and is the even-rank drop they buy worth their charge?", + "why_it_matters": "The Sylvester bound in PROOF.md A4 makes the per-job twist capacity (n - rank A_e) + rank A_o computable before any search.", + "first_step": "Compute (n - rank A_e, rank A_o) for each candidate paid job in an existing supplier inventory and compare with its paid rank.", + "blocked_by": "An inventory of multi-bank paid primitives with prices." + } + ] +} diff --git a/research/p104-controller-income-audit/VERIFY.json b/research/p104-controller-income-audit/VERIFY.json new file mode 100644 index 0000000000..ac1d8b51e8 --- /dev/null +++ b/research/p104-controller-income-audit/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-helper-lattice/CONTROLLER.json", + "research/kappa-backward-controller-20261023/CONTROLLER.json", + "research/p104-productive-controller/CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Authenticate the three pinned controllers; independent exact Laurent replay (own engine, no caller.py import) from the constant right boundary through the constant left boundary, outputs equal the declared odd diagonal; both boundary programs exact and invertible; per-stage determinant identity (output stage counts = row lifts) and net Q_POWER = sum of central exponents; income 17 = 18 - 1; even-part rank after every event under Q^2 -> 13/7, 19/11 with random nonzero stage values: free events never change it, first paid shear 0, each shear <= 1, trace 32,32,31,...,0; scope controls: Laurent entry boundary 2 odd rows from 2 shears, paid odd translation 1 from 1, two-row job 2 from 1; random one-destination words (n = 2, 4, 6) never exceed the bound on the even-rank deficit and reach it; RESULT.json compared in full." + } + ] +} diff --git a/research/p104-controller-income-audit/audit.py b/research/p104-controller-income-audit/audit.py new file mode 100644 index 0000000000..712626fdc1 --- /dev/null +++ b/research/p104-controller-income-audit/audit.py @@ -0,0 +1,309 @@ +"""Independent audit engine for PR6114's controller income bound. + +Written from the event semantics of research/p104-productive-controller/caller.py +without importing it or PR6114's incomebound.py. Standard library only. +Josie Elliston with Claude Code (Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as F +import random + +NS = 33 # stage markers D_0 .. D_32 (caller.py: 1 Q exponent + 33 stage exponents) + + +# ---------------------------------------------------------------- linear algebra +def rank(rows): + """Exact rank over Q of a list of Fraction vectors.""" + m = [list(r) for r in rows if any(r)] + rk, col = 0, 0 + ncol = len(m[0]) if m else 0 + while rk < len(m) and col < ncol: + piv = next((i for i in range(rk, len(m)) if m[i][col]), None) + if piv is None: + col += 1 + continue + m[rk], m[piv] = m[piv], m[rk] + p = m[rk][col] + for i in range(rk + 1, len(m)): + if m[i][col]: + f = m[i][col] / p + m[i] = [x - f * y for x, y in zip(m[i], m[rk])] + rk += 1 + col += 1 + return rk + + +def run_program(program, n): + m = [[F(int(i == j)) for j in range(n)] for i in range(n)] + for e in program: + if e[0] == 'SWAP': + m[e[1]], m[e[2]] = m[e[2]], m[e[1]] + elif e[0] == 'SCALE': + m[e[1]] = [F(e[2]) * x for x in m[e[1]]] + elif e[0] == 'ADD': + m[e[1]] = [x + F(e[3]) * y for x, y in zip(m[e[1]], m[e[2]])] + else: + raise ValueError('boundary opcode ' + repr(e[0])) + return m + + +# ---------------------------------------------------------------- exact Laurent replay +def padd(dst, src, c, shift): + for k, v in src.items(): + kk = tuple(a + b for a, b in zip(k, shift)) + w = dst.get(kk, F(0)) + c * v + if w: + dst[kk] = w + else: + dst.pop(kk, None) + + +def exact_replay(word): + """Symbolic replay over Q[Q^{+-1}, D_0..D_32]; returns output matrix and counters.""" + n = 2 * word['pairs'] + zero = (0,) * (1 + NS) + unit = lambda q=0, stages=(): (q,) + tuple(int(s in stages) for s in range(NS)) + rows = [[({zero: F(x)} if F(x) else {}) for x in r] for r in word['boundaries']['right']] + + def scaled(i, shift, sign=1): + rows[i] = [{tuple(a + b for a, b in zip(k, shift)): sign * v for k, v in cell.items()} for cell in rows[i]] + + cnt = {'LOCAL': 0, 'QUERY_SHEAR': 0, 'lifts': 0, 'qpower': 0} + for e in word['physical_events']: + op = e[0] + if op in ('LOCAL', 'QUERY_SHEAR'): + _, stage, pair, back = e + src, dst = (2 * pair + 1, 2 * pair) if back else (2 * pair, 2 * pair + 1) + shift, c = (unit(1), F(-1)) if back else (unit(-1), F(1)) + new = [dict(cell) for cell in rows[dst]] + for d, s in zip(new, rows[src]): + padd(d, s, c, shift) + rows[dst] = new + cnt[op] += 1 + if op == 'LOCAL': + for r in (2 * pair, 2 * pair + 1): + scaled(r, unit(0, (stage,))) + cnt['lifts'] += 2 + elif op == 'Q_POWER': + if e[2] not in (-2, 2): + raise ValueError('odd central power is not free') + scaled(e[1], unit(e[2])) + cnt['qpower'] += e[2] + elif op == 'IDLE': + # caller.py replay() reads the stage list as a set; its physical() rejects repeats, as here + if len(set(e[2])) != len(e[2]): + raise ValueError('repeated idle stage') + for r in (2 * e[1], 2 * e[1] + 1): + scaled(r, unit(0, tuple(e[2]))) + cnt['lifts'] += 2 * len(e[2]) + elif op == 'ADD': + new = [dict(cell) for cell in rows[e[1]]] + for d, s in zip(new, rows[e[2]]): + padd(d, s, F(e[3]), zero) + rows[e[1]] = new + elif op in ('SWAP', 'SIGNED_SWAP'): + a, b = e[1], e[2] + ra, rb = rows[a], rows[b] + rows[a] = rb + rows[b] = ra + if op == 'SIGNED_SWAP': + scaled(b, zero, -1) + else: + raise ValueError('opcode ' + repr(op)) + out = [[{} for _ in range(n)] for _ in range(n)] + for i, lrow in enumerate(word['boundaries']['left']): + for k, q in enumerate(lrow): + if F(q): + for j in range(n): + padd(out[i][j], rows[k][j], F(q), zero) + return out, cnt + + +# ---------------------------------------------------------------- specialized even/odd tracker +class Image: + """Image under Q^2 -> theta, D_s -> r_s: each bank row is a + Q b with a, b in Q^n.""" + + def __init__(self, entry_even, entry_odd, theta, r): + self.a = [list(x) for x in entry_even] + self.b = [list(x) for x in entry_odd] + self.t, self.r = F(theta), [F(x) for x in r] + + def even_rank(self): + return rank(self.a) + + def add(self, y, x, c, qexp=0): + """row_y += c * Q^qexp * row_x, qexp in {-1, 0, 1}.""" + ax, bx = self.a[x], self.b[x] + if qexp == 0: + da, db = ax, bx + elif qexp == 1: # Q(a + Qb) = theta b + Q a + da, db = [self.t * v for v in bx], ax + elif qexp == -1: # Q^-1(a + Qb) = b + Q a/theta + da, db = bx, [v / self.t for v in ax] + else: + raise ValueError(qexp) + self.a[y] = [u + c * v for u, v in zip(self.a[y], da)] + self.b[y] = [u + c * v for u, v in zip(self.b[y], db)] + + def scale(self, i, s): + self.a[i] = [s * v for v in self.a[i]] + self.b[i] = [s * v for v in self.b[i]] + + def times_q(self, i, sign=1): + """row_i *= sign * Q (a paid odd translation; not in the literal alphabet).""" + a, b = self.a[i], self.b[i] + self.a[i] = [sign * self.t * v for v in b] + self.b[i] = [sign * v for v in a] + + +def image_trace(word, theta, r): + """Even-part rank after every event; returns (trace at shears, per-event deltas by kind).""" + n = 2 * word['pairs'] + R = [[F(x) for x in row] for row in word['boundaries']['right']] + im = Image(R, [[F(0)] * n for _ in range(n)], theta, r) + trace = [im.even_rank()] + free_changes, shear_deltas = 0, [] + for e in word['physical_events']: + op = e[0] + before = trace[-1] + if op in ('LOCAL', 'QUERY_SHEAR'): + _, stage, pair, back = e + src, dst = (2 * pair + 1, 2 * pair) if back else (2 * pair, 2 * pair + 1) + if back: + im.add(dst, src, F(-1), 1) + else: + im.add(dst, src, F(1), -1) + if op == 'LOCAL': + for q in (2 * pair, 2 * pair + 1): + im.scale(q, im.r[stage]) + elif op == 'Q_POWER': + im.scale(e[1], im.t if e[2] == 2 else 1 / im.t) + elif op == 'IDLE': + s = F(1) + for st in e[2]: + s *= im.r[st] + for q in (2 * e[1], 2 * e[1] + 1): + im.scale(q, s) + elif op == 'ADD': + im.add(e[1], e[2], F(e[3])) + else: + a, b = e[1], e[2] + im.a[a], im.a[b] = im.a[b], im.a[a] + im.b[a], im.b[b] = im.b[b], im.b[a] + if op == 'SIGNED_SWAP': + im.scale(b, F(-1)) + now = im.even_rank() + if op in ('LOCAL', 'QUERY_SHEAR'): + shear_deltas.append(now - before) + trace.append(now) + elif now != before: + free_changes += 1 + trace[-1] = now + L = [[F(x) for x in row] for row in word['boundaries']['left']] + out_even = [[sum(L[i][k] * im.a[k][j] for k in range(n)) for j in range(n)] for i in range(n)] + return trace, shear_deltas, free_changes, out_even + + +def random_rationals(rng, k): + vals = [] + while len(vals) < k: + v = F(rng.randint(-29, 29), rng.randint(1, 17)) + if v: + vals.append(v) + return vals + + +# ---------------------------------------------------------------- scope controls (small n) +def laurent_entry_control(): + """Entry rows x = e1 - Q e2, y = e2 (a Laurent, non-constant boundary). + Two shears (y += Q^-1 x, then x += -Q y) give two odd monomial rows.""" + theta = F(7, 3) + im = Image([[F(1), F(0)], [F(0), F(1)]], [[F(0), F(-1)], [F(0), F(0)]], theta, []) + r0 = im.even_rank() + im.add(1, 0, F(1), -1) + im.add(0, 1, F(-1), 1) + rows = [(im.a[i], im.b[i]) for i in range(2)] + odd_monomials = all(not any(a) and sum(1 for v in b if v) == 1 for a, b in rows) + return {'entry_even_rank': r0, 'paid_shears': 2, 'odd_monomial_rows': 2 if odd_monomials else None, + 'final_rows': [[str(v) for v in a] + [str(v) for v in b] for a, b in rows], + 'exceeds_constant_entry_bound': odd_monomials and 2 > 2 - 1} + + +def odd_translation_control(): + """One paid odd translation row *= Q from a constant entry twists one output with s = 1.""" + im = Image([[F(1), F(0)], [F(0), F(1)]], [[F(0)] * 2, [F(0)] * 2], F(11, 5), []) + im.times_q(0) + return {'paid_jobs': 1, 'odd_rows': sum(1 for i in range(2) if not any(im.a[i]) and any(im.b[i])), + 'final_even_rank': im.even_rank()} + + +def two_row_job_control(): + """One paid job writing both rows of a pair (the composite of the three Whitehead shears) + from a constant entry: two odd rows with one paid job.""" + im = Image([[F(1), F(0)], [F(0), F(1)]], [[F(0)] * 2, [F(0)] * 2], F(13, 7), []) + before = im.even_rank() + im.add(1, 0, F(1), -1) + im.add(0, 1, F(-1), 1) + im.add(1, 0, F(1), -1) + return {'paid_jobs': 1, 'even_rank_before': before, 'even_rank_after': im.even_rank(), + 'odd_rows': sum(1 for i in range(2) if not any(im.a[i]) and any(im.b[i]))} + + +def one_destination_random(seed, words, n, length): + """Random words: free events (constant ADD, swap, even scalings) and paid one-destination jobs + row_y = u row_y + sum_j f_j row_j with u a nonzero even scalar and f_j = c0 + c1 Q + c2 Q^-1. + Checks every paid job changes the even rank by at most one, the first by zero, and free events by zero.""" + rng = random.Random(seed) + worst, jobs_total, drops, tight = None, 0, 0, 0 + for _ in range(words): + theta = F(rng.choice([2, 3, 5, 7, 11, 13]), rng.choice([1, 3, 5, 7])) + R = [[F(rng.randint(-3, 3)) for _ in range(n)] for _ in range(n)] + while rank(R) < n: + R = [[F(rng.randint(-3, 3)) for _ in range(n)] for _ in range(n)] + im = Image(R, [[F(0)] * n for _ in range(n)], theta, []) + rk, paid, first = n, 0, True + for _ in range(length): + kind = rng.random() + if kind < 0.5: + y = rng.randrange(n) + if rng.random() < 0.7: # literal-type shear: one source, coefficient Q^-1 or -Q + j = rng.choice([j for j in range(n) if j != y]) + if rng.random() < 0.5: + im.add(y, j, F(1), -1) + else: + im.add(y, j, F(-1), 1) + else: + srcs = rng.sample([j for j in range(n) if j != y], rng.randint(1, min(3, n - 1))) + im.scale(y, F(rng.choice([1, -1, 2, -3])) * (theta ** rng.choice([-1, 0, 1]))) + # simultaneous update: read sources before writing (sources exclude y) + for j in srcs: + for qexp in (-1, 0, 1): + c = F(rng.randint(-2, 2)) + if c: + im.add(y, j, c, qexp) + now = im.even_rank() + if now < rk - 1 or now > rk + 1 or (first and now != rk): + raise AssertionError('one-destination job moved even rank by more than allowed') + drops += rk - now if now < rk else 0 + rk, paid, first = now, paid + 1, False + else: + y, x = rng.sample(range(n), 2) + if kind < 0.8: + im.add(y, x, F(rng.choice([1, -1, 2]))) + elif kind < 0.9: + im.a[y], im.a[x] = im.a[x], im.a[y] + im.b[y], im.b[x] = im.b[x], im.b[y] + else: + im.scale(y, theta if rng.random() < 0.5 else F(rng.choice([2, -1]))) + now = im.even_rank() + if now != rk: + raise AssertionError('free event changed even rank') + zero_rows = n - rk # upper bound on odd outputs after any constant left boundary + if paid and zero_rows > paid - 1: + raise AssertionError('bound violated') + if paid: + worst = zero_rows - (paid - 1) if worst is None else max(worst, zero_rows - (paid - 1)) + tight += int(paid > 0 and zero_rows == paid - 1) + jobs_total += paid + return {'words': words, 'banks': n, 'length': length, 'paid_jobs_total': jobs_total, + 'even_rank_drops_total': drops, 'words_even_rank_deficit_equals_bound': tight, + 'max_excess_over_bound': worst} diff --git a/research/p104-controller-income-audit/verify.py b/research/p104-controller-income-audit/verify.py new file mode 100644 index 0000000000..5130f22cd5 --- /dev/null +++ b/research/p104-controller-income-audit/verify.py @@ -0,0 +1,127 @@ +#!/usr/bin/env python3 +"""Verify the independent audit of PR6114 (controller income bound). Standard library only. + + python3 -B research/p104-controller-income-audit/verify.py # check RESULT.json + python3 -B research/p104-controller-income-audit/verify.py --write # regenerate it + +Josie Elliston with Claude Code (Opus 5.5) assistance. Apache-2.0. +""" +from fractions import Fraction as F +from hashlib import sha256 +from pathlib import Path +import json +import random +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +import audit as A # noqa: E402 + +CONTROLLERS = { + 'kappa_backward_controller': 'research/kappa-backward-controller-20261023/CONTROLLER.json', + 'joint_helper_lattice': 'research/joint-helper-lattice/CONTROLLER.json', + 'p104_productive_controller': 'research/p104-productive-controller/CONTROLLER.json', +} +D = 8 # rank per stage lift per bank + + +def need(ok, msg): + if not ok: + raise SystemExit('FAIL: ' + msg) + + +def authenticate(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + inputs = [f for f in pins['files'] if f['usage'] == 'input'] + for f in inputs: + need(sha256((ROOT / f['path']).read_bytes()).hexdigest() == f['sha256'], 'pinned input ' + f['path']) + need(sorted(f['path'] for f in inputs) == sorted(CONTROLLERS.values()), 'input set') + return len(inputs) + + +def audit_controller(name, path): + word = json.loads((ROOT / path).read_text()) + n = 2 * word['pairs'] + need(n == 32, name + ': 32 banks') + # boundaries: exact constant rational programs, invertible + for side in ('left', 'right'): + M = A.run_program(word['boundaries'][side + '_program'], n) + need(M == [[F(x) for x in row] for row in word['boundaries'][side]], name + ': boundary program ' + side) + need(A.rank(M) == n, name + ': invertible ' + side + ' boundary') + out, cnt = A.exact_replay(word) + diag = [tuple(t) for t in word['diagonal']] + expected = [[({diag[i]: F(1)} if i == j else {}) for j in range(n)] for i in range(n)] + need(out == expected, name + ': exact Laurent outputs equal the declared diagonal') + odd = sum(1 for t in diag if t[0] % 2) + need(odd == n and all(abs(t[0]) == 1 for t in diag), name + ': every output an odd monomial Q^+-1 D^S') + thick, thin = cnt['LOCAL'], cnt['QUERY_SHEAR'] + s = thick + thin + # determinant identity (stage exponents and central exponent of det) + stage_mass = sum(sum(t[1:]) for t in diag) + need(all(max(t[1:]) <= 1 for t in diag), name + ': stage sets, no repeated stage in an output') + need(stage_mass == cnt['lifts'], name + ': sum |S_i| = row-stage lifts (det D-exponent)') + need(sum(t[0] for t in diag) == cnt['qpower'], name + ': sum of central exponents = net Q_POWER (det Q-exponent)') + for st in range(A.NS): + per_stage_out = sum(t[1 + st] for t in diag) + per_stage_lift = 0 + for e in word['physical_events']: + if e[0] == 'LOCAL' and e[1] == st: + per_stage_lift += 2 + if e[0] == 'IDLE' and st in e[2]: + per_stage_lift += 2 + need(per_stage_out == per_stage_lift, name + ': per-stage det identity at D_%d' % st) + targets = sum(1 + D * sum(t[1:]) for t in diag) + income = targets - D * cnt['lifts'] - thin + need(income == odd - thin == thick - 1, name + ': income = outputs - thin = thick - 1') + # specialized even-part traces with random nonzero stage values (PR6114 used D_s -> 1) + rng = random.Random('s46-' + name) + receipts = {} + for theta in (F(13, 7), F(19, 11)): + r = A.random_rationals(rng, A.NS) + trace, deltas, free_changes, out_even = A.image_trace(word, theta, r) + need(free_changes == 0, name + ': no free event changes the even rank') + need(deltas[0] == 0, name + ': first paid shear leaves the even rank unchanged') + need(all(d in (0, -1, 1) for d in deltas), name + ': each paid shear moves the even rank by at most one') + need(trace == [n] + [n - max(0, k - 1) for k in range(1, s + 1)], name + ': trace n, n, n-1, ..., 0') + need(all(not any(row) for row in out_even), name + ': all outputs have zero even part in the image') + receipts[str(theta)] = {'even_rank_trace': trace, 'stage_values_sha256': + sha256(','.join(map(str, r)).encode()).hexdigest()} + return {'path': path, 'events': len(word['physical_events']), 'thick': thick, 'thin': thin, + 'paid_shears': s, 'odd_outputs': odd, 'bound_s_minus_1': s - 1, 'row_stage_lifts': cnt['lifts'], + 'output_stage_mass': stage_mass, 'net_q_power': cnt['qpower'], 'targets_rank_sum': targets, + 'paid_lifts_rank': D * cnt['lifts'], 'income': income, 'image_receipts': receipts} + + +def main(): + pinned = authenticate() + result = {'audited_pr': 6114, 'audited_head': '3183c6553e5559df8807fde4fec27e2403f3040a', + 'pinned_inputs': pinned, 'controllers': {}} + for name, path in CONTROLLERS.items(): + result['controllers'][name] = audit_controller(name, path) + c1 = A.laurent_entry_control() + need(c1['entry_even_rank'] == 2 and c1['exceeds_constant_entry_bound'], 'Laurent-entry control twists 2 with 2 shears') + c2 = A.odd_translation_control() + need(c2['odd_rows'] == 1 and c2['final_even_rank'] == 1, 'paid odd translation twists 1 with 1 job') + c3 = A.two_row_job_control() + need(c3['odd_rows'] == 2 and c3['even_rank_before'] - c3['even_rank_after'] == 2, 'two-row job drops rank by 2') + rnd = [A.one_destination_random('s46-%d-%d' % (n, k), w, n, ln) for n, k, w, ln in ((2, 0, 400, 6), (4, 1, 300, 10), (6, 2, 100, 24))] + need(all(r['max_excess_over_bound'] <= 0 for r in rnd), 'one-destination generalization') + result['scope_controls'] = {'laurent_entry_boundary': c1, 'paid_odd_translation': c2, 'two_row_paid_job': c3, + 'one_destination_random': rnd} + text = json.dumps(result, indent=1, sort_keys=True) + '\n' + target = HERE / 'RESULT.json' + if '--write' in sys.argv: + target.write_text(text) + else: + need(target.read_text() == text, 'RESULT.json matches the recomputed audit') + for name, c in result['controllers'].items(): + print('%-27s thick=%d thin=%d shears=%d odd=%d income=%d (=thick-1)' % ( + name, c['thick'], c['thin'], c['paid_shears'], c['odd_outputs'], c['income'])) + print('controls: Laurent entry 2 odd / 2 shears; paid Q 1 odd / 1 job; two-row job 2 odd / 1 job;', + 'one-destination random words %d paid jobs within bound' % sum(r['paid_jobs_total'] for r in rnd)) + print('PASS p104-controller-income-audit') + + +if __name__ == '__main__': + main()