From 533a5f463e89e6fb74287ffe93c815fe83da10bb Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Sun, 25 Oct 2026 19:28:06 -0500 Subject: [PATCH] Prove pair parity bounds and a mixed chronology cut --- research/paired-stage-chronology-cut/PROOF.md | 180 ++++++ .../paired-stage-chronology-cut/README.md | 36 ++ .../paired-stage-chronology-cut/RESULT.json | 139 +++++ .../SOURCE-CONTEXT.json | 23 + .../paired-stage-chronology-cut/SOURCES.json | 24 + .../paired-stage-chronology-cut/TASK.json | 90 +++ .../paired-stage-chronology-cut/VERIFY.json | 30 + .../paired-stage-chronology-cut/chronology.py | 82 +++ .../inputs/PR5617-PROOF.md | 562 ++++++++++++++++++ .../inputs/PR5617-RESULT.json | 287 +++++++++ .../inputs/PR5617-cuts.py | 87 +++ .../paired-stage-chronology-cut/verify.py | 164 +++++ 12 files changed, 1704 insertions(+) create mode 100644 research/paired-stage-chronology-cut/PROOF.md create mode 100644 research/paired-stage-chronology-cut/README.md create mode 100644 research/paired-stage-chronology-cut/RESULT.json create mode 100644 research/paired-stage-chronology-cut/SOURCE-CONTEXT.json create mode 100644 research/paired-stage-chronology-cut/SOURCES.json create mode 100644 research/paired-stage-chronology-cut/TASK.json create mode 100644 research/paired-stage-chronology-cut/VERIFY.json create mode 100644 research/paired-stage-chronology-cut/chronology.py create mode 100644 research/paired-stage-chronology-cut/inputs/PR5617-PROOF.md create mode 100644 research/paired-stage-chronology-cut/inputs/PR5617-RESULT.json create mode 100644 research/paired-stage-chronology-cut/inputs/PR5617-cuts.py create mode 100644 research/paired-stage-chronology-cut/verify.py diff --git a/research/paired-stage-chronology-cut/PROOF.md b/research/paired-stage-chronology-cut/PROOF.md new file mode 100644 index 0000000000..c4bb728b85 --- /dev/null +++ b/research/paired-stage-chronology-cut/PROOF.md @@ -0,0 +1,180 @@ +# Pair parity and the missing chronology cut + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +## Scope and result + +Use the binary normalized controller model of PR #5617, at commit +6c088037e13b87faf7cfe3233c53d0ae51850dd8. There are n main fields per port, +L = n+2 = 2m full calls, m independent stage blocks, and two calls per +block. Each block has eight axes. Helpers are fresh independent jobs. +There are no thin calls or idle maps. Ports stay separate. Each normalized +query is R_i = u_i v_i, with R_i squared zero and sum R_i = I. Each call +has a rank-two idempotent P_i with P_i R_i = R_i P_i = R_i. The target +stage projectors E_c are diagonal in one common basis. + +Let r_c = rank E_c and D = 4m - sum r_c. Then: + +- D >= 2 for every m >= 4. +- D >= 4 for every odd m >= 5. +- At kappa >= 0.003, the complete PR #5599 bill excludes every m <= 47, + and every odd m <= 89. These are n <= 92 and odd m with n <= 176. + The original P104 bill gives m <= 50 and odd m <= 93. +- The previous rank and intersection cuts cannot force a loss that grows + without bound: an explicit compatible family has D = 8 for every odd + m >= 5. It passes those cuts, but fails a mixed coefficient condition. + +The small m <= 3 exclusions are inherited from PR #5617. None of these +claims supplies a native caller or changes kappa. The written proofs +apply over any field of characteristic two. The executable controls use F2. + +## 1. The rank of a pair is even + +Write E = P+P' for the two calls of one stage. Since E is an idempotent, +PP' = P'P. Commuting idempotents split the space into their four common +image/kernel spaces. Since both have rank two, + + rank E = rank P + rank P' - 2 rank(PP') = 4 - 2 rank(PP'). + +Thus each r_c is 0, 2 or 4. Section 8 of the pinned predecessor proves +that D > 0 for every m >= 4. It follows that D >= 2. + +For odd m, suppose only one class b is deficient. Factor the rank-two +complement of the query Gram matrix as I-K = XY, with YX = I_2. For +every full class c, the predecessor's capacity cut gives X_c Y_c = I_2. +Hence Y_c X_c = I_2. There are m-1 such classes, an even number. Therefore +Y_b X_b = I_2 as well. Both factors are invertible, so K_bb = 0 and +all off-diagonal blocks K_cb and K_bc have rank two. It follows that +U_b and V_b each have rank two. + +The two projectors P,P' of class b commute. Their join is the idempotent +H = P+P'+PP'. Its image is im P + im P', and its rank is 2+r_b/2. +Compatibility gives H U_b = U_b and V_b H = V_b. But V_b U_b = K_bb = 0. +The restriction of V_b to im H has rank two. Its kernel contains the +two-dimensional image of U_b. Thus rank H >= 4, which forces r_b = 4. +This contradicts the choice of b. At least two classes are deficient; +each loses at least two ranks. This proves D >= 4 for odd m >= 5. + +This argument does not prove that these lower bounds on D are attained. + +## 2. Complete price consequences + +Use the two exact paid and helper histograms in the pinned predecessor +RESULT.json. This package authenticates those bytes and recomputes their +net rank mass 1720 and all their nonpositive hinge sums. The predecessor +supplies the native inventory provenance; its native construction is +not replayed here. + +For any normalized nondecreasing concave tariff, the complete moment is +at most + + 104 * ((2m-2) + 8*(4m-D)) - 2m*1720 = 96m-208-832D. + +Thus D >= 2 rejects m <= 19 for every such tariff. D >= 4 rejects odd +m <= 35 for every such tariff. For the power tariff r^t, discrete +concavity distributes the remaining block occurrences as evenly as +possible among the 2m-2 jobs. The two sharper upper bounds are + + M_2(m,t) = 104*((2m-4)*17^t + 2*25^t) - 2m*net(t), + M_4(m,t) = 208*(m-1)*17^t - 2m*net(t), + net(t) = sum_r (paid[r]-helpers[r])*r^t. + +The verifier uses integer comparisons to enclose each power at + t=997/1000 within 2^-48. Both bounds are affine in m. It checks their +first and last rejected values and their next positive value. For the +PR #5599 profile the rejected endpoints are m=47 and odd m=89. For the +original P104 profile they are m=50 and odd m=93. A positive upper bound +at the next value is not evidence for an attainable caller. + +All negative coefficients have smaller rank than every positive +coefficient. Divide by the smallest positive rank to the power t. Each +positive term is nondecreasing in t; each negative term also is +nondecreasing in t. The normalized bound is therefore nondecreasing. +The exclusions hold for all 0= 3 be odd. Take two disjoint copies of a space with basis + e_0,e_1,...,e_g. For each copy and each j=1,...,g use + + u_j = v_j^T = e_0+e_j, + R_j = u_j v_j, + P_j = e_0 e_0^T + e_j e_j^T. + +Pair the two copies of each j as one stage. Let w = sum_(j=1)^g e_j. +Add two calls in each copy, + + R_A = e_0 w^T, R_B = w e_0^T, + P_A = P_B = e_0 e_0^T + w w^T. + +Pair A and B within that copy as one additional stage. Since g is odd, +w^T w = 1. All P are rank-two idempotents compatible with their rank-one +nilpotent queries. Direct addition gives sum R = I on each copy. Each +good stage E_j has rank four, on the two cores and its two leaves. Each +of the two extra stages has E=0. Thus n=2g+2, L=2g+4, m=g+2 and D=8. +All target projectors are diagonal and commute. + +These are actual compatible local matrices and target derivatives. +Consequently they meet the assumptions of every old capacity and +intersection cut. The verifier also runs the unchanged predecessor +filter on g=3,5,7,15,31,511; the last case has 131328 intersection cuts. +This proves that those algebraic conditions alone cannot imply a loss +that increases without bound with m. It does not show that D=8 is the +best constant possible. + +The relaxed main inventory has two jobs of rank 1+8g and 2g jobs of rank +9 per port. At g=511 and t=997/1000 its complete relaxed moment is +strictly positive for both source profiles. Exact enclosures are in +RESULT.json. This positive relaxation is an explicit false lead for a +search that omits chronology. It is not a kappa claim. + +## 4. A mixed coefficient cut + +Put Q=1+e and the stage under test z_c=1+d, with e^2=d^2=0. Set every +other stage to one. The normalized local gate is + + (I+d P_i)(I+e R_i) + +at a call in class c, and I+e R_i otherwise. Gates act in listed order, +with later factors on the left. Expand the coefficient of de. Use +sum R_i=I and P_i R_i=R_i. That coefficient is + + E_c + sum_(i in S_c) [P_i, sum_(j>i) R_j]. + +The target coefficient is E_c. Therefore every valid word must satisfy + + sum_(i in S_c) [P_i, sum_(j>i) R_j] = 0. (* ) + +Over F2 the commutator is AB+BA. The routine in chronology.py evaluates +this necessary condition from explicit local matrices and the call +order. A pass still does not prove the other word coefficients. + +For the family above, list good calls by j, with the two copies together, +then list A,B in each copy. The verifier finds g-1 failed stages, each +with defect rank four. A separate literal polynomial interpreter checks +the mixed coefficient for g=3,5,7. A genuine six-query positive word +passes and has all sixteen expected coefficients for three stages and Q. +Deleting one query fails the query-frame check. + +No reordering repairs this family. Restrict to either copy. It has +n'=g+1 fields and L'=g+2=n'+1 queries. The g good stages are private +in that copy and their projectors commute. Cinna Davis's minimum-query +private-projector lemma, retained in PR #5617 Section 4 and in the +pinned GLOBAL-PROOF.md, allows at most two such private calls for n'>=4. +Here g>=3. Every relative order fails the necessary mixed condition. +Calls in the other copy do not change that restriction. The verifier +also checks all 120 relative orders at g=3. + +## Verification and remaining obligations + +The proof of the unbounded statements is the argument above. Finite +matrix checks do not replace it. No proof-assistant check or independent +review is claimed. No general reduction from complex native programs to +this binary model is claimed. Coupled ports in the paired-stage case, +paid idles, mixed query ranks, partial block overlaps, main/helper mixing +and noninvolutive stages remain outside the price theorem. + +The next caller search should enforce (* ) before expanding a full word. +It must then check every coefficient and retain all native, scalar, +helper, routing, restoration and compiler charges. A positive relaxed +moment is insufficient. diff --git a/research/paired-stage-chronology-cut/README.md b/research/paired-stage-chronology-cut/README.md new file mode 100644 index 0000000000..9bc6942145 --- /dev/null +++ b/research/paired-stage-chronology-cut/README.md @@ -0,0 +1,36 @@ +# Paired-stage chronology cut + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +[PROOF.md](PROOF.md) proves even pair ranks, a stronger odd-pair loss, +and the mixed query-stage condition. For the complete PR #5599 profile, +the paired-stage family fails at kappa >= 0.003 through 92 fields and, +for odd stage-pair counts, through 176 fields. No new kappa is claimed. + +An unbounded compatible family has constant loss eight and passes the +previous rank and intersection cuts. It fails the new chronology cut in +every order. At 1024 fields its complete relaxed price is positive. This +separates a useful price screen from a real endpoint. + +Run `python3 -B scripts/research_package.py --package research/paired-stage-chronology-cut`. +The registered normal and optimized Python checks use exact arithmetic. +RESULT.json records the finite controls and interval numerators. + +## Sources and credit + +PR #5617 supplies the general cuts, the full-capacity obstruction, and +both complete source profiles. Its exact files are retained in inputs/, +with hashes and source paths in SOURCE-CONTEXT.json. Cinna Davis supplies +the private-projector lemma in the pinned GLOBAL-PROOF.md. Douglas +Colkitt and the P104 source contributors retain the source package credit. +The new contributions are pair parity, the odd-pair strengthening, the +constant-loss compatible family, the mixed coefficient filter and their +complete-price consequences. No predecessor native admission is repeated. + +## Open next questions + +Impose the mixed cut in a paired-stage search, then verify every word +coefficient of a surviving candidate. A result must retain the full bill. +Determine whether a constant-loss family can satisfy chronology at all +sizes. The construction here cannot. Coupled ports and paid idles need +separate price theorems. diff --git a/research/paired-stage-chronology-cut/RESULT.json b/research/paired-stage-chronology-cut/RESULT.json new file mode 100644 index 0000000000..1294ff2fac --- /dev/null +++ b/research/paired-stage-chronology-cut/RESULT.json @@ -0,0 +1,139 @@ +{ + "all_relative_orders_g3": 120, + "idempotent_pairs": 21280, + "limits": { + "formal_kernel": false, + "independent_review": false, + "native_replay": false, + "new_kappa": false, + "source_history_preflight": false + }, + "pair_ranks": { + "0": 560, + "2": 20160, + "4": 560 + }, + "positive_full_word_coefficients": 16, + "prices": { + "PR5599_at_09dd0965": { + "invalid_star_relaxation_g511": { + "denominator": 281474976710656, + "lower_numerator": 326605166740168710, + "upper_numerator": 326605166741877818 + }, + "loss_2_m_4": { + "denominator": 281474976710656, + "lower_numerator": -480436675478124072, + "upper_numerator": -480436675478110952 + }, + "loss_2_m_47": { + "denominator": 281474976710656, + "lower_numerator": -10629808591205894, + "upper_numerator": -10629808591049498 + }, + "loss_2_m_48": { + "denominator": 281474976710656, + "lower_numerator": 295932499187552, + "upper_numerator": 295932499347280 + }, + "loss_4_m_5": { + "denominator": 281474976710656, + "lower_numerator": -932243008932947362, + "upper_numerator": -932243008932930910 + }, + "loss_4_m_89": { + "denominator": 281474976710656, + "lower_numerator": -14480757339897898, + "upper_numerator": -14480757339601558 + }, + "loss_4_m_91": { + "denominator": 281474976710656, + "lower_numerator": 7370724840888994, + "upper_numerator": 7370724841191998 + } + }, + "original_P104": { + "invalid_star_relaxation_g511": { + "denominator": 281474976710656, + "lower_numerator": 95767729394002242, + "upper_numerator": 95767729395669284 + }, + "loss_2_m_4": { + "denominator": 281474976710656, + "lower_numerator": -482236577523708216, + "upper_numerator": -482236577523695424 + }, + "loss_2_m_50": { + "denominator": 281474976710656, + "lower_numerator": -351360889827356, + "upper_numerator": -351360889665064 + }, + "loss_2_m_51": { + "denominator": 281474976710656, + "lower_numerator": 10124404689170054, + "upper_numerator": 10124404689335596 + }, + "loss_4_m_5": { + "denominator": 281474976710656, + "lower_numerator": -934492886489927542, + "upper_numerator": -934492886489911500 + }, + "loss_4_m_93": { + "denominator": 281474976710656, + "lower_numerator": -12625515538155462, + "upper_numerator": -12625515537853420 + }, + "loss_4_m_95": { + "denominator": 281474976710656, + "lower_numerator": 8326015619839358, + "upper_numerator": 8326015620147900 + } + } + }, + "projectors": 560, + "status": "PASS_PAIRED_STAGE_CHRONOLOGY_CUT", + "witnesses": [ + { + "g": 3, + "loss": 8, + "mixed_rejections": 2, + "n": 8, + "prior_intersection_cuts": 10 + }, + { + "g": 5, + "loss": 8, + "mixed_rejections": 4, + "n": 12, + "prior_intersection_cuts": 21 + }, + { + "g": 7, + "loss": 8, + "mixed_rejections": 6, + "n": 16, + "prior_intersection_cuts": 36 + }, + { + "g": 15, + "loss": 8, + "mixed_rejections": 14, + "n": 32, + "prior_intersection_cuts": 136 + }, + { + "g": 31, + "loss": 8, + "mixed_rejections": 30, + "n": 64, + "prior_intersection_cuts": 528 + }, + { + "g": 511, + "loss": 8, + "mixed_rejections": 510, + "n": 1024, + "prior_intersection_cuts": 131328 + } + ] +} diff --git a/research/paired-stage-chronology-cut/SOURCE-CONTEXT.json b/research/paired-stage-chronology-cut/SOURCE-CONTEXT.json new file mode 100644 index 0000000000..a73ef0b395 --- /dev/null +++ b/research/paired-stage-chronology-cut/SOURCE-CONTEXT.json @@ -0,0 +1,23 @@ +[ + { + "file": "inputs/PR5617-PROOF.md", + "commit": "6c088037e13b87faf7cfe3233c53d0ae51850dd8", + "path": "research/shortest-controller-stage-capacity/PROOF.md", + "sha256": "df8c53e3b04fdfa9ea10dd02a8bf770ba3111c7fa2d561075e7dd00d2297613e", + "git_blob": "3e1a1f6b1f773780927f01e20be6719fe08ca5f3" + }, + { + "file": "inputs/PR5617-RESULT.json", + "commit": "6c088037e13b87faf7cfe3233c53d0ae51850dd8", + "path": "research/shortest-controller-stage-capacity/RESULT.json", + "sha256": "c82ab9537817d55db5c23e825d31e868deb3daa2dbc8b5f4db0b1f1a71960e0a", + "git_blob": "fe5ac435fe776bc7037b49e20352de055e2c7291" + }, + { + "file": "inputs/PR5617-cuts.py", + "commit": "6c088037e13b87faf7cfe3233c53d0ae51850dd8", + "path": "research/shortest-controller-stage-capacity/cuts.py", + "sha256": "79c56eb97e8bb6a27c362a5d87f1787f8ca5e05898dca5d1ea6fd72afbafccc9", + "git_blob": "9c1f001a1c4a2a1c993dde274b0104557c777d55" + } +] diff --git a/research/paired-stage-chronology-cut/SOURCES.json b/research/paired-stage-chronology-cut/SOURCES.json new file mode 100644 index 0000000000..6959d5192b --- /dev/null +++ b/research/paired-stage-chronology-cut/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63", + "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/productive-controller-basis-search/GLOBAL-PROOF.md", + "usage": "input", + "git_blob": "74b67e22e6c063193a83825207cdec19a8fef7a4", + "sha256": "adc377b13924701bf5b0b50b091d8b69c90195d50ce0f6808f7fb4c7e0b16457" + } + ] +} diff --git a/research/paired-stage-chronology-cut/TASK.json b/research/paired-stage-chronology-cut/TASK.json new file mode 100644 index 0000000000..0718280363 --- /dev/null +++ b/research/paired-stage-chronology-cut/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. 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", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "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_status": "changed", + "actual_scope": "Strengthen paired-stage capacity losses and identify the missing chronology condition.", + "scope_change_reason": "Take the released PR5617 handoff. Test whether its loss grows with caller size before a larger controller search.", + "bottleneck_link": "Reject impossible paid P104 callers earlier and prevent a profitable false relaxation from directing native work.", + "budget_minutes": 90, + "stop_rule": "Prove a stronger loss bound and either a growing-loss theorem or a counterexample with a new discriminating cut.", + "outcome": "negative-result", + "evidence": "PROOF.md, RESULT.json, chronology.py and verify.py", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for proofs, code, verification and publication.", + "open_questions": [ + { + "question": "What is the best loss bound after all mixed query-stage equations are imposed?", + "why_it_matters": "The old cuts allow an unbounded family with positive relaxed price and no endpoint.", + "first_step": "Add the chronology filter to a paired-stage solver and replay all coefficients of a survivor.", + "blocked_by": "No certified native caller in this family." + } + ] +} diff --git a/research/paired-stage-chronology-cut/VERIFY.json b/research/paired-stage-chronology-cut/VERIFY.json new file mode 100644 index 0000000000..18dd0c723c --- /dev/null +++ b/research/paired-stage-chronology-cut/VERIFY.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/productive-controller-basis-search/GLOBAL-PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact parity census, old-cut witnesses, mixed coefficients, positive word, all-order control and complete price intervals." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exact parity census, old-cut witnesses, mixed coefficients, positive word, all-order control and complete price intervals." + } + ] +} diff --git a/research/paired-stage-chronology-cut/chronology.py b/research/paired-stage-chronology-cut/chronology.py new file mode 100644 index 0000000000..29e821e6cc --- /dev/null +++ b/research/paired-stage-chronology-cut/chronology.py @@ -0,0 +1,82 @@ +"""Check one necessary mixed coefficient over F2. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Matrices use integer bit rows. A pass does not prove the full word. +""" + +def need(c, m): + if not c: + raise ValueError(m) + +def add(a, b): + return [x ^ y for x, y in zip(a, b)] + +def outer(u, v, n): + return [v if u >> i & 1 else 0 for i in range(n)] + +def mul(a, b): + out = [] + for x in a: + z = 0 + while x: + low = x & -x + z ^= b[low.bit_length() - 1] + x ^= low + out.append(z) + return out + +def rank(a): + p = {} + for x in a: + while x: + i = x.bit_length() - 1 + if i not in p: + p[i] = x + break + x ^= p[i] + return len(p) + +def family(g): + need(g >= 3 and g % 2 == 1, 'odd g') + n = 2 * (g + 1) + us = [] + vs = [] + ps = [] + labels = [] + for j in range(1, g + 1): + for a in range(2): + core = 1 << a * (g + 1) + leaf = core << j + us.append(core | leaf) + vs.append(core | leaf) + ps.append(add(outer(core, core, n), outer(leaf, leaf, n))) + labels.append(j - 1) + for a in range(2): + core = 1 << a * (g + 1) + leaves = (1 << g + 1) - 2 << a * (g + 1) + p = add(outer(core, core, n), outer(leaves, leaves, n)) + for u, v in [(core, leaves), (leaves, core)]: + us.append(u) + vs.append(v) + ps.append(p) + labels.append(g + a) + axes = [] + for c in range(g + 2): + group = [i for i, x in enumerate(labels) if x == c] + e = add(ps[group[0]], ps[group[1]]) + need(mul(e, e) == e, 'target idempotent') + outs = [j for j, x in enumerate(e) if x] + need(all((not x or x == 1 << j for j, x in enumerate(e))), 'diagonal target') + axes.append(dict(name=str(c), calls=group, outputs=outs)) + return (dict(n=n, u=us, v=vs, axes=axes), ps, labels) + +def mixed(candidate, ps, labels): + n = candidate['n'] + tail = [0] * n + defects = {c: [0] * n for c in set(labels)} + for i in reversed(range(len(ps))): + c = labels[i] + defects[c] = add(defects[c], add(mul(ps[i], tail), mul(tail, ps[i]))) + tail = add(tail, outer(candidate['u'][i], candidate['v'][i], n)) + need(tail == [1 << j for j in range(n)], 'identity frame') + return {c: rank(a) for c, a in defects.items() if any(a)} diff --git a/research/paired-stage-chronology-cut/inputs/PR5617-PROOF.md b/research/paired-stage-chronology-cut/inputs/PR5617-PROOF.md new file mode 100644 index 0000000000..3e1a1f6b1f --- /dev/null +++ b/research/paired-stage-chronology-cut/inputs/PR5617-PROOF.md @@ -0,0 +1,562 @@ +# A rank cut for stage reuse + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. + +## 1. Result and exact model + +This is a scoped obstruction for complete caller words. It does not keep +the inputs to earlier paid calls fixed. It allows arbitrary invertible +binary changes of basis between calls. + +There are n independent main fields, a central involution Q, and independent +commuting involutions z_x, one for each transverse axis. Work in the group +algebra over F2. A full call has the form + +```text +(I + (d_i + 1) P_i) (I + Q N_i), +d_i = product(z_x : x in S_i), |S_i| = b. +``` + +Here P_i is an idempotent of rank two, N_i is a nilpotent of rank one, +and P_i N_i = N_i P_i = N_i. A thin call is I + Q N_i. The sets S_i can +overlap or repeat in any way. Ordinary scalar changes of basis are free +for this necessary test. Helpers stay separate independent jobs. The +main target, after constant invertible binary input and output bases, is + +```text +diag(Q * product(z_x : x in T_j) : j = 1,...,n). +``` + +Its charged Fourier rank is 1 + |T_j|. Each full call uses a fresh complete +local helper inventory. A thin call costs one rank-one query per port. +Sections 1-8 describe the controller on each port. The complete price +applies these bounds across the v ports. Those sections keep ports +separate. Section 9 extends the shortest-query result to arbitrary +scalar mixing across all ports at the stated saturated main-field count. +The principal theorem permits no idle axis maps or other paid main maps. +Section 2 also gives a necessary cut when such idle maps are present. + +Let L count all query-bearing calls and f count the full calls. The +shortest case is L = n + 1. For n >= 4, the following statements hold. + +1. If axis x occurs in k_x full calls, it can occur in at most + k_x + (k_x mod 2) independent main targets. +2. At most two full calls can have an axis that occurs in no other call. +3. With b = 8 and either pinned P104 local inventory, the complete + target moment minus paid moment is at most -8 for every exponent + 0 < t <= 1. The bound is sharp at t = 1. + +This includes all main-field counts, all full/thin placements, every +commuting coordinate overlap, and all scalar bases in the declared +binary model. A finite search is not the proof of these statements. + +For n = 2, the three-full-call unit is the exception. Its optimistic +complete moment is already negative at kappa = 0.002 for both pinned +inventories, and remains negative for every larger kappa below one. +Thus no shortest caller in this model improves the selected bound. + +The binary model does not cover arbitrary complex scalar codes with +even denominators, noncommuting stage operators, an advancing operator +with unbounded order, joint main/helper codes, or a changed target +contract. An integral symbolic caller that reduces to this model must +pass its test. No reduction of every physical Clifford program to this +model is asserted. + +## 2. General query-frame cut + +Set Q = 1 + e, with e squared equal to zero. Absorb the ordinary changes +of basis and each call's constant value at Q = 1 into adjacent bases. +Each query then has the form I + e R_i, where + +```text +R_i = u_i v_i, v_i u_i = 0, sum_i R_i = I_n. +``` + +The corresponding full-call projector still has rank two and satisfies +P_i R_i = R_i P_i = R_i. This normalization is a conjugation. It does +not change ranks, independence, or the number of paid calls. + +Put U_0 = [u_0 ... u_(L-1)] and let V_0 have rows v_i. Then U_0 V_0 = I. +The query Gram matrix K = V_0 U_0 is an idempotent of rank n. Its diagonal +is zero. If L <= n, rank forces L = n and V_0 U_0 = I, a contradiction. +Thus L >= n + 1. Write h = L - n. The complementary idempotent I - K +has rank h. + +For any axis x, let S be the set of its full-call occurrences, with +|S| = k. Set that axis to 1 + d, where d squared is zero; set all other +axes and Q to one. The full-call derivative is P_i at an occurrence and +zero elsewhere. The monomial target gives an idempotent E_x whose rank +r_x is the number of target jobs that contain x. Hence + +```text +E_x = sum_(i in S) P_i. +``` + +More generally, h_x separately charged one-field idle occurrences add +h_x matrices of rank at most one to this sum. The same argument below +allows those terms. + +For each i, choose a_i in the image of P_i with v_i a_i = 1. Such a +choice exists because v_i P_i = v_i is nonzero. Choose b_i as the +coordinate of u_i in the basis (u_i, a_i) of that image, with b_i zero +on the kernel of P_i. Then + +```text +P_i = u_i b_i + a_i v_i, +b_i u_i = v_i a_i = 1, b_i a_i = v_i u_i = 0. +``` + +Factor the sum E_x = A B. Use the columns u_i, a_i of A and the rows +b_i, v_i of B, then append a rank-one factor for each idle term. Thus A +has 2k + h_x columns. Because E_x is an idempotent, + +```text +rank(I_(2k+h_x) - B A) = 2k + h_x - r_x. (1) +``` + +To prove (1), U: w -> A w maps the kernel of I - B A bijectively onto +the image of E_x. Its inverse is y -> B y. This proves the dimension +identity even when A or B has a kernel. + +Select the rows of B A that came from v_i and the columns that came +from u_j. The corresponding submatrix of the identity is zero. The +selected submatrix of I - B A is therefore -K[S,S]. A submatrix cannot +have larger rank than its parent. Equation (1) gives the necessary cut + +```text +r_x <= 2k + h_x - rank K[S,S]. (2) +``` + +This cut uses the actual query Gram matrix. It applies to longer words +as well as shortest words. Since K[S,S] = I_k - (I-K)[S,S], + +```text +rank K[S,S] >= max(0, k-h), +r_x <= k + min(k,h) + h_x. (3) +``` + +The cut can reject a proposed target inventory before the full stage +polynomial is built. Passing it is not an operator identity or admission. + +## 3. Sharp capacity at the shortest query count + +Suppose L = n + 1. The rank-one complementary idempotent I - K has +diagonal one. Over F2 it is the all-one matrix. Thus + +```text +v_i u_j = 1 for i != j, and 0 for i = j. +``` + +In particular, n is even. Every k by k principal submatrix is I_k + J_k, +where J_k is all one. It has rank k when k is even, and rank k-1 when +k is odd. Substitution in (2) gives + +```text +r_x <= k + (k mod 2) + h_x. (4) +``` + +The algebraic bound is sharp. In a space with coordinates 0,1,...,k, +take, for i = 1,...,k, + +```text +u_i = e_0 + e_i, v_i = e_0^T + e_i^T, +P_i = e_0 e_0^T + e_i e_i^T. +``` + +These R_i have the required pairings. Each P_i is an idempotent of +rank two that contains its R_i. Their sum is diagonal: it is one on +each private coordinate and is k mod 2 on coordinate zero. Its rank +is exactly k + (k mod 2). This is a sharp local algebraic witness, +not a complete profitable caller. + +The written results also extend to any field of characteristic two. +In that case the rank-one complement is a b^T, with a_i b_i=1, rather +than necessarily the all-one matrix. Replace u_i by a_i u_i and v_i +by v_i/a_i. This preserves each R_i and makes every off-diagonal +pairing equal to one. The proofs below then use the same simplex. +The general cuts and the rank-two complement argument use only field +linear algebra and integer target counts. The executable filters and +finite controls in this package use F2; they do not enumerate extension +fields. This extension still gives no characteristic-zero reduction. + +## 4. At most two calls can have private axes + +This step uses Cinna Davis's minimum-query projector lemma from +`productive-controller-basis-search/GLOBAL-PROOF.md`. Its hypotheses +hold for every call with a private axis, even when other calls share +arbitrary axes. The other stages need not have independent multipliers. + +For a private axis at call s, its target derivative is P_s. Independence +of that target projector from Q gives + +```text +[P_s, sum_(j>s) R_j] = 0. +``` + +All private-axis target projectors commute with one another because +they are diagonal in the same output basis. They also satisfy +P_s R_s = R_s P_s = R_s. + +Here is the retained argument. Normalize the simplex to +u_i = e_i and v_i = 1 + e_i for i < n, with u_n = v_n = 1. For an +interior position s, set U_s = sum_(j>s) u_j and V_s = sum_(j>s) v_j. +Commutation forces the image of P_s to contain u_s,U_s and its row +space to contain v_s,V_s. These two pairs are independent. Their +pairing matrix is + +```text +[0 n-s; n-s 0] over F2. +``` + +There is no rank-two projector if n-s is even. If n-s is odd, the only +choice is P_s = u_s V_s + U_s v_s. Two different interior choices do +not commute: for s < t, P_s u_t = U_s, P_t u_t = u_t, and P_t U_s = 0. + +An initial private-axis call can coexist with an interior one only at +s = 1. Otherwise its forced two-dimensional image and row space have +zero pairing. A terminal private-axis call can coexist with an interior +one only at s = n-1, for the same reason. For n >= 4 one interior call +cannot be both positions. There are at most two private-axis calls. + +With b axes per full call, at most 2b axes can have multiplicity one. +Let s count those axes. The total axis occurrence count is b f. For +k >= 2, k + (k mod 2) <= 4k/3. With no idles, (4) therefore gives + +```text +R := sum_x r_x + <= 2s + (4/3)(bf-s) + <= (4bf+4b)/3. (5) +``` + +Also R <= 2bf. These are bounds on all main outputs together. They do +not count a stage map as a new independent field. + +For future callers with idles, let H = sum_x h_x. At most H private +axes can have h_x > 0. The same argument gives the weaker useful tradeoff + +```text +R - H <= (4bf + 4b + 2H)/3. (6) +``` + +Equation (6) is a linear rank budget. It is not an all-concave rejection +when idle calls can combine several axes at a concave price. + +## 5. Complete P104 price, for every concave tariff + +Both pinned source inventories have v = 104 ports, b = 8, and + +```text +sum_r r (paid[r] - helpers[r]) = Lambda = 1720 + = 2*b*v + 56. +``` + +The 56 includes the local owned-copy debt. The helper targets are +independent source inputs. Their complete bill is retained at every +full call. The inputs are the main P104 package and PR5599 at +09dd0965711ca7eeb169057a420abab1c9052137. The latter source changes +helper inputs and includes PR5565's paid profile. Its native result +is inherited here; this package does not rerun its native construction. + +For c_r = paid[r] - helpers[r], both exact profiles satisfy + +```text +sum_r c_r max(r-j,0) <= 0 for every integer j >= 1. (7) +``` + +The verifier checks the complete finite list. Beyond the largest +source rank, the sums are zero. Let g be any nondecreasing concave +tariff on the nonnegative integers, with g(0)=0 and g(1)=1. Its +successive slope drops a_j are nonnegative, and + +```text +g(r) = r - sum_(j>=1) a_j max(r-j,0). +``` + +Only finitely many terms matter at each source rank. Equation (7) gives + +```text +sum_r c_r g(r) >= Lambda. (8) +``` + +Also g(1+r) <= 1+r. There are n main targets per port and L-f thin +queries. The complete target-minus-paid moment is therefore at most + +```text +v (n+R) - v(L-f) - Lambda*f + = 104(f-1+R) - 1720f. (9) +``` + +For f = 0,1,2, the bound R <= 16f gives, respectively, -104, -56, -8. +For f >= 3, (5) gives + +```text +moment <= (3016 - 1520f)/3 < -8. (10) +``` + +Thus the complete moment is at most -8 for every such tariff. In +particular, this holds for g(r)=r^(1-kappa), 0 <= kappa < 1. Adding +nonnegative compiler or ordinary-work costs cannot change this failure +of the necessary recursive moment inequality. + +The same calculation gives an inventory design condition. Let a local +family have v ports, b>=1 transverse axes and net rank mass +Lambda=2bv+d. Suppose its paid-minus-helper hinge sums are nonpositive, +as in (7). If d>=v/2, no shortest caller with n>=4 can have a positive +complete concave moment. At f=0,1,2 the bounds are -v,-d,v-2d. For f>=3, +the bound is + +```text +v*(4b/3-1) + f*(v*(1-2b/3)-d). +``` + +It decreases in f. At f=3 and d=v/2 it is v*(1/2-2b/3)<0. +Thus d=4. + +## 7. Joint axis cuts + +There is also a necessary intersection cut. It can reject profiles that +pass every separate capacity test. Let S and T be the occurrence sets +of two axes x and y. Define + +```text +delta_x = 2|S| + h_x - r_x, +delta_y = 2|T| + h_y - r_y. +``` + +These numbers are nonnegative. In the factorizations E_x=A_x B_x and +E_y=A_y B_y from Section 2, the rows V_S occur in B_x and the columns +U_T occur in A_y. Since E_x is an idempotent and its row space is +contained in the row space of B_x, + +```text +rank(V_S (I-E_x)) <= rank(B_x)-r_x <= delta_x. +rank((I-E_y) U_T) <= rank(A_y)-r_y <= delta_y. +``` + +Decompose V_S U_T as + +```text +V_S E_x E_y U_T + V_S(I-E_x)U_T + V_S E_x(I-E_y)U_T. +``` + +The target projectors commute and select their target axis sets. Hence +the number r_xy of independent main jobs that contain both axes obeys + +```text +r_xy = rank(E_x E_y) + >= rank K[S,T] - delta_x - delta_y. (11) +``` + +This is a necessary cut for arbitrary query counts and includes the +stated idle terms. A negative right side gives no constraint. At full +capacity, both deltas vanish. The cut then forces target intersections +directly from the off-diagonal query Gram blocks. + +## 8. A longer paired-stage obstruction + +Consider a second, narrower family. Every call is full. There are +L=n+2=2m calls. Each of m independent stage blocks occurs exactly twice; +each block has eight axes and different blocks have disjoint axes. The +two calls in a pair need not be adjacent. All binary scalar bases and +all call orders remain allowed. There are no idles. + +Let r_c be the number of main targets that contain stage block c. +Every word coefficient is a product of whole blocks. Constant boundary +bases cannot add new monomials, so each target contains a whole block +or none of that block. The count r_c is at most four. +Suppose first that every r_c=4. Write I-K=XY, +where X has two columns, Y has two rows and YX=I_2. For each two-call +index set S_c, (2) forces K[S_c,S_c]=0. Thus + +```text +X[S_c,:] Y[:,S_c] = I_2. +``` + +Both two-by-two factors are invertible. Their product in the reverse +order is also I_2. Summing in c gives YX=m I_2, so m must be odd. +For any two distinct classes, K[S_c,S_d] has rank two. Equation (11) +therefore requires at least two common target coordinates for every +pair of stage blocks. + +At full capacity, E_c=A_c B_c has rank four with four inner columns. +It follows that B_c A_c=I_4. In particular, E_c U_c=U_c and V_c E_c=V_c. +Use the common basis in which all E_c are diagonal. Every row of U_0 +is nonzero, since U_0 V_0=I. No row can be supported in just one class: +U_0 X=0 and X[S_c,:] is invertible. Thus every main coordinate belongs +to at least two stage sets. + +Let d_j count the stage sets that contain coordinate j. We now have + +```text +n=2m-2, 2 <= d_j <= m, sum_j d_j=4m, +sum_j binomial(d_j,2) >= 2*binomial(m,2)=m(m-1). (12) +``` + +Only four units remain after assigning degree two to all coordinates. +Convexity makes the largest intersection sum by putting those units +on as few coordinates as possible. At m=5 this maximum is 19, below +20. For m>=6 it is + +```text +binomial(6,2)+(2m-3)*binomial(2,2) = 2m+12 < m(m-1). +``` + +Even m already fails the parity condition. Thus full capacity is +impossible for every m>=4, or n>=6. For m=3, two disjoint three-query +units on four fields attain full capacity. Their three corresponding +stage pairs each reach all four outputs. This positive exact word +passes (2) and (11), and prevents an invalid extension of the shortest +query bound to all longer words. + +At least one stage occurrence must therefore be lost for n>=6: + +```text +sum_c r_c <= 4m-1. +``` + +The complete linear-tariff bound for either pinned P104 inventory is + +```text +104*(n+8*(4m-1)) - 2m*1720 = 96m-1040. (13) +``` + +It is negative for m<=10. The same bound holds for every normalized +nondecreasing concave tariff by (8). This rejects, in particular, the +fourteen-call/twelve-field candidate and the eighteen-call/sixteen-field +candidate for every such tariff. The former had a floating optimistic +crossing near .003393385 before the intersection cut. That crossing is +not a caller or a kappa claim. + +For larger m, discrete concavity gives the sharper power-tariff bound + +```text +M_m(t) <= 104*((2m-5)*17^t + 3*25^t) - 2m*sum_r c_r r^t. (14) +``` + +The verifier proves that this bound is negative at t=997/1000 for +m=4 and m=26. It is affine in m, so it is negative for all 4<=m<=26. +All negative coefficients have lower rank than all positive ones. +The sign-separation argument from Section 6 extends this rejection to +every 0s) U_j, and +the corresponding row spaces. Their pairing matrix is + +```text +[0 (n-s)I_q; (n-s)I_q 0]. +``` + +Even n-s is impossible; odd n-s gives the unique projector +`U_s V_tail + U_tail V_s`. The noncommuting interior pair and both +zero-pairing endpoint arguments in Section 4 apply to these blocks. +Thus at most two call positions have private axes. + +The total main transverse rank therefore satisfies + +```text +R <= 2qbf, R <= q*(4bf+4b)/3. +``` + +There are nq target jobs and q(L-f) thin paid queries. With q=v=104, +b=8 and the same autonomous helper inventory per full call, the +complete price calculation in Section 5 is unchanged. Its sharp -8 +bound covers arbitrary cross-port scalar codes at N=104n, L=n+1. +The proof also holds over characteristic-two extension fields. + +This extension does not extend Section 8's complete paired-stage price +bound to arbitrary coupled ports. At L=n+2 the complement has rank 2q; +one lost target occurrence need not mean one loss on every port. +Different main counts with N not equal to q(L-1), mixed query ranks, +and main/helper mixing also need separate arguments. The general +rank and intersection cuts still apply after each rank-q query and +rank-2q projector are factored into compatible rank-one/rank-two terms. + +## Credit and verification boundary + +Cinna Davis supplies the simplex, private-projector obstruction, the +sharp five-query word, and the controller lineage. The new result is +the Gram-submatrix rank and intersection cuts, their sharp repeat +capacity, their use for arbitrary coordinate overlap, the paired-stage +obstruction, and the complete all-concave P104 bound. +The equality cuts in PR5588 motivated the search; passing those cuts +alone did not supply an endpoint. The scalar, native, helper, compiler, +precision and analytic sources retain their attribution in SOURCES.json +and the package README. + +The written arguments prove the unbounded statements under their stated +algebraic hypotheses. The exact verifier checks finite instances and +discriminating controls. It is not a proof-assistant kernel or an +independent human review. No selected frontier is changed. diff --git a/research/paired-stage-chronology-cut/inputs/PR5617-RESULT.json b/research/paired-stage-chronology-cut/inputs/PR5617-RESULT.json new file mode 100644 index 0000000000..fe5ac435fe --- /dev/null +++ b/research/paired-stage-chronology-cut/inputs/PR5617-RESULT.json @@ -0,0 +1,287 @@ +{ + "authenticated_inputs": 5, + "block_simplex_controls": { + "includes_port_count_104": true, + "rank_controls": 80, + "total_dimension_contract": "N=q*n and L=n+1" + }, + "complete_prices": { + "PR5599_at_09dd0965": { + "helpers": { + "1": 2, + "2": 5, + "4": 89, + "5": 11, + "7": 5, + "8": 16, + "9": 412 + }, + "hinges_at_1_through_9": [ + -1187, + -1893, + -2145, + -1904, + -1660, + -1259, + -840, + -412, + 0 + ], + "n12_previous_equality_cut": { + "checks": [ + { + "k": 1, + "paid": "966665/32", + "paid_minus_targets": "22572866061/1048576", + "targets": "9102812659/1048576" + } + ], + "polynomial": { + "0": 39450, + "1": -30814, + "17": 832, + "2": -6356, + "25": 416, + "3": -6902, + "4": -42, + "5": -2198, + "6": -252, + "7": -126, + "8": 224, + "9": 5768 + }, + "schema": "native-equality-cut/v1", + "scope": "necessary conditions; no native admission or kappa claim", + "status": "PASS_NECESSARY_EQUALITY_CUTS", + "tail": { + "certified_from_k": 1, + "first_degree": 0, + "leading_coefficient": 39450, + "remaining_absolute_sum": 53930, + "strict_sign": 1 + }, + "width": null + }, + "n12_without_incidence_cut_positive": true, + "net_rank_mass": 1720, + "paid": { + "1": 2203, + "2": 459, + "3": 493, + "4": 92, + "5": 168, + "6": 18, + "7": 14 + }, + "paired_margin_at_kappa_003": { + "26": { + "denominator": 281474976710656, + "lower_decimal": "-30.924007237089384148021053988487", + "lower_numerator": -8704334216859892, + "upper_decimal": "-30.924007236782344421044399496168", + "upper_numerator": -8704334216773468 + }, + "4": { + "denominator": 281474976710656, + "lower_decimal": "-884.87666334030629400331235956401", + "lower_numerator": -249070638205515704, + "upper_decimal": "-884.87666334025968239984649699181", + "upper_numerator": -249070638205502584 + } + }, + "two_field_margin_at_kappa_002": { + "denominator": 281474976710656, + "lower_decimal": "-20.665999385967381840600864961743", + "lower_numerator": -5816961695867600, + "upper_decimal": "-20.665999385949994859856815310195", + "upper_numerator": -5816961695862706 + } + }, + "original_P104": { + "helpers": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "hinges_at_1_through_9": [ + -1378, + -2047, + -2159, + -1882, + -1544, + -1134, + -708, + -293, + 0 + ], + "n12_previous_equality_cut": { + "checks": [ + { + "k": 1, + "paid": "7927437/256", + "paid_minus_targets": "23507257869/1048576", + "targets": "8963524083/1048576" + } + ], + "polynomial": { + "0": 42124, + "1": -34006, + "17": 832, + "2": -7798, + "25": 416, + "3": -5446, + "4": -854, + "5": -1008, + "6": -224, + "7": 154, + "8": 1708, + "9": 4102 + }, + "schema": "native-equality-cut/v1", + "scope": "necessary conditions; no native admission or kappa claim", + "status": "PASS_NECESSARY_EQUALITY_CUTS", + "tail": { + "certified_from_k": 1, + "first_degree": 0, + "leading_coefficient": 42124, + "remaining_absolute_sum": 56548, + "strict_sign": 1 + }, + "width": null + }, + "n12_without_incidence_cut_positive": true, + "net_rank_mass": 1720, + "paid": { + "1": 2429, + "2": 557, + "3": 389, + "4": 112, + "5": 108, + "6": 16, + "7": 13, + "9": 1 + }, + "paired_margin_at_kappa_003": { + "26": { + "denominator": 281474976710656, + "lower_decimal": "-72.488495253100026616266404744238", + "lower_numerator": -20403697513156828, + "upper_decimal": "-72.488495252800561274852952919900", + "upper_numerator": -20403697513072536 + }, + "4": { + "denominator": 281474976710656, + "lower_decimal": "-891.27119995815408515227318275720", + "lower_numerator": -250870540251099848, + "upper_decimal": "-891.27119995810863883889396674931", + "upper_numerator": -250870540251087056 + } + }, + "two_field_margin_at_kappa_002": { + "denominator": 281474976710656, + "lower_decimal": "-22.264631701482969106109521817416", + "lower_numerator": -6266936689646252, + "upper_decimal": "-22.264631701466019109147964627482", + "upper_numerator": -6266936689641481 + } + } + }, + "incidence_controls": { + "gl2_pair_controls": 36, + "n12_all_concave_upper": -368, + "n16_all_concave_upper": -176, + "packing_dp_max_m": 65, + "paired_stage_cases": { + "3": { + "max_intersections": 12, + "parity_admissible": true, + "required": 6 + }, + "4": { + "max_intersections": 16, + "parity_admissible": false, + "required": 12 + }, + "5": { + "max_intersections": 19, + "parity_admissible": true, + "required": 20 + }, + "6": { + "max_intersections": 24, + "parity_admissible": false, + "required": 30 + }, + "7": { + "max_intersections": 26, + "parity_admissible": true, + "required": 42 + } + } + }, + "limits": { + "formal_kernel": false, + "independent_review": false, + "model": "Binary constant bases; commuting independent involutive axes; autonomous helpers", + "native_word_replay": false, + "new_kappa": false + }, + "operator_controls": { + "deleted_query_rejected": true, + "sharp_five_query_degrees": { + "0": 2, + "2": 2 + }, + "sharp_margin_at_linear_tariff": -8, + "six_query_gram": [ + 6, + 5, + 3, + 48, + 40, + 24 + ], + "six_query_paired_degrees": { + "3": 4 + }, + "two_literal_interpreters": true + }, + "rank_cut_controls": { + "intersection_factor_cases": 21808, + "kernel_identity_cases": 172, + "non_idempotent_control_rejected": true, + "simplex_projector_census": { + "2": { + "idempotent_sums": 7, + "ranks": [ + 0, + 2 + ], + "words": 256 + }, + "3": { + "idempotent_sums": 222, + "ranks": [ + 2, + 4 + ], + "words": 4096 + } + } + }, + "reusable_filter_controls": { + "fourteen-query-intersection-rejected": "REJECT_NECESSARY_CUT", + "invalid_query_frame": "REJECTED", + "shortest-repeat-rejected": "REJECT_NECESSARY_CUT", + "six-query-positive": "PASS_NECESSARY_CUTS_ONLY" + }, + "simplex_controls": { + "max_main_fields": 64, + "private_stage_controls": 6448, + "sharp_local_capacities": 64, + "simplex_pairings": 47904 + }, + "status": "PASS_CALLER_STAGE_CAPACITY_CUTS" +} diff --git a/research/paired-stage-chronology-cut/inputs/PR5617-cuts.py b/research/paired-stage-chronology-cut/inputs/PR5617-cuts.py new file mode 100644 index 0000000000..9c1f001a1c --- /dev/null +++ b/research/paired-stage-chronology-cut/inputs/PR5617-cuts.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python3 +"""Screen a binary query frame and proposed target axis sets. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +Passing these necessary cuts does not certify an operator word or a price. +""" +import argparse +from itertools import combinations +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rank(rows): + rows = list(rows) + pivot = 0 + for bit in range(max(rows, default=0).bit_length()-1, -1, -1): + chosen = next((i for i in range(pivot, len(rows)) if rows[i] >> bit & 1), None) + if chosen is None: + continue + rows[pivot], rows[chosen] = rows[chosen], rows[pivot] + for i in range(pivot+1, len(rows)): + if rows[i] >> bit & 1: + rows[i] ^= rows[pivot] + pivot += 1 + return pivot + + +def audit(candidate): + n, us, vs = candidate['n'], candidate['u'], candidate['v'] + require(type(n) is int and n > 0, 'n must be a positive integer') + require(len(us) == len(vs) and len(us) > n, 'A query frame needs L>n terms') + require(all(type(x) is int and 0 < x < (1 << n) for x in us+vs), 'Invalid query vector') + require(all((u & v).bit_count() % 2 == 0 for u, v in zip(us, vs)), 'Non-nilpotent query') + total = [0]*n + for u, v in zip(us, vs): + for j in range(n): + if u >> j & 1: + total[j] ^= v + require(total == [1 << i for i in range(n)], 'Query frame does not sum to identity') + gram = [sum(((v & u).bit_count() % 2) << i for i, u in enumerate(us)) for v in vs] + axes, singles, failures = [], [], [] + for axis in candidate['axes']: + calls, outputs = axis['calls'], axis['outputs'] + idles = axis.get('idle_terms', 0) + require(len(calls) == len(set(calls)) and len(outputs) == len(set(outputs)), 'Duplicate index') + require(all(type(i) is int and 0 <= i < len(us) for i in calls), 'Invalid call index') + require(all(type(i) is int and 0 <= i < n for i in outputs), 'Invalid output index') + require(type(idles) is int and idles >= 0, 'Invalid idle count') + require(all(axis['name'] != a['name'] for a in axes), 'Duplicate axis name') + block = [sum(((gram[i] >> j) & 1) << t for t, j in enumerate(calls)) for i in calls] + block_rank = rank(block) + capacity = 2*len(calls)+idles-block_rank + deficit = 2*len(calls)+idles-len(outputs) + singles.append({'axis': axis['name'], 'target_count': len(outputs), + 'capacity': capacity, 'gram_rank': block_rank}) + if len(outputs) > capacity: + failures.append({'kind': 'axis_capacity', 'axis': axis['name'], + 'requested': len(outputs), 'maximum': capacity}) + axes.append({**axis, 'deficit': deficit}) + intersections = [] + for a, b in combinations(axes, 2): + block = [sum(((gram[i] >> j) & 1) << t for t, j in enumerate(b['calls'])) + for i in a['calls']] + demand = max(0, rank(block)-a['deficit']-b['deficit']) + actual = len(set(a['outputs']) & set(b['outputs'])) + intersections.append({'axes': [a['name'], b['name']], 'required': demand, 'actual': actual}) + if actual < demand: + failures.append({'kind': 'axis_intersection', 'axes': [a['name'], b['name']], + 'requested': actual, 'minimum': demand}) + return {'status': 'REJECT_NECESSARY_CUT' if failures else 'PASS_NECESSARY_CUTS_ONLY', + 'n': n, 'query_count': len(us), 'query_surplus': len(us)-n, + 'single_axis': singles, 'intersections': intersections, 'failures': failures, + 'limits': 'Assumes compatible full projectors and independent target jobs. Does not construct them or price helpers, native maps, scalar work or compiler costs.'} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('candidate', type=Path) + args = parser.parse_args() + result = audit(json.loads(args.candidate.read_text())) + print(json.dumps(result, indent=2, sort_keys=True)) + raise SystemExit(bool(result['failures'])) diff --git a/research/paired-stage-chronology-cut/verify.py b/research/paired-stage-chronology-cut/verify.py new file mode 100644 index 0000000000..aa6ed1495a --- /dev/null +++ b/research/paired-stage-chronology-cut/verify.py @@ -0,0 +1,164 @@ +#!/usr/bin/env python3 +"""Replay the exact paired-stage bounds and the chronology controls. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +import hashlib +import json +from itertools import permutations, product +from pathlib import Path +import types +from chronology import add, outer, mul, rank, family, mixed, need + +HERE = Path(__file__).resolve().parent + + +def literal(us, vs, ps, labels, chosen=None): + n = len(ps[0]); identity = [1 << i for i in range(n)] + word = {0: identity} + for u, v, p, label in zip(us, vs, ps, labels): + factors = [{0: identity, 1: outer(u, v, n)}] + if chosen is None or chosen == label: + bit = 1 << (label + 1) if chosen is None else 2 + factors.append({0: identity, bit: p}) + for factor in factors: + nxt = {} + for a, x in factor.items(): + for b, y in word.items(): + if a & b: + continue + key = a | b + nxt[key] = add(nxt.get(key, [0]*n), mul(x, y)) + word = nxt + return word + + +def power_interval(r, precision=48): + value = pow(r, 997) << (precision*1000) + lo, hi = 0, r << precision + while lo < hi: + mid = (lo + hi + 1)//2 + if pow(mid, 1000) <= value: + lo = mid + else: + hi = mid-1 + need(pow(lo, 1000) <= value < pow(lo+1, 1000), 'root enclosure') + return lo, lo if pow(lo, 1000) == value else lo+1 + + +def interval(poly, powers): + lo = hi = 0 + for r, c in poly.items(): + a, b = powers[r] + lo += c*(a if c >= 0 else b) + hi += c*(b if c >= 0 else a) + return {'lower_numerator': lo, 'upper_numerator': hi, 'denominator': 1 << 48} + + +def moment(profile, m, loss): + poly = {r: 2*m*(profile['helpers'].get(str(r), 0)-profile['paid'].get(str(r), 0)) for r in range(1, 10)} + poly[17] = 104*(2*m-6+loss) + poly[25] = 104*(4-loss) + return {r: c for r, c in poly.items() if c} + + +def run(): + context = json.loads((HERE/'SOURCE-CONTEXT.json').read_text()) + for source in context: + need(hashlib.sha256((HERE/source['file']).read_bytes()).hexdigest() == source['sha256'], 'source bytes') + old = types.ModuleType('old_cuts') + exec(compile((HERE/'inputs/PR5617-cuts.py').read_text(), 'PR5617-cuts.py', 'exec'), old.__dict__) + profiles = json.loads((HERE/'inputs/PR5617-RESULT.json').read_text())['complete_prices'] + # Enumerate every rank-two projector on four binary coordinates. + projectors = [] + for rows in product(range(16), repeat=4): + rows = list(rows) + if rank(rows) == 2 and mul(rows, rows) == rows: + projectors.append(rows) + pairs = 0; counts = {} + for p in projectors: + for q in projectors: + e = add(p, q) + if mul(e, e) == e: + r = rank(e); intersection = rank(mul(p, q)) + need(mul(p, q) == mul(q, p) and r == 4-2*intersection, 'pair parity') + counts[r] = counts.get(r, 0)+1; pairs += 1 + need(len(projectors) == 560 and set(counts) == {0, 2, 4}, 'complete projector census') + witnesses = [] + for g in [3, 5, 7, 15, 31, 511]: + candidate, ps, labels = family(g); n = candidate['n'] + for u, v, p in zip(candidate['u'], candidate['v'], ps): + r = outer(u, v, n) + need(rank(p) == 2 and mul(p, p) == p and mul(p, r) == mul(r, p) == r, 'full-call compatibility') + screen = old.audit(candidate) + need(screen['status'] == 'PASS_NECESSARY_CUTS_ONLY', 'predecessor cuts') + loss = 4*(g+2)-sum(len(a['outputs']) for a in candidate['axes']) + need(loss == 8, 'constant loss') + defects = mixed(candidate, ps, labels) + need(len(defects) == g-1 and set(defects.values()) == {4}, 'chronology rejection') + if g <= 7: + for c in range(g+2): + word = literal(candidate['u'], candidate['v'], ps, labels, c) + e = [0]*n + for p, label in zip(ps, labels): + if label == c: e = add(e, p) + need(rank(add(word.get(3, [0]*n), e)) == defects.get(c, 0), 'independent mixed coefficient') + witnesses.append({'g': g, 'n': n, 'loss': loss, 'prior_intersection_cuts': len(screen['intersections']), 'mixed_rejections': len(defects)}) + # The first copy has three private stages and two repair queries. + candidate, ps, labels = family(3) + indices = [i for i, u in enumerate(candidate['u']) if u < 16] + orders = 0 + for order in permutations(indices): + c = {'n': 4, 'u': [candidate['u'][i] for i in order], 'v': [candidate['v'][i] for i in order]} + p = [ps[i][:4] for i in order]; labs = [labels[i] for i in order] + need(mixed(c, p, labs), 'all-order obstruction control') + orders += 1 + # Two complete three-query units give a positive six-query word. + us = []; vs = []; ps = []; labels = [] + for label, (u, v) in enumerate([(1, 2), (2, 1), (3, 3)]): + for shift in [0, 2]: + us.append(u << shift); vs.append(v << shift) + ps.append([1 << j if shift <= j < shift+2 else 0 for j in range(4)]) + labels.append(label) + need(mixed({'n': 4, 'u': us, 'v': vs}, ps, labels) == {}, 'positive chronology') + word = literal(us, vs, ps, labels) + need(set(word) == set(range(16)) and all(a == [1, 2, 4, 8] for a in word.values()), 'full positive word') + bad = us.copy(); bad.pop() + try: + mixed({'n': 4, 'u': bad, 'v': vs[:-1]}, ps[:-1], labels[:-1]) + except ValueError: + pass + else: + raise ValueError('deleted query accepted') + powers = {r: power_interval(r) for r in list(range(1, 10))+[17, 25, 4089]} + prices = {} + for name, p in profiles.items(): + c = {r: p['paid'].get(str(r), 0)-p['helpers'].get(str(r), 0) for r in range(1, 10)} + need(sum(r*v for r, v in c.items()) == 1720, 'complete linear price') + need(all(sum(v*max(r-j, 0) for r, v in c.items()) <= 0 for j in range(1, 10)), 'concave price') + last_even, last_odd = (47, 89) if name.startswith('PR5599') else (50, 93) + results = {} + for loss, last, first, step in [(2, last_even, 4, 1), (4, last_odd, 5, 2)]: + for m in [first, last, last+step]: + poly = moment(p, m, loss) + need(max(r for r, v in poly.items() if v < 0) < min(r for r, v in poly.items() if v > 0), 'sign separation') + bound = interval(poly, powers) + need(bound['upper_numerator'] < 0 if m <= last else bound['lower_numerator'] > 0, 'exact range endpoint') + results[f'loss_{loss}_m_{m}'] = bound + g = 511; poly = {r: 2*(g+2)*(-v) for r, v in c.items()} + poly[9] += 208*g; poly[1+8*g] = 208 + bound = interval(poly, powers); need(bound['lower_numerator'] > 0, 'positive relaxed price') + results['invalid_star_relaxation_g511'] = bound + prices[name] = results + return {'status': 'PASS_PAIRED_STAGE_CHRONOLOGY_CUT', 'projectors': len(projectors), 'idempotent_pairs': pairs, 'pair_ranks': {str(k): v for k, v in counts.items()}, 'witnesses': witnesses, 'all_relative_orders_g3': orders, 'positive_full_word_coefficients': len(word), 'prices': prices, 'limits': {'new_kappa': False, 'native_replay': False, 'independent_review': False, 'formal_kernel': False, 'source_history_preflight': False}} + + +if __name__ == '__main__': + result = run() + text = json.dumps(result, indent=2, sort_keys=True)+'\n' + import sys + if '--write' in sys.argv: + (HERE/'RESULT.json').write_text(text) + else: + need(json.loads((HERE/'RESULT.json').read_text()) == result, 'recorded result differs') + print(result['status'])