diff --git a/research/crt-occupied-color-macros/PROOF.md b/research/crt-occupied-color-macros/PROOF.md new file mode 100644 index 0000000000..72e6456316 --- /dev/null +++ b/research/crt-occupied-color-macros/PROOF.md @@ -0,0 +1,114 @@ +# Occupied colors, not all K residues, are the macros + +## Statement + +CRT.md §4 colors targets by current position modulo `K` and charges one +switch layer as `O(K)` colors. The macros that the same paragraph prices +are the occupied colors. On every batch cut by the pinned #4174 layout, + +```text +c ≤ r ≤ r_max, +``` + +where `r` is the number of active targets, `c` is the number of distinct +residues modulo `K`, and `r_max` is that layout's batch cap. Empty residues +are not macros. A same-color pair is one macro. + +At the recomputed production point `d = 65536`, `ell = 24`, alternating +widths `24/23`, this cap is `r_max = 5` and `K = 196608`. The color factor +in the §4 layer sentence may be `5` rather than `196608`. The ratio is the +exact rational `196608/5`. No new κ is claimed. #4100 is not accepted. + +## Definitions + +A batch is a finite set of active target positions. Its target count is `r`. +For an integer `K ≥ 1`, the occupied-color count is + +```text +c = |{ position mod K : position is an active target }|. +``` + +The pinned layout, transcribed from +`research/pr4100-guard-coloring/vendor/pr4174_allocator.py` +(`Layout.__init__`), sets + +```text +logarithm = ceil(log2(p + 2)), +G = 64 (ell + logarithm), +K = 64 G, +r_max = L // (100 G), +H = r_max G, +``` + +with `L` the total width and `p` the precision parameter passed to the +constructor. The constructor cuts each right-child stream into consecutive +groups of at most `r_max` axes, so every batch it emits has `r ≤ r_max`. + +## Lemma 1 + +For any batch and any `K ≥ 1`, `0 ≤ c ≤ min(r, K)`. Also `c = r` if and +only if the `r` residues are pairwise distinct. + +Proof. The residue map sends the `r` targets onto a set of size `c`, so +`c ≤ r`. The codomain has `K` residues, so `c ≤ K`. The map is bijective +onto its image exactly when no two targets share a residue, which is +`c = r`. + +## Lemma 2 + +Every batch emitted by the pinned layout satisfies `c ≤ r_max`. + +Proof. The layout's own cut gives `r ≤ r_max`. Lemma 1 gives `c ≤ r`. + +A collision does not increase the macro count. If two targets differ by a +nonzero multiple of `K`, then `c < r`, so the occupied-color bill is +strictly smaller than one macro per target. The `(K−1)`-bit guard +separation that lets those two targets share one macro is the lemma in +`research/pr4100-guard-coloring`; it is cited, not replayed. + +## Substitution into the §4 cost line + +CRT.md §4 says the coloring "uses `O(K)=O(ell+log p)` colors", that one +color costs `O(V H^(1-a)+V)`, and that with `K` colors and `H≤L=O(p)` one +switch layer costs `O(V p^(1-a) (ell+log p))`. The factor `ell+log p` is +the `O(K)` color count. Replacing that count by the occupied-color count +replaces the layer bound by + +```text +O(c (V H^(1-a) + V)), c ≤ r_max. +``` + +On a layout whose `r_max` and `H` are fixed integers, the color factor is +the integer `r_max`, not the integer `K`, whenever `r_max < K`. + +## Production corollary + +Take `d = 65536`, `ell = 24`, and `p = 6L`, which is the constructor call +in `research/pr4100-guard-coloring/verify.py`. Alternating widths `24, 23, +24, 23, ...` give + +```text +L = 1540096, logarithm = 24, G = 3072, +K = 196608, r_max = 5, H = 15360, +y-bit count = 1494016. +``` + +These are the production row of that package's table. Lemma 2 gives +`c ≤ 5` on every batch, while the written sentence multiplies by +`K = 196608`. The color factors are in the exact ratio + +```text +K / r_max = 196608/5. +``` + +The same constructor with every width `23` (nominal `ell = 24`) gives +`L = 1507328`, the same `K = 196608`, and `r_max = 4`. That is the table's +uniform-`23` row. Its color ratio is the integer `196608/4 = 49152`. + +## What this does not say + +The §5 product `O(V p^(1-a) ell^2 polylog p)` still hides `K` inside the +polylogarithmic factor. This note does not rewrite that line and does not +rerun the 104,864-plan census. It does not build the literal many-target +tape macro, does not change a selected supplier, and does not accept #4100. +The selected conditional exponent stays `605457647/200000000000`. diff --git a/research/crt-occupied-color-macros/README.md b/research/crt-occupied-color-macros/README.md new file mode 100644 index 0000000000..5131057f5e --- /dev/null +++ b/research/crt-occupied-color-macros/README.md @@ -0,0 +1,122 @@ +# Price CRT switch layers by occupied color + +**Scoped tariff lemma. No new κ.** The selected conditional exponent stays +`605457647/200000000000`. #4100 is not accepted. + +## Result + +CRT.md §4 colors active targets by position modulo `K` and charges a switch +layer for `O(K)` colors. The macro that paragraph prices is one occupied +color. For every batch cut by the pinned #4174 layout, + +```text +c ≤ r ≤ r_max. +``` + +Here `r` is the number of active targets, `c` is the number of distinct +residues modulo `K`, and `r_max` is the layout's batch cap. Empty residues +are not macros. Two targets exactly `K` apart are one macro. + +At `d = 65536`, `ell = 24`, and alternating widths `24/23`, with the +constructor call `p = 6L` used by `research/pr4100-guard-coloring`, the +parameters recompute as `L = 1540096`, `K = 196608`, `r_max = 5`, and +`H = 15360`. The §4 color factor may be `5` instead of `196608`. The ratio +is exactly `196608/5`. The all-short width `23` row recomputes as +`r_max = 4` and ratio `49152`. + +The proof is in [PROOF.md](PROOF.md). The singleton-color hypothesis in the +predecessor's open question is sufficient but not necessary: the batch cap +already forces `c ≤ r_max` when a color collides. + +## Scope + +Task card `uniform-transfer-audit`, priority revision 7, base +`32890bc5de034ab8fc93ac88ead7279a6a416d04`. Scope status is **refined**. + +The card asks whether one quantified step of #4100 holds at its caller. +This package prices the occupied-color factor in the CRT.md §4 layer +sentence. It is item 12 of the ordered list below. + +Ordered eligible list for session r44, rebuilt on 2026-10-25 against +`32890bc5de034ab8fc93ac88ead7279a6a416d04`. Open handoffs from the 19 +October index come first. Answered handoffs are dropped. Priority-table +rows come next, and inside `uniform-transfer-audit` the still-open +successors follow the order recorded in +`research/pr4100-ledger-boundary-exponent`: the first still-open successor +of an answered row, then the second. A row is dropped when a merged +package, an open pull request, an excluded unpaidmoon delivery, or a fork +`cursor/*` branch already answers it. + +1. A caller that accepts `(w, q, v_N)` without restoring the original source + slots (discussion comment 19030045). +2. Whether the PR2809 continuation serializer parks the ancestor chain or + one root-sized stream per cut. +3. Whether marker, template, and erased-backing cells sit inside the + `26041 V` budget. +4. Whether the stored narrow band has at most `2p` off-diagonal entries and + the rounding meets `2^{-5p}`. +5. Whether a byte-identical `outer/check_ledger.py` regenerates the + `tau_eff` point. +6. Whether the word-level scalar inventory fits constant one at the two + excluded `p = 2` corners. +7. Whether the full-batch allowance composes with reservoir placement and + the paid repair-key service. +8. Whether the normalized 1-norm stays below the infinity norm on longer + Gaussian paths. +9. An explicit `C` and `k` for `mu ≤ C (W/B) (log p)^k`. +10. A physically costed producer for the 32-bit CRT source ROM. +11. The control cost of the joined producer, scanner, and repair. +12. **This package.** Macros per occupied color, bounded by `r_max`. + +Dropped before this cut: the fresh T385 wrapper, the six-tape head-move +bill, the retiming handoff, the four-provider rebind, the matched +park/restore comparison (open #4167 and #4172), the literal `evaluate_key` +tape service, the separator-corner enclosure and its immediate Neumann +readings, the stack `O_q(V)` claim, and the printed `tau_eff` choice. +Catalogue cards already closed by this account, including the rank-8 +producer, the difference-basis census, the compact-switch audit, and the +stock, replay, packing, and scalar-itinerary cards, stay off the list. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -B research/crt-occupied-color-macros/verify.py +python3 -B scripts/research_package.py --package research/crt-occupied-color-macros +``` + +`verify.py` prints + +```text +PASS_CRT_OCCUPIED_COLOR_MACROS K=196608 r_max=5 ratio=196608/5 uniform23_r_max=4 ratio=49152 same_color_pair_macros=1 no_new_kappa=true +``` + +It hashes CRT.md and the layout allocator, checks the §4 sentences, exhausts +the `2^12` subsets of a 12-point universe at `K = 6`, and recomputes both +production rows. Not run: the 104,864-plan census, Lean, Docker, and the +selected cold replay. + +## Open next questions + +1. Can §5's `ell^2 polylog p` line be rewritten with `r_max` in place of the + hidden `K` factor, and does any later numerical budget use the looser + factor? The first step is to expand `O(log d)` levels times `O(ell)` + layers times `c ≤ r_max` colors. The blocker is that §5 does not display + `K` as a separate multiplier. +2. Does one same-color macro's repair bill stay inside the one-color `O(V)` + when that color holds two targets? The first step is the bad-density line + at `r = 2` and this `K`. The literal many-target tape macro is still + unpinned, so this question does not ask for that program. + +## Credit + +The coloring, the `O(K)` layer sentence, and the one-color cost are Cinna +Davis's #4100. The batch cap `r_max = L // (100 G)` is Hiroki KUMAZAKI's +#4174 layout, as vendored by Ryanson Jonathan in +`research/pr4100-guard-coloring`. That package leaves the occupied-color +price open and proves the `(K−1)`-bit guard lemma cited here. #4321 +(unpaidmoon) stated the disjoint-guard hypothesis that package decided. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. +No independent human review and no formal-kernel acceptance are claimed. diff --git a/research/crt-occupied-color-macros/SOURCES.json b/research/crt-occupied-color-macros/SOURCES.json new file mode 100644 index 0000000000..e07832e9cb --- /dev/null +++ b/research/crt-occupied-color-macros/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/unconditional-batched-crt/CRT.md", + "usage": "input", + "git_blob": "d98dd8e368431cac33d5fc1c8c336696663641d6", + "sha256": "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" + }, + { + "path": "research/pr4100-guard-coloring/vendor/pr4174_allocator.py", + "usage": "input", + "git_blob": "4b3ad89652a28f7d142248d1b5747272e696493c", + "sha256": "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688" + } + ] +} diff --git a/research/crt-occupied-color-macros/TASK.json b/research/crt-occupied-color-macros/TASK.json new file mode 100644 index 0000000000..f11195c525 --- /dev/null +++ b/research/crt-occupied-color-macros/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Replace the CRT.md section-4 switch-layer factor O(K) by the occupied-color count, and prove that count is at most the pinned layout batch cap r_max.", + "scope_change_reason": "The card asks for one quantified #4100 implication at its caller. This is the unblocked occupied-color price left by research/pr4100-guard-coloring, the still-open many-target macro tariff. It does not build a tape macro, replay the production census, or accept #4100.", + "bottleneck_link": "Side result under the retained #4100 transfer audit. A tighter color factor does not change the selected exponent; unknown tape and repair costs stay unknown.", + "budget_minutes": 60, + "stop_rule": "Stop once the occupied-color inequality and the recomputed production ratios are checked. Do not rerun the 104864-plan census or write a many-target tape program.", + "outcome": "completed", + "evidence": "PROOF.md lemmas and verify.py: CRT.md and allocator hashes, section-4 sentences, 4096-subset residue census, production rows K=196608 with r_max=5 and r_max=4.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance for the proof, verifier, and package text. No independent human or formal-kernel acceptance.", + "open_questions": [ + { + "question": "Can the section-5 ell^2 polylog p line be rewritten with r_max in place of the hidden K factor?", + "why_it_matters": "The layer sentence is tighter, but the aggregate still hides K, so a later numerical budget may keep the loose factor.", + "first_step": "Expand O(log d) levels times O(ell) layers times c <= r_max colors and compare with the written aggregate.", + "blocked_by": "Section 5 does not display K as a separate multiplier." + }, + { + "question": "Does one same-color macro's repair bill stay inside the one-color O(V) when that color holds two targets?", + "why_it_matters": "Occupied-color pricing charges one macro for a collision; the repair term might still grow with the target count.", + "first_step": "Instantiate the bad-density line at r = 2 and K = 196608.", + "blocked_by": "The literal many-target tape macro is not pinned, and this question does not ask for it." + } + ] +} diff --git a/research/crt-occupied-color-macros/VERIFY.json b/research/crt-occupied-color-macros/VERIFY.json new file mode 100644 index 0000000000..e6f0f3577f --- /dev/null +++ b/research/crt-occupied-color-macros/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/unconditional-batched-crt/CRT.md", + "research/pr4100-guard-coloring/vendor/pr4174_allocator.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "CRT.md and allocator hashes, the K-color sentence, the 4096-subset lemma, and both recomputed production rows." + } + ] +} diff --git a/research/crt-occupied-color-macros/verify.py b/research/crt-occupied-color-macros/verify.py new file mode 100644 index 0000000000..28d095bf28 --- /dev/null +++ b/research/crt-occupied-color-macros/verify.py @@ -0,0 +1,163 @@ +#!/usr/bin/env python3 +"""Occupied CRT colors are at most the layout batch cap.""" + +import hashlib +from fractions import Fraction +from itertools import combinations +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +CRT = ROOT / "research/unconditional-batched-crt/CRT.md" +ALLOCATOR = ROOT / "research/pr4100-guard-coloring/vendor/pr4174_allocator.py" +CRT_SHA = "02c3a1e38cbee25aefe2640cc72676da62ba10eb7519fbcb9adb9d48b74eff2b" +ALLOCATOR_SHA = "b764195fc6291e3c8fa8297b1f4ceaefc119d5664d8ff348b49eac8a2e79c688" + +COLOR_SENTENCE = ( + "Color targets by current position modulo K, so guard intervals are disjoint.\n" + "This uses O(K)=O(ell+log p) colors." +) +ONE_COLOR_SENTENCE = ( + "One color uses O(1) ordinary H-bit interchanges plus linear scans and paid\n" + "repair. It costs O(V H^(1-a)+V). With K colors and H<=L=O(p), one switch\n" + "layer costs O(V p^(1-a) (ell+log p)), including placement and restoration." +) +SECTION_FIVE = "O(V p^(1-a) ell^2 polylog p)." +FORMULA_LINES = ( + "guard_digit_bits = 64 * (ell + logarithm)", + '("K", 64 * guard_digit_bits)', + '("r_max", maximum_batch)', + "maximum_batch = length // (100 * guard_digit_bits)", + "active = tuple(islice(axes, layout.r_max))", +) + + +def fail(message): + raise SystemExit("FAIL_CRT_OCCUPIED_COLOR_MACROS " + message) + + +def sha256(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def ceil_log2(value): + if value < 1: + fail("logarithm argument") + exponent = 0 + power = 1 + while power < value: + power *= 2 + exponent += 1 + return exponent + + +def layout(ell, widths): + """The pinned Layout arithmetic. p = 6L, as in the coloring census.""" + length = sum(widths) + precision = 6 * length + logarithm = ceil_log2(precision + 2) + if ell < logarithm: + fail("ell below ceil(log2(p+2))") + guard = 64 * (ell + logarithm) + batch_cap = length // (100 * guard) + if batch_cap < 1 or 100 * batch_cap * guard > length: + fail("layout rejected its own volume bound") + return { + "L": length, + "logarithm": logarithm, + "G": guard, + "K": 64 * guard, + "r_max": batch_cap, + "H": batch_cap * guard, + } + + +def occupied(positions, modulus): + return len({position % modulus for position in positions}) + + +def check_phrases(crt, allocator): + if COLOR_SENTENCE not in crt or ONE_COLOR_SENTENCE not in crt: + fail("CRT.md no longer states the K-color layer charge") + if SECTION_FIVE not in crt: + fail("section 5 aggregate is missing") + if "occupied" in ONE_COLOR_SENTENCE or "r_max" in ONE_COLOR_SENTENCE: + fail("the written one-color sentence already prices the cap") + for line in FORMULA_LINES: + if line not in allocator: + fail("allocator no longer defines " + line) + + +def check_color_lemma(): + modulus = 6 + universe = range(12) + checked = 0 + for size in range(len(universe) + 1): + for subset in combinations(universe, size): + count = occupied(subset, modulus) + if count > min(size, modulus): + fail("occupied colors exceeded min(r, K)") + distinct = len({position % modulus for position in subset}) == size + if (count == size) != distinct: + fail("equality c = r disagreed with distinct residues") + checked += 1 + if checked != 2**12: + fail("subset census changed size") + if occupied((0, modulus), modulus) != 1: + fail("targets K apart did not share a color") + if occupied((0, 1, modulus), modulus) != 2: + fail("a third residue was lost") + if occupied(range(modulus), modulus) != modulus: + fail("a full set of residues was not K colors") + # A per-target bill on a collision, or a per-residue bill on a singleton, overcharges. + if not (occupied((0, modulus), modulus) < 2 and occupied((0,), modulus) < modulus): + fail("control: the overcharging bills were not strict") + + +def check_production(): + alternating = layout(24, tuple(24 if index % 2 == 0 else 23 for index in range(65536))) + expect = {"L": 1540096, "logarithm": 24, "G": 3072, "K": 196608, "r_max": 5, "H": 15360} + if alternating != expect: + fail("production layout " + str(alternating)) + y_bits = (alternating["L"] - alternating["H"]) - 2 * alternating["H"] + if y_bits != 1494016: + fail("production y-bit count") + if alternating["K"] * 1 <= alternating["r_max"]: + fail("the cap did not tighten the color factor") + if Fraction(alternating["K"], alternating["r_max"]) != Fraction(196608, 5): + fail("production ratio") + uniform_short = layout(24, tuple(23 for _ in range(65536))) + if uniform_short["L"] != 1507328 or uniform_short["K"] != 196608 or uniform_short["r_max"] != 4: + fail("uniform ell-1 layout " + str(uniform_short)) + if uniform_short["K"] // uniform_short["r_max"] != 49152: + fail("uniform ell-1 ratio") + # The cap binds collisions as well as singletons. + for positions, residue_count in (((0, alternating["K"]), 1), ((0, 1), 2)): + if occupied(positions, alternating["K"]) != residue_count: + fail("production residue example") + if residue_count > alternating["r_max"] and len(positions) <= alternating["r_max"]: + fail("a legal batch exceeded the cap") + + +def main(): + crt_bytes = CRT.read_bytes() + allocator_bytes = ALLOCATOR.read_bytes() + if sha256(CRT) != CRT_SHA or hashlib.sha256(crt_bytes).hexdigest() != CRT_SHA: + fail("CRT.md hash") + if sha256(ALLOCATOR) != ALLOCATOR_SHA: + fail("allocator hash") + crt = crt_bytes.decode() + allocator = allocator_bytes.decode() + check_phrases(crt, allocator) + check_color_lemma() + check_production() + print( + "PASS_CRT_OCCUPIED_COLOR_MACROS " + "K=196608 r_max=5 ratio=196608/5 " + "uniform23_r_max=4 ratio=49152 " + "same_color_pair_macros=1 " + "no_new_kappa=true" + ) + + +if __name__ == "__main__": + main()