research/lockstep-live-role-audit: live roles in the lockstep compiler and the #4470 outer constant C (no new κ)

research/lockstep-live-role-audit/README.md

@@ -0,0 +1,135 @@
+# Live roles in the lockstep compiler, and the #4470 outer-reserve constant
+
+**Audit with a positive scoped result; no new κ.** The selected κ is unchanged.
+
+Base: `b58ad9ef4`. This package answers the two open questions of our
+`research/bit-row-stock-atom-audit` package (#4612):
+
+1. Does the finite lockstep compiler give every simultaneously live child role
+   a distinct physical array? This is DELAYED-COVER-BRIDGE open question 1.
+   Both the delayed BIT cover and the row-digit reserve argument assume it.
+2. What is the outer-reserve constant `C` of OUTER-TRANSFER-AUDIT §5 for the
+   actual #4470 templates?
+
+## 1. Live roles in the lockstep compiler
+
+**Why it matters.** The delayed cover routes a child target role by
+`x_g -> y_{gS}` on the *whole* cover fiber of its physical array
+(DELAYED-COVER-BRIDGE §3). Suppose two roles that are live at the same level
+sat on one array and needed different matchers. Their routes would then
+conflict on a single fiber. Nested roles are harmless: a child role sits on the
+array of the job its suspended parent issued, so the routes compose as
+`g -> gS1 -> gS1S2` and are undone in LIFO order.
+
+**What already existed.** `transfer-audit/finite_dag_audit.py` checks that the
+input fields inside each class are distinct, and it counts batches. It does not
+execute the schedule across classes. It also does not execute replication,
+source complements or exit substitution at field level, and it does not run any
+BIT-shaped rule.
+
+**What is checked here.** `live_roles.py` is an independent implementation of
+the FINITE-PRECOMPILATION compiler. It covers the Theorem 1G lockstep flow, `a`
+lockstep replicas, source complements, and exit batches substituted by the
+smaller uniform program. It **executes** the compiler event by event. For every
+physical field (productive array or owned center) it keeps the stack of live
+roles: a push is one whole-fiber route and a pop is its inverse. At every event
+it checks:
+
+| Invariant | Meaning |
+|---|---|
+| I1 | The roles and owned centers of the units in one class lie on pairwise distinct fields. |
+| I2 | A child role enters a field only when the top of that field's stack is the suspended parent that issued the job, and only at equal rank (whole-job substitution). A source enters on its program's array. |
+| I3 | A unit issues a paid job only on a field whose top is itself, and never while its previous child class is live. The jobs of one round lie on distinct fields. |
+| I4 | Every pop is LIFO. After every class and every program, all stacks are exactly as they were on entry. |
+| I5 | Exit and complement batches hand `B_e` distinct fields to the smaller program, each still owned by its issuer. |
+| I6 | Every top-level array receives exactly one complement and exactly one source job. |
+
+Results (`verify.py`):
+
+- Counting reproduces the repository receipt: the toy rule at rank 40 gives
+  `B = 91,854` and `P = 2,242,264`, and the actual complex p2 rule at rank 41
+  gives `B = 1397` and `P = 57,149`.
+- All cases pass:
+  - the toy rule at `N = 4..64`, with full width executed up to `N = 40`
+    (6.9M events, 88,687 nested programs executed);
+  - BIT-shaped rules with target ranks `{8, 22, 50}` and paid ranks `1..7` (the
+    BIT p3 rank sets with reduced multiplicities), random owner chronologies and
+    two adversarial ones (every round on one role; every round on the owned
+    center), at `N = 50, 400, 3200, 25600`, up to three generations;
+  - the actual complex p2 rule with its native owner order.
+- Where the width is astronomical (`B` up to about `10^254`), two lockstep
+  replicas are executed, and the smaller programs are checked through their
+  interface (I5 plus a LIFO push/pop).
+- Rejecting controls (`test_verify.py`):
+  - one owned center per recursion depth, instead of one per unit instance,
+    is rejected. This is the allocation that FINITE-PRECOMPILATION §6 already
+    calls insufficient.
+  - an eager parent that issues round `j+1` before child class `j` finishes is
+    rejected.
+  - an exit batch that repeats a field is rejected.
+
+**General argument.** Induct over the events.
+
+- Sources are fresh arrays.
+- Each unit issues exactly one job per round, on a field it currently owns.
+- The units of a class own pairwise distinct fields when the class starts.
+- Owned centers are allocated per unit instance.
+
+Hence the roles of the next class again lie on distinct fields, and the live
+roles on any one field form a chain parent → child → … . Lockstep suspension
+pops that chain before the parent issues again. This is exactly the
+nested-route structure that the delayed cover needs.
+
+The #4470 compiled unit is a 1024-fold product with completion and splitting
+(higher-moment-strictification). The product is itself a two-level lockstep
+substitution: `B_V` copies of `U`, one job per copy per paid position, and never
+two paid positions of one suspended copy. Splitting and completion add
+sequential paid rounds on the same owner. The generic rule format here covers
+these. The 1024-fold word itself is not materialized, so its owner chronology is
+represented only by BIT-shaped rules of the same structure.
+
+## 2. The outer-reserve constant C for #4470
+
+`constant_c.py` bounds `C` in `q0(h,p) <= C(log2 h + h^δ (log2 p)^3 + 1)`
+(δ = 0.004). The inputs are the #4440 BIT ranks that #4470 keeps (`N_b = 2^25986965159937`) and the
+#4470 complex word (`v = 1024`, `N_c = 2^64215200000000`), together with the
+#4436 nested widths `B_N <= C_N^N`. Every rounding is upward.
+
+| Quantity | Bound |
+|---|---|
+| BIT share | `log2 <= 51,973,930,319,885` |
+| Complex share | `log2 <= 64,215,200,000,086` (at least `2^64215199999954` in the same realization) |
+| **C** | **`log2 C <= 64,215,200,000,088`** |
+| `H(p) = [1024 C L^3]^(1/(1-δ))` fits the group width `p^β` | from `log2 p = 64,473,100,659,114` (#4612's illustrative value was `5.2·10^13`) |
+
+The complex row stock dominates, by more than `10^13` bits. With the #4440
+complex word instead, the fit point would be `1.05·10^16`. For this `C` the
+displayed `H` already dominates the #4618 term `4096 C log2(4096 C)`, and
+`q0 <= h/512` holds at `h = H` for every tested `L`. Two coefficients are
+inherited, not re-derived: the complex row proportionality `c_row <= 2^64` and
+the old-supplier stock `A_old <= 2^64`.
+
+## Replay
+
+```sh
+python3.12 -B research/lockstep-live-role-audit/verify.py
+python3.12 -B research/lockstep-live-role-audit/test_verify.py
+```
+
+## Open next questions
+
+1. Derive the two inherited coefficients of `C` (`c_row <= 2^64`,
+   `A_old <= 2^64`) from the #4470 sources. They affect only lower-order bits
+   of `log2 C`.
+2. Emit the raw #4440 BIT paid-owner list and confirm the two local premises
+   of the live-role argument (one job per round on a currently owned field;
+   per-instance owned centers) for a `v = 2` product. The argument needs
+   nothing else from the native word.
+
+## Credit
+
+zxv for #4359, the delayed-cover bridge and the finite compiler; Jacob Alan
+Sussman for the Theorem 1G flow; Cinna Davis for the #4440/#4470 chain;
+the transfer-audit authors for `finite_dag_audit.py`, whose counting this
+package reproduces. Prepared by Mark (Matarener) with substantial Claude Code
+(Claude) assistance. Apache-2.0.

research/lockstep-live-role-audit/SOURCES.json

@@ -0,0 +1,84 @@
+{
+  "schema_version": 1,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "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/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md",
+      "usage": "input",
+      "git_blob": "ae676a6504cc7987863da1827551c18e7ec20ce1",
+      "sha256": "c41a2571b9c4c1d7920633f10c3ed2c74da39ca3bc8d6a910e6ffed380327413"
+    },
+    {
+      "path": "research/higher-moment-strictification/README.md",
+      "usage": "input",
+      "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3",
+      "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d"
+    },
+    {
+      "path": "research/joint-helper-lattice/RESULT.json",
+      "usage": "input",
+      "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596",
+      "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21"
+    },
+    {
+      "path": "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md",
+      "usage": "input",
+      "git_blob": "4badb40f0919c515823cb07e44c6470d4d6469ca",
+      "sha256": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md",
+      "usage": "input",
+      "git_blob": "a58774e237c9362869a60a22bda35be09fb85872",
+      "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443"
+    },
+    {
+      "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz",
+      "usage": "input",
+      "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c",
+      "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39"
+    },
+    {
+      "path": "research/kappa-rebuild/controller/GLOBAL-IDENTITY-COVER.json.gz",
+      "usage": "input",
+      "git_blob": "d79363206474ea0f9a3600df1a530a6b50ea1177",
+      "sha256": "c4a3103c85d0d7fc1a253e117c238e00945c938877e27fcdc98c0dd18cc3e2c5"
+    },
+    {
+      "path": "research/kappa-rebuild/transfer-audit/AUDIT.md",
+      "usage": "input",
+      "git_blob": "ee8c49a3450f812011eb3f7f40c25f5ade26b2d0",
+      "sha256": "032488343667d19613cab84df5dad554cfd2a283fb4fc0d4c9b4d165cfa04669"
+    },
+    {
+      "path": "research/kappa-rebuild/transfer-audit/FINITE-DAG-AUDIT.json",
+      "usage": "input",
+      "git_blob": "45e5bc924bcbfc5544ed206c44e457baebfbc81c",
+      "sha256": "5965986a93f611fdc6bb9fc0a47820385df57e49e2d7edccc257b14deb0f7085"
+    },
+    {
+      "path": "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md",
+      "usage": "input",
+      "git_blob": "e8b7ef8956ece5bd493cbf52113916e5dc288535",
+      "sha256": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779"
+    },
+    {
+      "path": "research/query-thinned-controllers/RESULT.json",
+      "usage": "input",
+      "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c",
+      "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f"
+    }
+  ]
+}

research/lockstep-live-role-audit/TASK.json

@@ -0,0 +1,88 @@
+{
+  "schema_version": 1,
+  "task_id": "selected-stock-envelope",
+  "priority_revision": 7,
+  "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51",
+  "original_card": {
+    "id": "selected-stock-envelope",
+    "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?",
+    "starting_points": [
+      "research/selected-bootstrap-stock-audit/README.md",
+      "research/bootstrap-cutoff-time-space-split/README.md",
+      "certificates/selected-result.json",
+      "docs/research/community-efficient1000-review.md",
+      "research/stock-margin-chain/README.md"
+    ],
+    "methods": [
+      "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.",
+      "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope."
+    ],
+    "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.",
+      "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."
+    },
+    "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.",
+    "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.",
+    "allowed_variations": [
+      "One stage or one explicit reserve/depth implication.",
+      "An independently checked same-domain proof repair, retaining all remaining assumptions."
+    ],
+    "scope_change_triggers": [
+      "Importing the historical 57604 or 252 allowance without a selected-producer binding.",
+      "Calling a conditional fit lemma a full outer-proof adoption.",
+      "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality."
+    ],
+    "overlap_terms": [
+      "selected stock",
+      "stock envelope",
+      "bootstrap cutoff",
+      "1956",
+      "1965",
+      "1990",
+      "2972",
+      "stock-margin-chain",
+      "actual_stock_coefficient"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.",
+        "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation",
+        "remaining": "Derive one actual reserve/depth coefficient from the selected producer.",
+        "status": "reviewed",
+        "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Ownership of simultaneously live child roles in the FINITE-PRECOMPILATION lockstep compiler (DELAYED-COVER-BRIDGE open question 1), and the outer-reserve constant C of OUTER-TRANSFER-AUDIT s5 bound to the #4470 templates.",
+  "scope_change_reason": "These are the two open questions left by the #4612 stock audit of the selected #4359/#4470 producer.",
+  "bottleneck_link": "Side result for the selected-result audit: removes an ownership assumption under the delayed BIT cover and makes the outer thresholds explicit; it does not move the frontier.",
+  "budget_minutes": 180,
+  "stop_rule": "Stop after event-level execution of the compiler with live-role stacks on toy, BIT-shaped and actual complex p2 rules, and after the explicit C bound; do not materialize the 1024-fold winning word.",
+  "outcome": "completed",
+  "evidence": "README.md; verify.py binds the source statements, recomputes C and executes the compiler with invariants I1-I6; test_verify.py has rejecting controls (per-depth owned centre, eager parent, repeated exit field).",
+  "author": "Mark (Matarener)",
+  "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.",
+  "open_questions": [
+    {
+      "question": "Can the inherited coefficients c_row <= 2^64 and A_old <= 2^64 in C be derived from the #4470 sources?",
+      "why_it_matters": "They are the only non-derived factors in the explicit C; they change only lower-order bits of log2 C.",
+      "first_step": "Trace the complex row proportionality (old lineage 20,161 per role-bit level) through the #4470 complex compiler.",
+      "blocked_by": "none"
+    },
+    {
+      "question": "Does the actual 1024-fold #4470 owner chronology satisfy the two local premises (one job per round on a currently owned field; per-instance centres)?",
+      "why_it_matters": "The live-role argument is generic in the owner chronology; only these premises are needed from the native word.",
+      "first_step": "Emit the raw #4440 BIT paid-owner list and check the premises for the v=2 product.",
+      "blocked_by": "none"
+    }
+  ]
+}

research/lockstep-live-role-audit/VERIFY.json

@@ -0,0 +1,39 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md",
+    "research/higher-moment-strictification/README.md",
+    "research/joint-helper-lattice/RESULT.json",
+    "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md",
+    "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md",
+    "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz",
+    "research/kappa-rebuild/controller/GLOBAL-IDENTITY-COVER.json.gz",
+    "research/kappa-rebuild/transfer-audit/AUDIT.md",
+    "research/kappa-rebuild/transfer-audit/FINITE-DAG-AUDIT.json",
+    "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md",
+    "research/query-thinned-controllers/RESULT.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Bind source statements; explicit #4470 constant C and fit point; compiler counting equals FINITE-DAG-AUDIT receipts; event-level lockstep execution with live-role stacks (I1-I6) on toy, BIT-shaped and actual complex p2 rules."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/test_verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Rejecting controls: owned centre per depth, eager parent, exit batch repeating a field; unmutated rules pass; BIT share alone understates the threshold."
+    }
+  ]
+}