diff --git a/research/pauli-twisted-history-threshold/PROOF.md b/research/pauli-twisted-history-threshold/PROOF.md new file mode 100644 index 0000000000..c09c2bd7ee --- /dev/null +++ b/research/pauli-twisted-history-threshold/PROOF.md @@ -0,0 +1,127 @@ +# Sharp paid-history threshold for the phase-complete Pauli alphabet + +Let K=Q(i), X=[[0,1],[1,0]], Z=diag(1,-1), and +G=. This is the 16-element group of actual matrices +{i^c X^u Z^v: 0<=c<4, u,v in {0,1}}. Its projective quotient has +four classes. At each positive width f define P=X^tensor f, +C=Z^tensor f and R=span_K{I,P,C,PC}. Ordinary operations are left +actions from R, arbitrary K-linear row combinations, COPY and CLEAR. +Scalar coefficients, word lengths and choices may vary with f. + +Begin with ordinary combinations of N independent whole-field inputs, +including every independent dirty input, and zero scratch. A paid call +acts on one actual current field and returns one additional K-linear row +(not assumed linearly independent of earlier rows) at +the same capacity. It may depend on earlier paid outputs and need not +commute with R. Conceptually retain all actual paid rows after overwrites +or clears. No freely supplied nonordinary initial observation is allowed. + +For q distinct input owners v_j, request H_j w_vj up to ordinary initial +backgrounds, where H_j=(a_j I+b_j X)^tensor f and +a_j b_j (a_j^2-b_j^2) != 0. Correctness is on the entire independent +input space. Then every such program has at least q paid returns for +every f>=2. At f=1 all targets are ordinary and zero returns suffice. +If each H_j is an available paid primitive, q direct calls attain the +bound for f>=2. Without this last hypothesis this is a lower bound, +not a supplier construction or an attainable native-call count. + +## 1. Exact phases and actual algebra + +The lift of i^c X^u Z^v is i^(cf) P^u C^v. In particular, +PC=(-1)^f CP, P^2=C^2=I. Phases merge into K scalars; the algebra is +the actual matrix image, not the untwisted group algebra of four labels. +For positive f the four matrices I,P,C,PC are independent. To see this, +use the X-eigenbasis of each tensor factor: P is diagonal with entry +(-1)^k on a binary string of weight k, and C maps each string to its +complement. The diagonal supports I,P are disjoint from the complement +supports C,PC; within each pair both parities occur. Thus dim R=4. +R is commutative at even f and noncommutative at odd f. + +For one target write l+=a+b and l-=a-b. Both are nonzero. In this basis +H is diagonal with entry t_k=l+^(f-k) l-^k. For 0<=k<=f-2, + + t_k - t_(k+2) = 4ab l+^(f-k-2) l-^k != 0. (1) + +The basis change is an exact invertible common conjugation, used only +in the proof; it is not granted as a free physical instruction. + +## 2. Odd widths at least three: full module separation + +Suppose A H belongs to R, where A=alpha I+beta P+gamma C+delta PC. +The diagonal entries of AH on parity epsilon are +(alpha+beta epsilon)t_k. An ordinary matrix has a constant diagonal +coefficient on each parity. Compare k=0,2 in even parity and k=1,3 in +odd parity. By (1), alpha+beta=alpha-beta=0, hence alpha=beta=0. + +At row complement(s), column s, the remaining entry is +(gamma+delta (-1)^(f-k))t_k. Ordinary complement entries are constant +within each input parity. The same two comparisons give +gamma-delta=gamma+delta=0 at odd f, hence gamma=delta=0. This uses +characteristic zero, invertibility of l+,l- and f>=3. Therefore + + R intersect R H = {0}. (2) + +This proof allows coefficients in the full actual R. It does not +pretend its odd-width matrix blocks are one-dimensional characters. + +Represent current fields as rows in End_K((K^2)^tensor f)^N. Let I0=R^N. +After m returns t_1,...,t_m, every available field belongs to +M=I0+sum_j R t_j: ordinary operations preserve it, and each paid +call adjoins its actual output row. Thus dim M <=4N+4m. Each target +generates R H_j e_vj, of dimension four because H_j is invertible. +Equation (2) separates it from the ordinary row at that owner, and +distinct owners separate the q modules from one another. Consequently +dim M >=4N+4q and m>=q. A growing finite N or finite word length +cancels at each width independently. + +## 3. Even widths at least two: one actual character suffices + +Now P,C commute. Set E=(I+P)(I+C)/4. It is a nonzero idempotent, +EP=EC=E, so ER=K E. This assertion would be false at odd widths. +In the same tensor eigenbasis, on every even-weight string s, +E has entry 1/2 at (s,s) and at (s,complement(s)); odd-weight rows +are zero. Complements are distinct at every positive width. + +The diagonal entries of EH at weights zero and two are t_0/2 and +t_2/2. Both corresponding entries of E are 1/2. Their difference is +2ab l+^(f-2), nonzero by (1). Hence EH is not a scalar multiple of E, +including at f=2. This does not require R intersect RH to vanish. + +Project all history rows on the left by E. Initial projected history +is the direct sum of K E at each independent owner. Since ER=K E, +each actual paid return can enlarge this projected span by at most +one dimension. Each requested EH_j e_vj adds one new dimension modulo +initial history; distinct owners make these q directions independent. +Therefore m>=q. This projection is an analysis of information already +available, not a free additional paid call or an assumed field split. + +## 4. Sharp threshold, scope and predecessor distinction + +At f=1, R=M_2(K) and h_j=a_j I+b_j X is ordinary. This proves the +width-one exception. With H_j available, one call on each original +owner gives the matching upper bound. Calls can preserve originals +by the allowed ordinary COPY; independent dirty inputs are not used +as zero scratch. No claim is made about a more restricted paid alphabet. + +PR5446's general projective-coset theorem gives only f>=2p-1=7 here. +PR5450 proves threshold two for the smaller R=span{I,X^tensor f}. +Its projector (I+P)/2 does not have one-dimensional ER for the enlarged +group: the extra C direction survives. The even-width projector and +odd-width full module argument above discharge that missing implication. +The history-dimension method and classical Pauli/character algebra are +credited, not claimed as new general theorems. + +Free initial paid history can invalidate the count. Repeated owners +cannot each be charged; projectively ordinary targets such as 2X cost +zero despite lying outside the finite G. If a=0 or b=0 the target is +ordinary; if a=+/-b the invertibility and comparisons used in the odd +case fail. Changing geometry, cross-column ordinary operations, +multiple independent outputs per call, nonlinear input-dependent +programs and approximation are excluded. This standalone theorem does +not establish a charge at a cached physical caller boundary, a new +recursive profile, precision/tape costs, or an integer-multiplication kappa. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +Predecessor credit: Chris R / Clear1nsight and PR5425/5446's retained +history authors; Ali Romman's PR5450; classical tensor-power separation, +finite group representation theory and the retained native/compiler lineage. diff --git a/research/pauli-twisted-history-threshold/README.md b/research/pauli-twisted-history-threshold/README.md new file mode 100644 index 0000000000..02501f470b --- /dev/null +++ b/research/pauli-twisted-history-threshold/README.md @@ -0,0 +1,124 @@ +# Full-Pauli paid history has sharp width threshold two + +The standalone one-return-per-owner lower bound survives enlarging the ordinary +alphabet from `{I,X}` to the full phase-complete Pauli group ``. +For targets `(aI+bX)^tensor f` with `ab(a^2-b^2) != 0`, width one costs zero +in this ordinary model; every width at least two requires at least q new +single-row paid returns for q distinct independent input owners. The matching +q-call upper bound requires each requested target operator to be an available +paid primitive. This is a scoped algebraic result, with no new kappa. + +The [uniform proof](PROOF.md) accounts for the actual phase factor +`(X Z)^tensor f = X^tensor f Z^tensor f` and +`X^tensor f Z^tensor f = (-1)^f Z^tensor f X^tensor f`. +At even widths, a one-dimensional character detects all requested owners. +At odd widths at least three, the proof uses full ordinary/target module +separation. The one-character argument from the smaller alphabet does not +survive unchanged: its projected ordinary span has dimension two here. + +This answers the larger-group next question in +[PR5450](https://github.com/CrocSwap/integer-mult-bounds/pull/5450). +[PR5446](https://github.com/CrocSwap/integer-mult-bounds/pull/5446)'s general +projective-group theorem gives only width at least seven when p=4. Its valid +general proof is not repaired or replaced. At width two the full ordinary +and target spans intersect in dimension two, so demanding disjoint full +spans would miss the sharp bound. [SOURCES.json](SOURCES.json) records exact +immutable proof citations and hashes of the inspected UTF-8 text. + +## Verification + +```sh +python3.12 -B scripts/research_package.py --package research/pauli-twisted-history-threshold +# Git-free direct commands, from any directory: +python3.12 -I -B /path/to/package/verify.py +python3.12 -I -O -B /path/to/package/verify.py +python3.12 -I -B /path/to/package/check_modular.py +python3.12 -I -O -B /path/to/package/check_modular.py +python3.12 -I -B /path/to/package/test_mutations.py +``` + +All commands use only the standard library and explicit checks active under +optimization. The first engine uses exact Gaussian rationals and literal +Kronecker matrices, cross-checked against an independent Hamming-distance +entry formula. [RESULT.json](RESULT.json) records 24 complete tensor cases, +all 64 actual phase-group lifts across four widths, 18 full owner/history +checks, 366 scalar identities and 13 boundary controls. The source +square-root-of-X target is included. Owner rows retain an independent dirty +coordinate and check that duplicate owners or a supplied cached target cannot +be charged again. Other controls cover ordinary scalar multiples, singular +targets, zero coefficients, invalid widths and using the even projector at +odd width. + +The separate `check_modular.py` imports no primary-engine code. It constructs +the operators directly from bit indices and uses independent modular Gaussian +elimination: 512 complete target cases over F5 and F13, eight phase twists, +eight projectively ordinary controls and 3,072 nonzero separation identities. +These finite-field checks exercise the algebra; they are not physical Q(i) +input tests. Neither executable proves the all-width theorem: that reasoning +is in PROOF.md. Separate peer review and any limitations are reported with +the publication rather than inferred from a PASS marker. + +Six additional semantic mutants run in disposable files under optimized Python, +with receipt comparison disabled. They must fail at named predicates when +width-dependent phase is dropped, the odd algebra is made commutative, the +smaller projector is reused, the target coefficient sign changes, singular +targets are accepted, or a cached target is charged again. These controls +change no frozen source and cannot pass merely because RESULT.json differs. + +The package has no external executable input and imports no predecessor code. +Public proof citations are not Git-object replay dependencies, so the +predecessors' unmerged commits are not needed for cold execution. The only +Git provenance pins are the task catalogue and selected record at the +canonical base. The official committed exporter therefore needs no +`--input-ref`; it preserves the unchanged package manifest. Source-history +validation checks those declared provenance pins, not the availability or +truth of the cited external proofs. The new argument is self-contained. + +## Scope and coordination + +The full initial state is independent, with only ordinary observations and +zero scratch. Ordinary coefficients and finite word lengths may vary with +width; paid calls may have feedback and need not commute with ordinary maps. +Each call returns one actual transformed whole-field row at fixed capacity. +The proof explicitly retains every paid output after overwrite or clear. +It assumes neither a free arbitrary matrix coefficient nor multiple outputs +from one call. A common eigenbasis is a proof device, not a free instruction. + +No actual parent-cut observation ledger is supplied. Cached paid history, +dependent owners, noninvertible targets, cross-column ordinary operations, +nonlinear programs, multiple-output paid calls and approximate recovery need +different arguments. Physical phase/compiler admission, recursive profiles, +precision, storage, tape cost and the selected frontier remain outside this +result. It does not certify a complete multiplication theorem. + +[Discussion5476](https://github.com/CrocSwap/integer-mult-bounds/discussions/5476) +is the canonical investigation. The base is +`32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority revision seven. +The scope change from the historical uniform-transfer card is explicit in +[TASK.json](TASK.json). Initial overlap covered 342 open PRs and 4,736 +Discussion records with complete pagination, plus the latest released +handoffs; public cached prose does not exclude unpublished work. +PR5449's general finite history quotient and PR5447's physical input kernels +are separate scopes. No physical application is inferred from either. + +## Open next questions + +Bind this lower bound to one actual versioned physical cut, including every +cached observation and owner. Without that ledger the standalone hypothesis +cannot justify another caller charge. A further target-family extension needs +one justified physical target and a concrete cost consequence; this proof +does not classify arbitrary Pauli-nonordinary matrices. See TASK.json for the +first steps and blockers. + +## Credit + +Chris R / Clear1nsight and the retained PR5425/5446 authors supply the +paid-history argument and general projective separation. Ali Romman's +PR5450 supplies the smaller bit-flip specialization and larger-group handoff. +Classical Pauli representation theory, involution characters, tensor-power +separation and the retained native/helper/compiler/analytic lineage retain +their credit. No predecessor implementation is imported. + +JoyboyBrian, with substantial OpenAI Codex assistance in proof, exact +implementation, controls and writing. Apache-2.0. No independent human or +formal-kernel acceptance is claimed. diff --git a/research/pauli-twisted-history-threshold/RESULT.json b/research/pauli-twisted-history-threshold/RESULT.json new file mode 100644 index 0000000000..a35b658fe2 --- /dev/null +++ b/research/pauli-twisted-history-threshold/RESULT.json @@ -0,0 +1,180 @@ +{ + "actual_group_lifts": 64, + "boundary_controls": 13, + "literal_cases": [ + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 4, + "sample": 0, + "width": 1 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 6, + "sample": 0, + "width": 2 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 0, + "width": 3 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 0, + "width": 4 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 4, + "sample": 1, + "width": 1 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 6, + "sample": 1, + "width": 2 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 1, + "width": 3 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 1, + "width": 4 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 4, + "sample": 2, + "width": 1 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 6, + "sample": 2, + "width": 2 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 2, + "width": 3 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 2, + "width": 4 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 4, + "sample": 3, + "width": 1 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 6, + "sample": 3, + "width": 2 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 3, + "width": 3 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 3, + "width": 4 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 4, + "sample": 4, + "width": 1 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 6, + "sample": 4, + "width": 2 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 4, + "width": 3 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 4, + "width": 4 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 4, + "sample": 5, + "width": 1 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 6, + "sample": 5, + "width": 2 + }, + { + "candidate_character_dimension": 2, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 5, + "width": 3 + }, + { + "candidate_character_dimension": 1, + "ordinary": 4, + "ordinary_plus_target": 8, + "sample": 5, + "width": 4 + } + ], + "owner_and_history_controls": 18, + "scalar_identity_cases": 366, + "scope": "finite checks corroborate PROOF.md; no physical caller admission", + "status": "PASS_PAULI_TWISTED_HISTORY_THRESHOLD", + "theorem": "zero at width one; at least q at every width >=2", + "upper_bound_condition": "each requested H is an available paid primitive" +} diff --git a/research/pauli-twisted-history-threshold/SOURCES.json b/research/pauli-twisted-history-threshold/SOURCES.json new file mode 100644 index 0000000000..ed0a7d1f16 --- /dev/null +++ b/research/pauli-twisted-history-threshold/SOURCES.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ], + "external_references": [ + { + "role": "PR5446 general pointwise history theorem; proof inspected, no predecessor code executed", + "url": "https://github.com/Clear1nsight/integer-mult-bounds/blob/0d0bcf3fa261c9591e7e60ed5926c6e04d360f9e/docs/research/standalone-history-scalar-ceiling/proofs/pointwise-lemma-v1.md", + "commit": "0d0bcf3fa261c9591e7e60ed5926c6e04d360f9e", + "retrieved_utf8_sha256": "ac2a5a7c2e98b9dc3b19fbe0112003b37edf94dc13c0dc1411805cf52200c1e4" + }, + { + "role": "PR5450 smaller ordinary alphabet and explicit larger-group next question; proof inspected, no code imported", + "url": "https://github.com/aliromman/integer-mult-bounds/blob/616bf049b669d56a2bf21de130941f8de3f5d7bf/research/flip-history-sharp-width/README.md", + "commit": "616bf049b669d56a2bf21de130941f8de3f5d7bf", + "retrieved_utf8_sha256": "1b2c32ab9ec02e1d65342479d5265b03e440988cab986ae82e51a9e27a78617e" + } + ], + "external_reference_policy": "Immutable public proof citations, not executable/Git-history dependencies. Hashes identify retrieved UTF-8 text; no claim of a cold fetch or object-byte pin for these citations. The new proof and both verifiers are self-contained." +} diff --git a/research/pauli-twisted-history-threshold/TASK.json b/research/pauli-twisted-history-threshold/TASK.json new file mode 100644 index 0000000000..962282a96e --- /dev/null +++ b/research/pauli-twisted-history-threshold/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the sharp standalone paid-history threshold after enlarging the bit-flip ordinary group to G=, with exact even/odd phase treatment.", + "scope_change_reason": "Explicit PR5446/PR5450 released handoffs and parent assignment take precedence over the historical CRT card. This is a new quantified larger-alphabet implication, not a selected-frontier or #4100 audit.", + "bottleneck_link": "Side result: prevents transferring a smaller ordinary-alphabet lower bound without checking the actual phase-twisted algebra. No physical caller cost is inferred.", + "budget_minutes": 60, + "stop_rule": "Stop after the all-width theorem, exact finite cross-checks and meaningful history/phase controls; do not expand supplier or frontier scope.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; independently implemented check_modular.py; README.md reproduction and limits.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance in proof, exact implementation, adversarial checks and writing.", + "open_questions": [ + { + "question": "Does a named physical parent cut have only ordinary initial observations for these target owners?", + "why_it_matters": "The standalone q-return bound cannot be charged at a cached cut without its versioned observation module.", + "first_step": "Extract one actual caller cut with owner identities and all retained paid observations, then compute its projected history.", + "blocked_by": "No physical cut/source ledger is bound in this package." + }, + { + "question": "What is the sharp width for a target outside the two-term aI+bX family under the same full Pauli alphabet?", + "why_it_matters": "The proof uses two same-parity weight differences and does not classify arbitrary targets.", + "first_step": "Choose one explicitly source-bound invertible target, compute the even-character and odd-coset modules, and identify a uniform obstruction.", + "blocked_by": "A justified physical target and complete cost consequence, rather than another arbitrary parameter census." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5476", + "overlap": { + "base": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "open_prs": 342, + "discussion_records": 4736, + "discussion_fetched_at": "2026-10-25T03:48:26.071023+00:00", + "complete_pagination": true, + "limits": "Public cached bodies and explicit handoffs; unpublished work and all historical diffs not covered." + } +} diff --git a/research/pauli-twisted-history-threshold/VERIFY.json b/research/pauli-twisted-history-threshold/VERIFY.json new file mode 100644 index 0000000000..6f021d67b2 --- /dev/null +++ b/research/pauli-twisted-history-threshold/VERIFY.json @@ -0,0 +1,61 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact Gaussian-rational literal tensor, phase, owner-history and boundary controls with committed receipt" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact Gaussian-rational literal tensor, phase, owner-history and boundary controls with committed receipt; optimized explicit checks" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/check_modular.py" + ], + "timeout_seconds": 60, + "checks": "Independent modular arithmetic and bit-index tensor oracle, without primary-engine imports" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/check_modular.py" + ], + "timeout_seconds": 60, + "checks": "Independent modular arithmetic and bit-index tensor oracle, without primary-engine imports; optimized explicit checks" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_mutations.py" + ], + "timeout_seconds": 120, + "checks": "Six optimized semantic mutants must reject at named active predicates without comparing the stored receipt" + } + ] +} diff --git a/research/pauli-twisted-history-threshold/check_modular.py b/research/pauli-twisted-history-threshold/check_modular.py new file mode 100644 index 0000000000..835856af64 --- /dev/null +++ b/research/pauli-twisted-history-threshold/check_modular.py @@ -0,0 +1,103 @@ +#!/usr/bin/env python3 +"""Independent finite-field oracle: no Gaussian engine imports or Kronecker code. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +Finite fields exercise the same algebraic identities, not physical Q(i) inputs. +""" +import json + + +def require(ok, message): + if not ok: + raise RuntimeError(message) + + +def dimension(vectors, prime): + a = [list(row) for row in vectors] + pivot = 0 + for col in range(len(a[0])): + chosen = next((j for j in range(pivot, len(a)) if a[j][col] % prime), None) + if chosen is None: + continue + a[pivot], a[chosen] = a[chosen], a[pivot] + inv = pow(a[pivot][col] % prime, -1, prime) + a[pivot] = [x*inv % prime for x in a[pivot]] + for j in range(pivot+1, len(a)): + factor = a[j][col] % prime + a[j] = [(x-factor*y) % prime for x, y in zip(a[j], a[pivot])] + pivot += 1 + if pivot == len(a): + break + return pivot + + +def flatten(a): + return sum(a, []) + + +def product(a, b, prime): + n = len(a) + return [[sum(a[i][k]*b[k][j] for k in range(n)) % prime + for j in range(n)] for i in range(n)] + + +def run(): + cases, twists, projective, polynomial = 0, 0, 0, 0 + spectrum = {} + for prime in (5, 13): + for f in range(1, 5): + n, full = 2**f, 2**f-1 + # Direct computational-basis action of X^u Z^v; independent of + # the proof's X-eigenbasis and the primary Kronecker interpreter. + ordinary = [[[((-1)**(v*s.bit_count())) % prime + if r == s^(full if u else 0) else 0 + for s in range(n)] for r in range(n)] + for u, v in ((0, 0), (1, 0), (0, 1), (1, 1))] + ident, p, c, pc = ordinary + cp = product(c, p, prime) + require(pc == [[(-1)**f*x % prime for x in row] for row in cp], 'twist') + require(dimension([flatten(m) for m in ordinary], prime) == 4, 'image algebra') + twists += 1 + quarter = pow(4, -1, prime) + e = [[sum(g[r][s] for g in ordinary)*quarter % prime + for s in range(n)] for r in range(n)] + for a in range(1, prime): + for b in range(1, prime): + if (a*a-b*b) % prime == 0: + continue + # Each differing coordinate contributes b; each equal one a. + h = [[pow(a, f-(r^s).bit_count(), prime) * + pow(b, (r^s).bit_count(), prime) % prime + for s in range(n)] for r in range(n)] + targets = [product(g, h, prime) for g in ordinary] + union = dimension([flatten(m) for m in ordinary+targets], prime) + spectrum[str((prime, f, union))] = spectrum.get(str((prime, f, union)), 0)+1 + if f == 1: + require(union == 4, 'ordinary width one') + elif f % 2: + require(union == 8, 'odd separation') + else: + require(product(e, e, prime) == e, 'even projector') + require(dimension([flatten(e), flatten(product(e, h, prime))], prime) == 2, + 'even target character') + cases += 1 + lp, lm = (a+b) % prime, (a-b) % prime + for width in (2, 3, 7, 8, 31, 32): + left = (pow(lp, width, prime)-pow(lp, width-2, prime)*lm*lm) % prime + right = 4*a*b*pow(lp, width-2, prime) % prime + require(left == right and right != 0, 'nonzero weight difference') + polynomial += 1 + # Counterexample to using h outside G as the target criterion. + extra = [[2*x % prime for x in row] for row in p] + require(dimension([flatten(m) for m in ordinary+[extra]], prime) == 4, + 'ordinary scalar multiple') + projective += 1 + return {'status': 'PASS_INDEPENDENT_MODULAR_PAULI_HISTORY', + 'literal_tensor_cases': cases, 'phase_twists': twists, + 'projective_controls': projective, 'separation_identities': polynomial, + 'rank_spectrum': spectrum, + 'limits': 'finite-field identity controls; all-width Q(i) theorem is PROOF.md'} + + +if __name__ == '__main__': + print(json.dumps(run(), sort_keys=True, indent=2)) diff --git a/research/pauli-twisted-history-threshold/test_mutations.py b/research/pauli-twisted-history-threshold/test_mutations.py new file mode 100644 index 0000000000..1255f983d4 --- /dev/null +++ b/research/pauli-twisted-history-threshold/test_mutations.py @@ -0,0 +1,49 @@ +#!/usr/bin/env python3 +"""Prove the active checks reject semantic drift, without receipt comparison. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +from pathlib import Path +import subprocess +import sys +import tempfile + + +def main(): + source = Path(__file__).with_name('verify.py').read_text() + cases = [ + ('forget width-dependent global phase', + 'Q(0, 1)**(phase*f)', 'Q(0, 1)**phase', 'actual phase lift'), + ('make the odd algebra commute', + 'Q((-1)**f)', 'Q(1)', 'phase twist'), + ('reuse smaller-alphabet projector', + 'scale(Q(F(1, 4)), mul(add(ident, p), add(ident, c)))', + 'scale(Q(F(1, 2)), add(ident, p))', 'odd-width false character control'), + ('reverse the b coefficient in the literal target', + 'scale(b, x)), f)', 'scale(-b, x)), f)', 'Kronecker vs Hamming expansion'), + ('weaken the invertibility boundary', + 'bool(a*b*(a*a-b*b))', 'bool(a*b)', 'invalid target admitted'), + ('forget that one target was cached', + 'per*(q-1)', 'per*q', 'cached observation control'), + ] + receipts = [] + with tempfile.TemporaryDirectory(prefix='pauli-history-mutations-') as tmp: + for index, (name, old, new, expected) in enumerate(cases): + if source.count(old) != 1: + raise RuntimeError('ambiguous mutation anchor: '+name) + script = Path(tmp)/('case_'+str(index)+'.py') + script.write_text(source.replace(old, new)) + # --emit bypasses committed RESULT comparison: an active semantic + # check must reject the change, including under optimized Python. + run = subprocess.run([sys.executable, '-I', '-O', '-B', str(script), '--emit'], + capture_output=True, text=True, timeout=20) + if run.returncode == 0 or expected not in run.stderr: + raise RuntimeError('mutation escaped intended predicate: '+name+' '+run.stderr) + receipts.append({'mutation': name, 'rejection': expected}) + print(json.dumps({'status': 'PASS_PAULI_HISTORY_SEMANTIC_MUTATIONS', + 'optimized_semantic_rejections': receipts}, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/pauli-twisted-history-threshold/verify.py b/research/pauli-twisted-history-threshold/verify.py new file mode 100644 index 0000000000..7585eacd60 --- /dev/null +++ b/research/pauli-twisted-history-threshold/verify.py @@ -0,0 +1,268 @@ +#!/usr/bin/env python3 +"""Exact literal Pauli-history certificates; no imports from predecessor code. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from fractions import Fraction as F +import json +from pathlib import Path + + +class Q: + """Gaussian rationals, with exact arithmetic and no floating point.""" + __slots__ = ('a', 'b') + + def __init__(self, a=0, b=0): + if isinstance(a, Q): + self.a, self.b = a.a, a.b + else: + self.a, self.b = F(a), F(b) + + def __add__(self, other): + other = Q(other) + return Q(self.a + other.a, self.b + other.b) + + __radd__ = __add__ + + def __neg__(self): + return Q(-self.a, -self.b) + + def __sub__(self, other): + return self + -Q(other) + + def __mul__(self, other): + other = Q(other) + return Q(self.a*other.a-self.b*other.b, + self.a*other.b+self.b*other.a) + + __rmul__ = __mul__ + + def __truediv__(self, other): + other = Q(other) + d = other.a**2 + other.b**2 + if not d: + raise ZeroDivisionError('Gaussian zero denominator') + return self * Q(other.a/d, -other.b/d) + + def __pow__(self, exponent): + if not isinstance(exponent, int) or exponent < 0: + raise ValueError('nonnegative integer exponent required') + result, base = Q(1), self + while exponent: + if exponent & 1: + result = result * base + base = base * base + exponent //= 2 + return result + + def __bool__(self): + return bool(self.a or self.b) + + def __eq__(self, other): + other = Q(other) + return self.a == other.a and self.b == other.b + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def eye(n): + return [[Q(i == j) for j in range(n)] for i in range(n)] + + +def scale(c, a): + return [[c*x for x in row] for row in a] + + +def add(a, b): + return [[x+y for x, y in zip(ar, br)] for ar, br in zip(a, b)] + + +def mul(a, b): + out = [[Q() for _ in b[0]] for _ in a] + for i, row in enumerate(a): + for k, value in enumerate(row): + if value: + for j, other in enumerate(b[k]): + if other: + out[i][j] = out[i][j] + value*other + return out + + +def kron(a, b): + return [[x*y for x in ar for y in br] for ar in a for br in b] + + +def power(a, f): + out = [[Q(1)]] + for _ in range(f): + out = kron(out, a) + return out + + +def flat(a): + return [x for row in a for x in row] + + +def rank(rows): + basis = {} + for original in rows: + row = list(original) + for pivot, vector in sorted(basis.items()): + c = row[pivot] + if c: + row = [x-c*y for x, y in zip(row, vector)] + pivot = next((j for j, x in enumerate(row) if x), None) + if pivot is not None: + c = row[pivot] + basis[pivot] = [x/c for x in row] + return len(basis) + + +def span_rank(matrices): + return rank([flat(a) for a in matrices]) + + +def model(a, b, f): + need(isinstance(f, int) and not isinstance(f, bool) and f > 0, + 'positive integer width required') + need(bool(a*b*(a*a-b*b)), 'target must satisfy ab(a^2-b^2) != 0') + x = [[Q(0), Q(1)], [Q(1), Q(0)]] + z = [[Q(1), Q(0)], [Q(0), Q(-1)]] + p, c = power(x, f), power(z, f) + ordinary = [eye(2**f), p, c, mul(p, c)] + h = power(add(scale(a, eye(2)), scale(b, x)), f) + return ordinary, h + + +def owner_rows(matrices, owner, count): + width = len(flat(matrices[0])) + return [[Q()]*(owner*width) + flat(m) + + [Q()]*((count-owner-1)*width) for m in matrices] + + +def main_check(): + samples = [(Q(1), Q(2)), (Q(2), Q(1)), (Q(1), Q(0, 1)), + (Q(F(1, 2), F(1, 2)), Q(F(1, 2), F(-1, 2))), + (Q(0, 1), Q(2)), (Q(2, 1), Q(1, -1))] + rows, phase_cases, owner_cases = [], 0, 0 + for sample, (a, b) in enumerate(samples): + for f in range(1, 5): + ordinary, h = model(a, b, f) + ident, p, c, pc = ordinary + n = len(h) + need(span_rank(ordinary) == 4, 'ordinary dimension') + need(mul(p, c) == scale(Q((-1)**f), mul(c, p)), 'phase twist') + need(mul(p, p) == ident and mul(c, c) == ident, 'involutions') + # Independent coefficient expansion in the computational basis. + expanded = [[a**(f-(r^s).bit_count()) * b**((r^s).bit_count()) + for s in range(n)] for r in range(n)] + need(h == expanded, 'Kronecker vs Hamming expansion') + target = [mul(g, h) for g in ordinary] + combined = span_rank(ordinary + target) + need(span_rank(target) == 4, 'invertible target module') + if f == 1: + need(combined == 4, 'width-one ordinary target') + elif f % 2: + need(combined == 8, 'odd-width direct-sum separation') + e = scale(Q(F(1, 4)), mul(add(ident, p), add(ident, c))) + projected_rank = span_rank([mul(e, g) for g in ordinary]) + if f % 2 == 0: + need(mul(e, e) == e and projected_rank == 1, 'even character') + need(span_rank([e, mul(e, h)]) == 2, 'character detects target') + else: + need(mul(e, e) != e and projected_rank != 1, + 'odd-width false character control') + rows.append({'sample': sample, 'width': f, 'ordinary': 4, + 'ordinary_plus_target': combined, + 'candidate_character_dimension': projected_rank}) + + if sample == 3: + # All 16 actual group matrices, including width-dependent phases. + x = [[Q(), Q(1)], [Q(1), Q()]] + z = [[Q(1), Q()], [Q(), Q(-1)]] + for phase in range(4): + for u in range(2): + for v in range(2): + g = mul(x if u else eye(2), z if v else eye(2)) + literal = power(scale(Q(0, 1)**phase, g), f) + lifted = mul(p if u else ident, c if v else ident) + need(literal == scale(Q(0, 1)**(phase*f), lifted), + 'actual phase lift') + phase_cases += 1 + + if sample == 0 and f in (2, 3): + base = [e] if f == 2 else ordinary + targets = [mul(e, h)] if f == 2 else target + per = len(base) + for q in (1, 2, 3): + count = q+1 # An independent dirty coordinate remains present. + initial = sum((owner_rows(base, j, count) for j in range(count)), []) + goals = sum((owner_rows(targets, j, count) for j in range(q)), []) + need(rank(initial + goals) == per*(count+q), 'independent owners') + cached = owner_rows(targets, 0, count) + need(rank(initial + cached + goals)-rank(initial+cached) == per*(q-1), + 'cached observation control') + duplicate = owner_rows(targets, 0, count)*q + need(rank(initial+duplicate)-rank(initial) == per, + 'duplicate owner control') + owner_cases += 3 + + # The scalar separation identity is checked independently of tensor matrices. + scalar_cases = 0 + for a, b in samples: + lp, lm = a+b, a-b + for f in range(2, 33): + for k in (0, 1) if f >= 3 else (0,): + need(lp**(f-k)*lm**k-lp**(f-k-2)*lm**(k+2) == + Q(4)*a*b*lp**(f-k-2)*lm**k, 'weight separation identity') + scalar_cases += 1 + controls = 0 + for a, b in [(Q(), Q(1)), (Q(1), Q()), (Q(1), Q(1)), (Q(1), Q(-1))]: + try: + model(a, b, 3) + except ValueError: + controls += 1 + else: + raise ValueError('invalid target admitted') + for f in (0, -1, True): + try: + model(Q(1), Q(2), f) + except ValueError: + controls += 1 + else: + raise ValueError('invalid width admitted') + # Merely excluding actual G is insufficient: 2X is projectively ordinary. + for f in (1, 2, 3): + ordinary, _ = model(Q(1), Q(2), f) + need(span_rank(ordinary+[scale(Q(2)**f, ordinary[1])]) == 4, + 'projectively ordinary target control') + controls += 1 + # A single involution character does not stay scalar after adding Z. + for f in (2, 3, 4): + ordinary, _ = model(Q(1), Q(2), f) + small_e = scale(Q(F(1, 2)), add(ordinary[0], ordinary[1])) + need(span_rank([mul(small_e, g) for g in ordinary]) == 2, + 'smaller-alphabet projector must not be reused') + controls += 1 + return {'status': 'PASS_PAULI_TWISTED_HISTORY_THRESHOLD', + 'literal_cases': rows, 'actual_group_lifts': phase_cases, + 'owner_and_history_controls': owner_cases, + 'scalar_identity_cases': scalar_cases, 'boundary_controls': controls, + 'theorem': 'zero at width one; at least q at every width >=2', + 'upper_bound_condition': 'each requested H is an available paid primitive', + 'scope': 'finite checks corroborate PROOF.md; no physical caller admission'} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser() + parser.add_argument('--emit', action='store_true') + args = parser.parse_args() + result = main_check() + if not args.emit: + expected = json.loads(Path(__file__).with_name('RESULT.json').read_text()) + need(result == expected, 'committed certificate mismatch') + print(json.dumps(result, indent=2, sort_keys=True))