Derive 2,240 idle phase tags and remove 50,337 metadata bytes (no κ)

research/derived-phase-stream/README.md

@@ -0,0 +1,176 @@
+# Derive idle phase translations instead of storing them
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Result
+
+An opt-in metadata emitter and consumer remove all 2,240 stored
+`idle_children[*].translation_after` fields from the pinned DATA-PHASES
+document. The consumer reconstructs the complete legacy document and every
+ordered idle-child record exactly. Using the same canonical JSON encoding,
+the source occupies 814,140 bytes and the new envelope occupies 763,803
+bytes, including its schema and original-document digest. The saving is
+**50,337 bytes**. This counts uncompressed canonical metadata, not compressed
+archive size, runtime, physical storage or a recursive invoice.
+
+Claim type: **finite representation construction with a scoped correctness
+proof**. The result answers the representation part of Open next question 1
+in Ryanson Jonathan / pinterbanget's [PR4466](https://github.com/CrocSwap/integer-mult-bounds/pull/4466).
+The phase formula is that predecessor's result. The new contribution is its
+two-bit-plane implementation, compact producer, legacy-record consumer and
+complete source-instance reduction. No phase identity or predecessor result
+is re-audited as a deliverable.
+
+The source is historical QQ16/P112 data. This package does not install the
+adapter in a physical native caller or change selected PR6030. It removes
+stored values, not the required physical translations. No new kappa follows.
+
+## Construction and proof
+
+The input is a JSON object with dimension `m`, a declared port count and
+ordered recipes. Each recipe contains its port normal `q` and ordered idle
+children. Every child contains its rank, ordered binary row masks and a
+translation. Other metadata is carried through unchanged. The admitted
+schema is bounded in `codec.py`; invalid ranks, duplicate ports, noninteger
+rows, incomplete supported frames and nonorthogonal frames fail explicitly.
+
+Retain PR4466's frame convention. Prepend `q` exactly when the child axes
+meet the first nine port bits. The resulting rows form an orthonormal basis
+on their coordinate support. For each column let `c_i` be its integer count.
+The cited formula is `t_i = [c_i = 3 modulo 4]`. Empty children have tag zero.
+
+The following accumulator evaluates that formula without column counters:
+
+```text
+low = high = 0
+for row in rows:
+    high = high XOR (low AND row)
+    low = low XOR row
+return high
+```
+
+After every prefix, bit `i` of `low` is `c_i modulo 2`; bit `i` of `high`
+is `floor(c_i/2) modulo 2`. Initially this holds for zero counts. Adding a
+row toggles the low bit in its active columns and carries to the high bit
+exactly when the OLD low bit was one. This proves the invariant by induction,
+including wraparound from three to zero. An orthogonal square matrix has
+odd column weights, so its final high bit is precisely the cited tag. This
+is a standard binary counter specialization, not a new phase identity.
+
+For `r` rows of width `m`, synthesis uses exactly `r` ANDs and `2r` XORs on
+two `m`-bit state integers. Input rows, frame validation and document parsing
+are additional work. This operation count is not a physical machine tariff.
+
+`encode` copies the document, verifies that every supplied translation equals
+the derived value, and removes just those fields. It encloses the payload
+with a versioned schema and the SHA256 of the original canonical document.
+`decode` rejects stored translation fields in its compact input, reconstructs
+them from the frames, and checks that digest. For every admitted encoder
+input, every deleted value is therefore restored to the same value; all
+other keys and array orders are preserved. Hence `decode(encode(D)) = D` as
+JSON values. This equality follows from construction, not a hash-collision
+assumption. The digest is a corruption check, not independent authentication.
+
+`events` first validates the complete decoded envelope, then yields
+`(port, child_index, legacy_child)` in original order. No record is released
+before validation finishes. The JSON input and restored document are held
+in memory. "Stream" means the ordered consumer records; this is not an
+incremental constant-memory JSON parser. Object-key ordering and the source
+file's final newline are normalized; byte-exact original whitespace is not
+part of the round-trip contract.
+
+## Evidence and reproduction
+
+CPython 3.12 and its standard library suffice. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/derived-phase-stream/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/derived-phase-stream/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/derived-phase-stream
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/derived-phase-stream --check-source-history
+```
+
+Any CPython 3.12 interpreter can replace the local path. Direct checks accept
+`--scratch EXISTING_DIRECTORY` to contain temporary CLI fixtures. The replay
+prints `PASS_DERIVED_PHASE_STREAM` and a freshly computed receipt bound to
+every package file and live input. It stores no receipt in the checkout.
+
+The exact new-construction checks are:
+
+- The full source document and all 2,240 ordered consumer records round-trip;
+  encoding is stable and the encoder does not mutate its input.
+- A separate column-sum oracle covers every row sequence of length zero
+  through five in widths one through three: 38,877 cases. Four further
+  cases exercise 129 rows at widths 9, 73, 128 and 256.
+- Eighteen API rejection controls cover wrong supplied translations, schema,
+  digest, retained compact fields, invalid or incomplete frames, rank,
+  port normal, unrelated metadata, record order, duplicate JSON keys,
+  input capacity, row capacity, negative masks, overflow and booleans.
+- The real optimized CLI executes encode, decode and ordered events, with
+  byte-for-byte expected canonical output. A malformed envelope exits two
+  with empty stdout before releasing a record.
+
+The full source reconstruction is verification of this new codec, not a
+claim of fresh scientific coverage of the inherited phase identities. No
+predecessor scientific executable is imported or run. [SOURCES.json](SOURCES.json)
+authenticates the live source and the cited question; catalogue and selected
+record pins are historical provenance.
+
+## Limits and code bounds
+
+The universal statement is the scoped encoder/decoder proof above. The byte
+reduction is a finite certificate for this one source document. A new frame
+convention or a partial frame outside the declared coordinate support needs
+a different derivation. The adapter does not infer native admissibility from
+its structural frame checks. It preserves all other source claims as opaque
+metadata and does not certify them.
+
+The CLI accepts at most 2 MiB, 256 ports, 64 children per recipe, 128 supplied
+axes per child and width 256. The port block remains exactly nine bits.
+All explicit loops have these bounds or fixed finite verification domains.
+Functions fit within 60 lines, use no recursion or dynamic code generation,
+and keep checks active under optimization. The CLI reports parse and
+validation errors before writing output. Verification subprocesses have
+30-second timeouts and run only the fixed local codec with the current Python.
+
+Power of Ten rule 3 deviation: Python, JSON and arbitrary-precision integers
+allocate dynamically. Bounded byte sizes, dimensions and fixture counts
+bound live objects; a fixed-allocation implementation is not supplied.
+The JSON decoder's fixed duplicate-key hook and the verifier's fixed
+negative-control callbacks are rule 9 deviations. Warning-strict normal
+and optimized execution provide runtime diagnostics. Ruff is unavailable
+in the local interpreter; no static-analyzer result is claimed.
+
+Physical metadata access, validation, coefficient preparation, routing,
+rounding, restoration, stock/tapes, compiler, full supplier and outer costs
+remain unpriced. All five selected framework assumptions remain. Selected
+cold replay, native replay, Lean and Docker were not run.
+
+## Open next questions
+
+Can one actual native consumer read these reconstructed records without
+recreating the full document? Start with one caller's literal idle-child
+access and count parsing, validation, tag synthesis, data movement and
+restoration. A complete physical caller and its access contract are the
+blockers. This package supplies a legacy-record adapter, not that integration.
+
+## Credit and coordination
+
+Credit Ryanson Jonathan / pinterbanget #4466 for the forced-translation
+formula and explicit construction question; Mihir Srivastava / mihir-s-05
+#4464 and Mark / Matarener #4457 for stage-zero context; ToikY #4002 and
+Chris R / Clear1nsight #3987 for distinct native phase-tag conventions; and
+the retained QQ16/P112, Cinna Davis, zxv, native and compiler lineage.
+Those formulas and their original notices are unchanged. No global
+literature-priority claim is made for counters, derived metadata or JSON.
+
+The `formal-interface-lemma` card changes to this representation side result,
+rather than formalizing a selected assumption. Canonical base is
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8. Selected
+baseline binding orientation passed. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371077).
+The overlap helper covered 521 open PRs and 6,525 Discussion records with
+complete remote pagination. Main/merged object and general-form searches,
+recent account work and local reservations supplemented its sparse local
+notes. Unpublished work and arbitrary diffs remain outside that coverage.
+The first verified representation improvement ends the construction work.

research/derived-phase-stream/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json",
+      "usage": "input",
+      "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70",
+      "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa"
+    },
+    {
+      "path": "research/stage-zero-forced-translation/README.md",
+      "usage": "input",
+      "git_blob": "190333ccb2558a84b89307391082782ef0803ce3",
+      "sha256": "9a9edf851c929db1b9373946c68756f0ffd7224bc9ce2b311d168df0ad2cad46"
+    }
+  ]
+}

research/derived-phase-stream/TASK.json

@@ -0,0 +1,107 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Construct an opt-in derived idle-translation metadata stream and legacy consumer, with exact reconstruction and a finite storage reduction.",
+  "scope_change_reason": "PR4466 explicitly leaves computing translations instead of storing them open. This is a representation construction, not a predecessor audit or a formalization of the selected assumptions.",
+  "bottleneck_link": "Side result: removes redundant historical native phase metadata; it does not improve the binding signed invoice or supply a physical caller.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified complete source round trip with fewer canonical metadata bytes.",
+  "outcome": "completed",
+  "evidence": "814140 canonical source bytes become 763803 including schema and digest; 2240 idle records round-trip; 38877 independent column-sum cases, four capacity cases, eighteen API rejections, three CLI successes and one CLI rejection pass.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can an actual native consumer use derived idle records without restoring the full document?",
+      "why_it_matters": "A physical caller might avoid metadata storage, but this byte reduction does not price its work.",
+      "first_step": "Bind one literal idle-child access and count parsing, validation, synthesis, movement and restoration.",
+      "blocked_by": "Actual native consumer and physical access contract."
+    }
+  ],
+  "claim_type": "finite representation construction with scoped correctness proof",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19371077",
+  "predecessor": {
+    "pr": 4466,
+    "author": "pinterbanget",
+    "head": "496a7d6bd053b7019935529ce5b5c3eb3dc664ed"
+  },
+  "upstream_refresh": {
+    "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+    "priority_revision": 8,
+    "checked_at": "2026-11-03T09:54:37Z"
+  }
+}

research/derived-phase-stream/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json",
+    "research/stage-zero-forced-translation/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Complete new-codec source/consumer round trip, exact byte reduction, independent bit-plane oracle and API/CLI rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete new-construction coverage with optimization enabled."
+    }
+  ]
+}