diff --git a/research/phase-rank-debt/PROOF.md b/research/phase-rank-debt/PROOF.md new file mode 100644 index 0000000000..544ff45127 --- /dev/null +++ b/research/phase-rank-debt/PROOF.md @@ -0,0 +1,155 @@ +# Phase gains must pay their own concave rank debt + +Prepared by Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. + +## Statement and scope + +Consider the frozen PR4610 word and the symmetric-bilinear-form grammar +described in Dugongue's PR4654 and Cinna Davis's PR4665. Retain its subspaces, +scalar order and coefficients, logical warp maps, and all main and explicit +adapter boundaries. Scalar operands must still meet in one common chart. +Allow arbitrary symmetric forms at the helper boundaries and intermediate +charts, including the owned-center contacts. Allow **increased paid ranks** +and new paid corrections at formerly rank-zero transitions. + +Pay each changed single-field contact block at its actual Fourier rank. Keep +the owned center uncredited. This model does not introduce a shared paid +instruction on several field owners, change the main operator, change the +subspaces or scalar graph, or delete a source operation. + +For every such legal deformation and every 0 <= t <= 1, let T_t and P_t +denote the complete productive and paid rank moments, omitting rank-zero +jobs. Then + + T_t(new) - P_t(new) <= T_t(old) - P_t(old). + +Thus paid phase corrections cannot improve the recursive moment of this +fixed word. Applying the same replacement in an unchanged path controller +cannot improve its complete moment either. This is a scoped cost theorem, +not a universal obstruction to phases, new native suppliers or higher K. + +The phase grammar is a premise: a nested transition U subset W with forms +b_U,b_W has rank + + dim(W)-dim(U) + rank((b_U+b_W)|U). + +More generally, for G U subset W the rank is dim(W)-dim(U) plus the +rank of b_in + G^* b_out on U. This includes an originally monomial warp +as the equal-dimension case. All added ranks are nonnegative. +Absolute-phase implementation and the all-column native theorem are not +re-proved here. The argument is conditional on these exact rank formulas; +it is not justified by ordinary rational matrix rank alone. + +## 1. The exact word has monotone paths, including its logical warps + +For each persistent field, every paid transport strictly increases its +subspace. A logical warp maps its complete old subspace isomorphically to +its new subspace, preserving dimension. Consequently the sum of old paid +ranks on field i is + + h_i = dim(final_i)-dim(initial_i). + +The verifier reconstructs these paths directly from the complete forward +and backward words, checks every scalar contact and center transport, and +recounts the full paid profile + + {1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}. + +For all 408 helpers the endpoint spaces are nested and h_i>0. Their ranks +are {4:28,7:7,8:47,9:326}, with total 3471. Every composed logical warp +fixes that helper's entrance space pointwise. This last assertion is +checked as a map on every entrance basis vector, rather than inferred +from endpoint dimensions. Each old paid step r_ij therefore satisfies +0 <= r_ij <= h_i. Rank-zero contacts and logical warps may be included +as additional steps with r_ij=0. + +For the cost comparison use the blocks between consecutive scalar contacts +on each helper, also cutting at fixed adapters and the two endpoints. +Operations on other owners commute with a block until its next scalar +contact. A block may include logical warps and can be refactored as one +whole job; the proof does not charge a separate phase correction when it +can be absorbed into that job's monomial normalizers. The verifier checks +that every original helper block contains **at most one positive paid +call**. Consequently its original moment is exactly r_ij^t, with r_ij=0 +when it was wholly monomial. Transported entrance spaces stay nested +through the entire block, so the generalized rank formula applies to +the block's composed G. Every r_ij is still bounded by h_i. Fusing across +a scalar contact or introducing a shared multi-owner operation changes +the model and is outside this theorem. + +## 2. Helper rank gain is bounded by its own added paid ranks + +Fix a helper and transport its entrance space along its actual field path: +use inclusion at an ascending step and G at a logical warp. Pull each +intermediate symmetric form back to this fixed entrance space. At a +common scalar contact there is a single form, so no discontinuity occurs. +At a contact block, the rank of the difference between +the two pulled-back forms is at most its added paid rank delta_j: +restriction cannot increase bilinear-form rank. + +The sum of these differences telescopes. Because the final composed warp +fixes the entrance pointwise, its sum is exactly the helper endpoint +difference form. The grammar gives the new helper rank h+g, where g is +the rank of that difference. Rank subadditivity yields + + g <= sum_j delta_j. + +This also allows new corrections at previously equal charts. Such a +correction is not a free phase change: its old rank is zero and its +positive new rank must be paid. Corrections to fixed adapters, if needed +inside a proposed implementation, must likewise be paid; omitting them +does not invalidate this necessary lower bound. + +## 3. Concavity prices that debt at least as highly as its reward + +Let h>0, 0<=r_j<=h, delta_j>=0, D=sum delta_j and 00. +For each step, using the improper integral at zero when necessary, + + (r_j+delta_j)^t-r_j^t + = integral_(0..delta_j) t(r_j+u)^(t-1) du + >= integral_(0..delta_j) t(h+D_j+u)^(t-1) du. + +Summing gives + + sum_j [(r_j+delta_j)^t-r_j^t] + >= (h+D)^t-h^t + >= (h+g)^t-h^t. + +Thus every helper's added productive moment is at most the increase in +paid moment on that same helper's path. These paths have distinct paid +field owners, even where their scalar contacts share a chart; no paid +occurrence is charged to two helpers. Main boundaries are fixed, so their +productive moments do not increase. Added main and center costs are +nonnegative. Summing proves the claimed inequality. + +At t=0, every helper already has positive rank, so its productive job +count is unchanged. An old positive paid step stays positive, while a +corrected zero step adds a paid job. Therefore the inequality also holds +at t=0 with rank-zero jobs omitted. At t=1 it is just the rank-debt bound. + +For an unchanged controller, each full native call gets the same fixed +main operator and its own independent helper inventory. Apply the local +inequality per invocation; thin queries, idle calls and all other main +contributions stay as prescribed by that controller. No controller +optimality theorem or outer-transfer assumption is required for this +comparison. A new controller or a change to its main contract is outside +the statement. + +## Verification boundary + +The analytic argument above covers all exponents and every legal form +assignment. Computation checks the exact source-specific hypotheses, not +an exhaustive search of phase assignments. It also exhausts the 512 triples +of symmetric forms on F_2^2 to check the endpoint rank triangle, proves two +strict square-root comparisons with outward rational intervals, rejects +four mutations of the actual word, and changes every frame basis without +changing the certificate. These are author checks, not a formal proof or +independent human verification. + +PR4665's homogeneous zero-solution certificate is a predecessor with a +different scope. This proof does not need every form to vanish. In +particular it permits paid rank increases and arbitrary compatible center +forms. An exploratory relaxation of its owned-contact freezes left 288 +coordinates on empty center resets and no nonzero helper difference; +that experiment is motivation only and is not a premise of this theorem. diff --git a/research/phase-rank-debt/README.md b/research/phase-rank-debt/README.md new file mode 100644 index 0000000000..51906b7b21 --- /dev/null +++ b/research/phase-rank-debt/README.md @@ -0,0 +1,70 @@ +# Paid phase changes cannot improve the frozen word's concave moment + +**Scoped cost theorem; no higher K.** On Cao Yifan's PR4610 word, changing +symmetric phase forms cannot improve any complete recursive moment +`T_t-P_t`, for every `0 <= t <= 1`, under the fixed-graph contracts below. +This includes paid rank increases, new rank-zero-to-positive corrections, +and compatible phases on the owned-center contacts. It does not require +all phase forms to vanish. + +For each helper, the added endpoint rank `g` is bounded by the sum of its +own added paid ranks. Every original paid contact block has rank at most +that helper's endpoint rank `h`. Concavity then forces + +``` +paid moment increase >= (h+g)^t-h^t. +``` + +[PROOF.md](PROOF.md) proves the all-assignment, all-exponent statement. +[RESULT.json](RESULT.json) records exact checks of its source-specific +hypotheses on both orientations, all 632 persistent paths and 408 helpers. +The eight owned rank-eight center jobs remain paid and uncredited. + +This extends the question left open by +[PR4665](https://github.com/CrocSwap/integer-mult-bounds/pull/4665): that +certificate froze owned contacts and required unchanged paid ranks. Here +paid phase corrections are permitted and priced, and the obstruction is a +moment inequality rather than a homogeneous zero-solution certificate. +The rank formulas come from +[PR4654](https://github.com/CrocSwap/integer-mult-bounds/pull/4654)'s phase +chart grammar. Their native and absolute-phase theorem is a premise. + +Keep the subspaces, scalar graph/order/coefficients, main operator and +explicit adapter boundaries fixed. Each scalar contact uses one common +chart. Phase corrections can be absorbed into a contact block's whole-job +normalizers; a correction is not charged separately when such absorption +is available. Each helper block has at most one original paid call, checked +from the actual word. Shared multi-owner paid operations, fusion across a +scalar contact, changed endpoints and new center protocols are outside scope. +This does not rule out higher K from a different construction. + +## Reproduce + +``` +python3.12 -B scripts/research_package.py --package research/phase-rank-debt +``` + +The standard-library verifier authenticates original PR4610 bytes (retained +by PR4665), checks all path/rank/warp hypotheses, exhausts 512 small symmetric +form triangles, certifies strict concavity examples with rational intervals, +rejects four source mutations and checks independent changes to every frame +basis. It uses explicit checks that remain enabled under `-O`. +Direct exported replay is `python3.12 -I -B verify.py` from this directory. +No native all-column, outer, selected cold replay or formal kernel run is +claimed. The selected conditional K at the pinned base is still .00302015. + +## Open next questions + +A useful phase construction must change at least one hypothesis of this +cost theorem. One concrete option is a shared multi-owner correction across +a scalar contact: freeze the smallest actual contact, write its complete +arbitrary-input operator and compare its paid rank with the sum of separate +corrections. A formal shared rank or relaxed output flag is insufficient; +the field owners, return contract and physical bill are the missing work. +The structured questions and stopping rule are in [TASK.json](TASK.json). + +Prepared by Cinna Davis with substantial OpenAI Codex assistance; Apache-2.0. +Credit Dugongue/PR4654 for the phase grammar; Cao Yifan/PR4610 for the word; +Cinna Davis/PR4665 for its previous rigidity question; Cinna Davis/PR4470, +zxv, Jacob Alan Sussman and the retained native/helper/compiler contributors. +Original bytes, Git blob and commit/path provenance are in SOURCES.json. diff --git a/research/phase-rank-debt/RESULT.json b/research/phase-rank-debt/RESULT.json new file mode 100644 index 0000000000..809f83207c --- /dev/null +++ b/research/phase-rank-debt/RESULT.json @@ -0,0 +1,93 @@ +{ + "controls": { + "all_frame_basis_changes": true, + "source_mutations_rejected": [ + "wrong_width", + "missing_center", + "wrong_warp", + "wrong_helper_endpoint" + ], + "strict_concave_increment_and_missing_hypothesis": true, + "symmetric_form_rank_triangles": 512 + }, + "no_new_kappa": true, + "orientations": { + "backward": { + "events": { + "adapter": 448, + "center": 8, + "climb": 3290, + "phase": 10, + "scalar": 17453, + "warp": 240 + }, + "helper_contact_blocks_by_original_paid_calls": { + "0": 19817, + "1": 2208 + }, + "helper_maximum_paid_step": { + "1": 34, + "2": 61, + "3": 251, + "4": 50, + "5": 12 + }, + "helper_path_rank_mass": 3471, + "helper_ranks": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "persistent_paths_with_exact_rank_telescope": 632, + "pointwise_fixed_helper_entrances": 408 + }, + "forward": { + "events": { + "adapter": 448, + "center": 8, + "climb": 3290, + "phase": 10, + "scalar": 17453, + "warp": 240 + }, + "helper_contact_blocks_by_original_paid_calls": { + "0": 19817, + "1": 2208 + }, + "helper_maximum_paid_step": { + "1": 34, + "2": 61, + "3": 251, + "4": 50, + "5": 12 + }, + "helper_path_rank_mass": 3471, + "helper_ranks": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "persistent_paths_with_exact_rank_telescope": 632, + "pointwise_fixed_helper_entrances": 408 + } + }, + "status": "FIXED_WORD_PHASE_CHANGES_CANNOT_IMPROVE_ANY_CONCAVE_MOMENT" +} diff --git a/research/phase-rank-debt/SOURCES.json b/research/phase-rank-debt/SOURCES.json new file mode 100644 index 0000000000..d54e85d2c3 --- /dev/null +++ b/research/phase-rank-debt/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/phase-rank-debt/inputs/round3-native.json.gz", + "usage": "input", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e", + "sha256": "7679daa4ec6a40f56fc7f0202379a6f454310e94945aba4f48beaaaafb838d05", + "pin": "head:d3dada62d182187f26651be598571df606662c32:research/phase-rank-debt/inputs/round3-native.json.gz", + "origin": { + "commit": "1eb8da6cfb35512c0cc2533413e5ca42f48e13c6", + "path": "research/kappa-round3-warp-20261022/ACTUAL-WORD.json.gz", + "git_blob": "46d929df83817b85a5387bcdb9745e0627d6366e" + } + } + ] +} diff --git a/research/phase-rank-debt/TASK.json b/research/phase-rank-debt/TASK.json new file mode 100644 index 0000000000..c251f73b03 --- /dev/null +++ b/research/phase-rank-debt/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove and source-bind the complete concave rank debt of symmetric phase deformations of the PR4610 fixed scalar graph, allowing paid corrections and owned-center phases.", + "scope_change_reason": "The user requests a structural K breakthrough. PR4665 leaves paid phase changes and owned-center forms outside its zero-solution certificate. Price this enlarged phase grammar before spending a construction round on it.", + "bottleneck_link": "A higher productive helper rank is useful only if its paid corrections cost less moment. This theorem excludes that gain on the frozen monotone graph, across all concave exponents and compatible forms.", + "budget_minutes": 60, + "stop_rule": "Stop this phase-only family once the exact debt inequality and both source-specific path certificates pass. Reopen only after changing a stated graph, subspace, main or shared-operation hypothesis.", + "outcome": "negative-result", + "evidence": "PROOF.md proves the exact inequality; RESULT.json and verify.py bind its hypotheses to both complete source orientations and list meaningful controls.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematical derivation, code, verification and prose. No subagents or independent human review.", + "open_questions": [ + { + "question": "Can one shared multi-owner correction across an actual scalar contact beat the sum of separate phase corrections?", + "why_it_matters": "It changes the owner-separated debt hypothesis and could supply a new paid profile.", + "first_step": "Freeze the smallest real contact, give its arbitrary-input block operator, and price both orientations including owners, correction and restoration.", + "blocked_by": "No complete shared correction operator or physical bill has been constructed." + } + ] +} diff --git a/research/phase-rank-debt/VERIFY.json b/research/phase-rank-debt/VERIFY.json new file mode 100644 index 0000000000..31049a273a --- /dev/null +++ b/research/phase-rank-debt/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/phase-rank-debt/inputs/round3-native.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate original word; both complete paths and paid profiles; contact-block and warp hypotheses; exact rank and concavity controls; source mutations; frame basis changes." + } + ] +} diff --git a/research/phase-rank-debt/inputs/round3-native.json.gz b/research/phase-rank-debt/inputs/round3-native.json.gz new file mode 100644 index 0000000000..46d929df83 Binary files /dev/null and b/research/phase-rank-debt/inputs/round3-native.json.gz differ diff --git a/research/phase-rank-debt/verify.py b/research/phase-rank-debt/verify.py new file mode 100644 index 0000000000..e54f708b24 --- /dev/null +++ b/research/phase-rank-debt/verify.py @@ -0,0 +1,227 @@ +"""Rank-debt certificate. Apache-2.0; substantial OpenAI Codex assistance. + +Checks the hypotheses of PROOF.md, not native phases or a new supplier. +Original word: Cao Yifan/PR4610, retained by Cinna Davis/PR4665. +""" +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +import gzip +import hashlib +import json +from math import isqrt +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +PAID = {1: 2201, 2: 412, 3: 510, 4: 127, 5: 40, 8: 8} +HELPERS = {4: 28, 7: 7, 8: 47, 9: 326} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def span(basis): + out = {0} + for x in basis: + need(type(x) is int and 0 < x < 512, 'nonzero nine-bit vector') + out |= {v ^ x for v in tuple(out)} + need(len(out) == 2 ** len(basis), 'independent binary frame') + return frozenset(out) + + +def mv(columns, x): + out = 0 + for i, v in enumerate(columns): + if x >> i & 1: + out ^= v + return out + + +def invert(columns): + table = {mv(columns, x): x for x in range(512)} + need(len(table) == 512, 'invertible warp') + return [table[1 << i] for i in range(9)] + + +def audit(payload): + c, programs = payload['canonical'], payload['programs'] + frames = c['frames'] + spaces = list(map(span, frames)) + need(len(c['start']) == len(c['final']) == 632, '632 independent fields') + need(set(programs) == {'forward', 'backward'}, 'both orientations') + maps = {w['op']: w['G_columns'] for w in c['warps']} + maps.update({-op: invert(g) for op, g in list(maps.items())}) + results = {} + for direction, word in sorted(programs.items()): + current = {('L', r): f for r, f in enumerate(c['start'])} + current['C', 0] = None + images = [list(frames[f]) for f in c['start']] + widths = [[] for _ in range(632)] + blocks = [[] for _ in range(632)] + helper_blocks = Counter() + paid, counts = Counter(), Counter() + + def close_block(r): + if r >= 224: + need(len(blocks[r]) <= 1, 'at most one original paid call between scalar contacts') + helper_blocks[len(blocks[r])] += 1 + blocks[r] = [] + + for e in word: + kind = e[0] + counts[kind] += 1 + if kind in ('climb', 'center'): + if kind == 'climb': + _, _, r, a, b, width = e + role = ('L', r) + need(spaces[a] < spaces[b], 'monotone persistent transport') + widths[r].append(width) + blocks[r].append(width) + else: + _, r, a, b, width = e + role = ('C', r) + need(spaces[a] < spaces[b] or spaces[b] < spaces[a], + 'nested center transport') + need(current[role] == a, 'paid input chart') + need(width == abs(len(frames[b]) - len(frames[a])), 'paid width') + paid[width] += 1 + current[role] = b + elif kind == 'warp': + _, reg, op, a, b = e + role = tuple(reg) + need(role[0] == 'L' and current[role] == a, 'warp input chart') + need(span([mv(maps[op], x) for x in frames[a]]) == spaces[b], + 'warp acts on its complete declared subspace') + need(len(frames[a]) == len(frames[b]), 'warp preserves dimension') + images[role[1]] = [mv(maps[op], x) for x in images[role[1]]] + current[role] = b + elif kind == 'scalar': + g, f = e[1:] + role = tuple(g[1]) + if g[0] == 'clear': + need(role == ('C', 0), 'only owned center cleared') + current[role] = f + else: + need(g[0] in ('add', 'copy', 'scale'), 'known scalar action') + refs = g[1:3] if g[0] in ('add', 'copy') else g[1:2] + need(all(current[tuple(reg)] == f for reg in refs), 'common scalar chart') + for typ, r in refs: + if typ == 'L': + close_block(r) + if g[0] == 'copy': + need(role == ('C', 0), 'only owned center overwritten') + else: + need(kind in ('phase', 'adapter'), 'known inert marker') + if kind == 'adapter': + close_block(e[2]) + need(paid == PAID, 'complete source paid profile, including centers') + need([current['L', r] for r in range(632)] == c['final'], 'all final charts') + helpers, maximum_step, path_mass = Counter(), Counter(), 0 + for r in range(632): + close_block(r) + h = len(frames[c['final'][r]]) - len(frames[c['start'][r]]) + need(sum(widths[r]) == h, 'telescoping persistent paid mass') + if r >= 224: + need(h > 0 and spaces[c['start'][r]] <= spaces[c['final'][r]], + 'positive nested helper endpoint') + need(images[r] == frames[c['start'][r]], 'net warp fixes helper entrance pointwise') + need(max(widths[r], default=0) <= h, 'each paid step bounded by endpoint rank') + helpers[h] += 1 + maximum_step[max(widths[r], default=0)] += 1 + path_mass += sum(widths[r]) + need(helpers == HELPERS and path_mass == 3471, 'all 408 helper paths') + results[direction] = { + 'events': dict(sorted(counts.items())), 'paid': dict(sorted(paid.items())), + 'helper_ranks': dict(sorted(helpers.items())), + 'helper_maximum_paid_step': dict(sorted(maximum_step.items())), + 'helper_path_rank_mass': path_mass, 'pointwise_fixed_helper_entrances': 408, + 'helper_contact_blocks_by_original_paid_calls': dict(sorted(helper_blocks.items())), + 'persistent_paths_with_exact_rank_telescope': 632, + } + return results + + +def rank(rows): + pivots = {} + for x in rows: + while x: + p = x.bit_length() - 1 + if p not in pivots: + pivots[p] = x + break + x ^= pivots[p] + return len(pivots) + + +def controls(payload): + forms = [(a | b << 1, b | c << 1) + for a in range(2) for b in range(2) for c in range(2)] + cases = 0 + for a in forms: + for b in forms: + for c in forms: + difference = lambda x, y: [u ^ v for u, v in zip(x, y)] + g = rank(difference(a, c)) + debt = rank(difference(a, b)) + rank(difference(b, c)) + need(g <= debt, 'exact endpoint rank triangle inequality') + cases += 1 + scale = 1 << 80 + root = lambda n: (Q(isqrt(n * scale * scale), scale), + Q(isqrt(n * scale * scale) + 1, scale)) + need(root(2)[0] - 1 > root(5)[1] - 2, + 'split path pays more than its endpoint at t=1/2') + need(root(9)[1] - root(8)[0] < root(5)[0] - 2, + 'step larger than endpoint breaks the required inequality') + failures = [] + for label in ('wrong_width', 'missing_center', 'wrong_warp', 'wrong_helper_endpoint'): + bad = deepcopy(payload) + word = bad['programs']['forward'] + if label == 'wrong_width': + next(e for e in word if e[0] == 'climb')[5] += 1 + elif label == 'missing_center': + word.remove(next(e for e in word if e[0] == 'center')) + elif label == 'wrong_warp': + next(e for e in word if e[0] == 'warp' and bad['canonical']['frames'][e[3]])[4] = 0 + else: + bad['canonical']['final'][224] = 0 + try: + audit(bad) + except (ValueError, KeyError): + failures.append(label) + else: + raise ValueError('mutation accepted: ' + label) + return {'symmetric_form_rank_triangles': cases, + 'strict_concave_increment_and_missing_hypothesis': True, + 'source_mutations_rejected': failures} + + +def main(): + source = HERE / 'inputs/round3-native.json.gz' + pins = json.loads((HERE / 'SOURCES.json').read_text()) + pin = next(row for row in pins['files'] if row['path'].endswith(source.name)) + raw = source.read_bytes() + need(hashlib.sha256(raw).hexdigest() == pin['sha256'], 'exact original source bytes') + payload = json.loads(gzip.decompress(raw)) + report = {'status': 'FIXED_WORD_PHASE_CHANGES_CANNOT_IMPROVE_ANY_CONCAVE_MOMENT', + 'no_new_kappa': True, 'orientations': audit(payload), + 'controls': controls(payload)} + changed = deepcopy(payload) + for basis in changed['canonical']['frames']: + if len(basis) >= 2: + basis[0] ^= basis[1] + need(audit(changed) == report['orientations'], 'all frame basis changes preserve certificate') + report['controls']['all_frame_basis_changes'] = True + report = json.loads(json.dumps(report)) + path = HERE / 'RESULT.json' + if '--write' in sys.argv: + path.write_text(json.dumps(report, indent=2, sort_keys=True) + '\n') + else: + need(report == json.loads(path.read_text()), 'committed result equality') + print('PASS_PHASE_RANK_DEBT: both orientations, 408 helpers, all 0<=t<=1; no new kappa') + + +if __name__ == '__main__': + main()