diff --git a/research/mixed-clifford-dyadic-imbalance/PROOF.md b/research/mixed-clifford-dyadic-imbalance/PROOF.md new file mode 100644 index 0000000000..2e6bf3bd1b --- /dev/null +++ b/research/mixed-clifford-dyadic-imbalance/PROOF.md @@ -0,0 +1,159 @@ +# Mixed Clifford lanes at widths congruent to two + +This contribution is produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Work over a characteristic-zero field containing i, where i^2=-1. Put + +``` +C = ((1+i) I + (1-i) X)/2, X = [[0,1],[1,0]], C_f = C tensor ... tensor C. +``` + +Fix f>0 with f=2 modulo 4, nonnegative integers a,b with q=a+b>0, +and delta=a-b. The independent payload operator is + +``` +T = (I_a tensor C_f) direct-sum (I_b tensor C_f^-1). +``` + +All q 2^f coordinates are arbitrary independent inputs. Identity complements +also hold arbitrary dirty data. Allow any invertible square encoder E and its +exact inverse as decoder. One candidate child has operator +H=lambda (C_h tensor I_t), with h,t positive integers and nonzero lambda. + +There is a full-space identity + +``` +T direct-sum I_d = E^-1 (H direct-sum I_e) E +``` + +if and only if d=e and there is an integer j>=0 such that + +``` +q = 2^j |delta|, 4^j divides q, +h = f+2j, t = q/4^j, +lambda = sign(delta) i^(-j). +``` + +In particular, delta cannot be zero. These conditions determine the candidate +uniquely. They classify a forward child; allowing an inverse child adds no +widths because C_h^-1 is similar to (-i)^h C_h, as in Arham Tahir's PR1920. +The theorem does not classify other congruence classes of f. + +## Necessity + +The source facts used here are PR1920's reciprocal full-space contract, +Walsh eigenbasis and trace method. Their application to arbitrary directional +multiplicities, and the resulting integer conditions, are the new step. + +Since C has eigenvalues 1,i, all payload eigenvalues are fourth roots of +unity. Taking fourth powers of the identity forces lambda^4=1 on the +nonempty child operand. Therefore lambda belongs to {1,i,-1,-i}. +The traces of C_f^2 and C_h^2 are zero, since they are positive tensor powers +of the traceless X. The square traces of the two full operators are d and e, +so d=e. Dimension equality then gives + +``` +q 2^f = t 2^h. (1) +``` + +Write z=(1+i)^f. Since f=2 modulo 4, its Gaussian conjugate is -z. After +subtracting the equal complement traces, the first trace identity becomes + +``` +delta z = t lambda (1+i)^h. (2) +``` + +The right side is nonzero, so delta is nonzero. Taking the algebraic Gaussian +norm of this equality gives + +``` +delta^2 2^f = t^2 2^h. +``` + +Combine this with (1) to obtain q^2/delta^2=2^(h-f). Because |delta|<=q, +h>=f. A rational square that is a power of two has an even exponent, by +the exponent of the prime 2 in its numerator and denominator. Thus h-f=2j +for an integer j>=0, and q=2^j |delta|. Equation (1) now gives t=q/4^j; +its required positive integrality is exactly 4^j dividing q. Finally, +(1+i)^(f+2j)=z (2i)^j in (2) gives the asserted lambda, including its sign. + +No positivity, ordering or analytic norm on the ambient field was used. +The norm calculation is in its embedded copy of Q(i). + +## Sufficiency and explicit basis + +Assume the displayed integer conditions. The dimensions agree. Substitution +shows the first traces agree, since + +``` +(q/4^j) sign(delta) i^(-j) z (2i)^j = delta z. +``` + +The square traces vanish. The third traces are the Gaussian conjugates of +the first traces, so they agree as well. The zeroth traces are dimensions. +The four-point Fourier matrix recovers eigenvalue multiplicities from these +four traces. Since x^4-1 has distinct roots in characteristic zero, both +operators are diagonalizable and equal multiplicities suffice for similarity. + +This is constructive with rational dyadic matrices. Let +W_f[x,y]=(-1)^popcount(x&y). Its column y has C_f eigenvalue +i^popcount(y), and W_f^-1=2^-f W_f^T. Let U be the direct sum of q copies +of W_f, retaining the inverse direction in the eigenvalue list for the last +b copies. Let V be W_h tensor I_t, with columns reordered to match U's +eigenvalues after multiplication by lambda. Equal multiplicities guarantee +this matching. Then + +``` +E = V U^T / 2^f, E^-1 = U V^T / 2^h, +H E = E T. +``` + +Both products of the unscaled encoding and decoding numerators equal +2^(f+h) I. Extend E by I_d to retain any dirty complement. Thus the identity +holds for every input column, including arbitrary independent dirty data. +This construction does not require that E itself be a native operation. + +## First new identity and sharp minimum batch + +Taking f=2, a=3, b=1 gives q=4, delta=2 and j=1. Therefore + +``` +C_2 direct-sum C_2 direct-sum C_2 direct-sum C_2^-1 + = E^-1 (-i C_4) E. +``` + +This is a 16-coordinate identity. PR1920's balanced opposite pair has zero +first trace at f=2 and cannot do this. Any proper width upgrade in the +present model has j>=1 and hence q>=4^j>=4. The four-lane batch is minimal. +More generally the conditions give a minimum q=4^j for a width increase 2j, +attained by a=(4^j+2^j)/2 and b=(4^j-2^j)/2 for every j>=1. +This minimum is an algebraic batch size, not an operation-cost claim. + +## Cost and applicability limit + +Under the inherited PR679 expression A V f^sigma per full lane, with +A,V>0 and 00 its ratio is (1+2j/f)^sigma>1. This is a comparison of available +upper expressions, not a lower bound on optimal runtime. The identity +does not establish the card's favorable complete-invoice gate. + +The congruence condition applies to the literal tensor width f. An operation +whose literal width varies with a column parameter would need an implementation +for every required width. This package supplies no such uniform supplier, +native encoding, physical placement, scalar-read tariff, precision/tape proof, +restoration schedule for the encoder, new kappa or multiplication theorem. +Independent human and formal proof-kernel review are unclaimed. + +## Proof versus finite corroboration + +The preceding argument proves the quantified statement. The standalone +verifier independently compares its integer classification with literal +binomial eigenspace counts, and constructs four dense rational encoders. +It checks both inverse orders and every coefficient of H E=E T using +Gaussian integer tensor coefficients, including identity complements. +Those finite checks corroborate the proof; they are not extrapolated to +unbounded widths or converted into physical costs. diff --git a/research/mixed-clifford-dyadic-imbalance/README.md b/research/mixed-clifford-dyadic-imbalance/README.md new file mode 100644 index 0000000000..08eaaf11db --- /dev/null +++ b/research/mixed-clifford-dyadic-imbalance/README.md @@ -0,0 +1,140 @@ +# Exact directional imbalance for mixed Clifford lanes + +This contribution is produced by Nick Petalas. Apache-2.0. + +Scoped algebraic proof with finite corroboration. For literal tensor widths +f=2 modulo 4, an unbalanced collection of forward and inverse Clifford lanes +can sometimes be one wider child under an arbitrary reciprocal linear +encoding. The first new identity uses three forward width-two lanes and one +inverse lane on 16 coordinates: + +``` +C_2 direct-sum C_2 direct-sum C_2 direct-sum C_2^-1 = E^-1 (-i C_4) E. +``` + +Four lanes are necessary and sufficient for a proper width upgrade in this +model. This differs from Arham Tahir's PR1920 balanced-pair result, which +excludes an opposite width-two pair. The spectral and Walsh methods are +inherited; the arbitrary directional multiplicities and exact integer +classification are the new contribution. No literature priority is claimed +for elementary spectral similarity or prime valuations. + +## Exact classification + +Let a,b be the forward/inverse counts, q=a+b>0, and delta=a-b. With the +convention C=((1+i)I+(1-i)X)/2 and C_f=C tensor ... tensor C, a single +forward child lambda (C_h tensor I_t) is similar to the independent lanes +exactly when, for an integer j>=0, + +``` +q = 2^j |delta|, 4^j divides q, +h = f+2j, t = q/4^j, +lambda = sign(delta) i^(-j). +``` + +In particular a=b never works at these widths. The smallest batch for an +increase 2j is q=4^j. All payload coordinates are independent arbitrary +inputs. Arbitrary restored dirty complements can be mixed by the encoder; +they cannot increase the active child volume. [PROOF.md](PROOF.md) gives +necessity, sufficiency, explicit rational dyadic encoding/decoding, the exact +complement statement and the inherited volume-cost limitation. + +This is an algebraic interface identity. The joined child loses the inherited +PR679 full-volume upper expression even with free adapters. Physical/native +encoding, frame conversion, reads, storage, routing, precision, restoration +and every complete consumer cost remain unpaid. Widths in other congruence +classes and a uniform implementation at every column multiplicity are outside +this theorem. No supplier admission, new kappa or multiplication theorem is +claimed. Independent human and formal proof-kernel review are unclaimed. + +## Reproduce + +From the repository root, using the standard library and CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mixed-clifford-dyadic-imbalance +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/mixed-clifford-dyadic-imbalance/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/mixed-clifford-dyadic-imbalance/verify.py +``` + +The interpreter path is local; reviewers elsewhere can substitute their +CPython 3.12 executable. The verifier is read-only and also works in a +Git-free package export. Its JSON receipt is generated, includes file SHA256 +hashes, and is printed to stdout. No saved receipt is a proof input. + +The finite sweep enumerates every a,b with 1<=a+b<=64 at widths +f=2,6,...,30. It checks 17,152 target multiplicity lists against 1,170,400 +dimension-compatible phased candidates. There are 1,360 matches, of which +336 are proper width upgrades. The uniform boundary cases are controls, +not predecessor results claimed anew. A separate cyclic recurrence checks +all 37 binomial spectrum lists used in the sweep. + +Four dense rational witnesses cover both imbalance signs, a nontrivial +spectator factor, a four-width increase, and arbitrary dirty identity +complements. They check 5,870 entries of H E=E T, plus both inverse products +for every fixture. Exact Gaussian tensor coefficients are constructed +separately from the Walsh eigenbasis. Controls reject a wrong phase, +direction, encoder, dirty output, balanced batch, nondyadic imbalance and +nonintegral spectator count, plus four invalid domains. All checks remain +enabled under optimized Python. + +The written proof establishes the quantified result. Finite enumeration +alone is not an unbounded proof. No predecessor verifier, selected cold +replay, native implementation, Lean or Docker build is run for this result. + +## Scope and overlap + +Base canonical main is `624de9dc66858af0945e5f8a0942488d62280d43`, priority +revision 7. [The advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133741) +states the delivered target. [TASK.json](TASK.json) records the changed scope +from physical synthesis to an exact prerequisite classification and the +bounded stop rule. The current selected source-binding orientation passed. +The card's historical ceiling command failed with `KeyError: complex_profile` +against the changed selected schema; it supplies no evidence here. + +Overlap checks read current open PRs, this account's recent work, recent +handoffs, active Discussions, targeted merged PRs and distinctive terms in +all main READMEs. The cached search covers 379 open PRs and 3,853 Discussion +records, but only 101 of 6,319 local-main notes were materialized. This does +not cover unpublished work or every code diff. Exact predecessor READMEs are +historical provenance in [SOURCES.json](SOURCES.json); no predecessor code is +imported or copied. The standalone verifier has no external proof input. + +The implementation has no recursion or background work. The entrypoint fixes +every finite enumeration range; dense matrices have at most 67 rows and +columns. Python allocates integers and collections dynamically, a managed +runtime deviation from fixed allocation. Live matrices are bounded by those +fixture caps. Functions stay below 60 physical lines. Warning-strict normal +and optimized execution are the registered diagnostics; no static type or +native-code analysis is claimed. + +## Credit + +Arham Tahir, PR1920, supplied the reciprocal full-space contract, equal-width +uniform and balanced-pair results, trace invariants and Walsh construction. +Adam Gall, PR1946, classified two unequal-width equal-volume lanes, a +different multiplicity contract. The exact correction-rank work by ywz65 +concerns an additional nonreciprocal adapter, which this theorem does not +allow. Greer Guthrie, PR679, and Ross Richardson's diagonal-child contract +audit supplied the inherited volume-aware scope and tariff. ToikY, PR1924, +and Douglas Colkitt, PR665, supplied distinct clean-injection/spectral +interfaces. Jose Manuel/jmbarrancoml with Cinna Davis/1337isnot1337, PR1779, +and Josie Elliston, PR1817, supplied the batching motivation and retiming +context. Credit icekylinx, DreamingOfClouds, Rohan Arun, Jeremy Kothe, +Hao Yan and the retained native-kernel/construction lineage. Their original +credit and source files remain unchanged. + +## Open next questions + +- Can a real three-forward/one-inverse width-two caller support a different, + favorable fully paid operation or volume contract? First name its actual + charts, inputs, outputs and complete adapter ledger. No such physical + caller or cheaper tariff is supplied here. +- Can a uniform supplier exploit this exception while supporting every + required literal width? First pin one caller's column parameter, derive + its admissible congruences, and price a legal fallback. An actual caller + and all-size cost contract remain missing. + +The structured questions in TASK.json give their relevance, first steps and +blockers. Further reciprocal basis searches under the same losing tariff +are not justified by this algebraic identity. diff --git a/research/mixed-clifford-dyadic-imbalance/SOURCES.json b/research/mixed-clifford-dyadic-imbalance/SOURCES.json new file mode 100644 index 0000000000..02effeadff --- /dev/null +++ b/research/mixed-clifford-dyadic-imbalance/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/clifford-reciprocal-basis-obstruction/README.md", + "usage": "provenance", + "git_blob": "6aff66509d3748445d33847e90a0abbafca14263", + "sha256": "ecef2b644bfb28083d9220f56aed2903c778c96851d5c6daa749bd974bbbdf24" + }, + { + "path": "research/complex-heterogeneous-child-interface/README.md", + "usage": "provenance", + "git_blob": "72f125c320ee6f0ccfeff4c6373d1b5081361e2e", + "sha256": "de40ae7874788a3f4875d41e9a294c3a1a78f4fec1f1f0b7677e60cdd5eed670" + }, + { + "path": "research/clifford-sharp-correction-rank/README.md", + "usage": "provenance", + "git_blob": "457263eece572398f3ddadd87793d0a189413f93", + "sha256": "767b6d8c72561026cf6dea31db5d5ef86dfb7b35c33d66fe4366b71ae744bfe3" + } + ] +} diff --git a/research/mixed-clifford-dyadic-imbalance/TASK.json b/research/mixed-clifford-dyadic-imbalance/TASK.json new file mode 100644 index 0000000000..6eb61a72d3 --- /dev/null +++ b/research/mixed-clifford-dyadic-imbalance/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "complex-rank-shape-decoder", + "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/complex-decoder-field-extension-seed44/README.md", + "research/complex-frame-pair-decoders/README.md", + "research/selected-k8-unrestricted-ends/README.md", + "research/eisenstein-reduction-copy-floor/README.md" + ], + "methods": [ + "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.", + "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration." + ], + "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).", + "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.", + "allowed_variations": [ + "One masked, overcomplete or block decoder family with exact labels and supports.", + "A scoped lower bound on effective rank for one alphabet.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Repacking idle remainders of an unchanged word (covered by the packing ceiling).", + "Repeating the eight-term all-pairs search inside its proved scope.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "rank shape", + "block climb", + "masked decoder", + "overcomplete", + "effective rank" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact arbitrary-multiplicity reciprocal Clifford classification for literal widths f congruent to 2 modulo 4.", + "scope_change_reason": "Replace physical decoder synthesis by a self-contained algebraic prerequisite classification extending Arham Tahir PR1920. No favorable full-invoice or 5% gate is claimed.", + "bottleneck_link": "A larger-rank child needs an actual all-input interface identity. This classifies a directional-mixing exception and its minimum batch, but the inherited joined-volume expression still loses.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved new mixed-lane identity and exact integer criterion; do not extend the mechanism or optimize a supplier.", + "outcome": "completed", + "evidence": "PROOF.md supplies the quantified proof. verify.py independently enumerates spectra and constructs four exact rational intertwiners with both inverse orders and semantic rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a physically legal boundary implement a 3:1 mixed batch under a different fully paid volume or operation contract?", + "why_it_matters": "The inherited full-volume upper expression loses even with free encoding; the algebraic identity alone cannot improve a supplier.", + "first_step": "Identify one real simultaneous three-forward/one-inverse width-two caller, its input/output charts, and a legal complete encoding, decoding and movement ledger.", + "blocked_by": "No such caller or improved physical cost contract is supplied." + }, + { + "question": "Can a uniform supplier exploit the exception while supporting every required literal width?", + "why_it_matters": "The present theorem assumes f congruent to 2 modulo 4 and does not cover all column multiplicities.", + "first_step": "Name one caller width parameter and derive its exact admissible congruences and fallback invoice before constructing code.", + "blocked_by": "An actual caller and complete all-size cost contract are absent." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133741", + "overlap_coverage": "Live first 100 open PRs and last 60 account PRs; 35 latest handoff comments plus active Discussions and preclaim refresh; cached 379 open PRs and 3853 Discussion records, complete pagination; sparse 101 local notes of 6319 main notes. Distinctive git grep on all main READMEs and targeted merged PR searches included PR1920, PR1924, PR1946 and sharp-correction work. Unpublished work and arbitrary code diffs are not fully covered.", + "first_working_example": "Current selected source-binding baseline passed. Historical complex-local-word-ceiling control failed with KeyError complex_profile; it was not repaired or treated as evidence." + } +} diff --git a/research/mixed-clifford-dyadic-imbalance/VERIFY.json b/research/mixed-clifford-dyadic-imbalance/VERIFY.json new file mode 100644 index 0000000000..7dad6b3a37 --- /dev/null +++ b/research/mixed-clifford-dyadic-imbalance/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact mixed-lane integer classification versus binomial spectra; four full rational operator identities and both inverse orders; semantic and domain rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the exact checks with optimization enabled; every check uses explicit exceptions." + } + ] +} diff --git a/research/mixed-clifford-dyadic-imbalance/verify.py b/research/mixed-clifford-dyadic-imbalance/verify.py new file mode 100644 index 0000000000..7b70427935 --- /dev/null +++ b/research/mixed-clifford-dyadic-imbalance/verify.py @@ -0,0 +1,233 @@ +"""Exact, read-only corroboration of the mixed-lane theorem. Standard library.""" + +import hashlib +import json +from math import comb +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def classification(width, forward, inverse): + """Return (child width, spectator multiplicity, phase exponent), or None.""" + require(all(type(x) is int for x in (width, forward, inverse)), "integers required") + require(width > 0 and width % 4 == 2, "width must be 2 modulo 4") + require(min(forward, inverse) >= 0 and forward + inverse > 0, "invalid lanes") + total, imbalance = forward + inverse, forward - inverse + for step in range(total.bit_length()): + scale = 1 << step + if abs(imbalance) * scale == total and total % (scale * scale) == 0: + phase = ((0 if imbalance > 0 else 2) - step) % 4 + return width + 2 * step, total // (scale * scale), phase + return None + + +def spectrum(width): + return tuple(sum(comb(width, k) for k in range(r, width + 1, 4)) for r in range(4)) + + +def spectral_sweep(): + """Compare the theorem with literal binomial eigenspace capacities.""" + spectra = [spectrum(w) for w in range(37)] + recurrence = (1, 0, 0, 0) + for width in range(37): + require(spectra[width] == recurrence, "independent spectrum recurrence") + recurrence = tuple(recurrence[r] + recurrence[(r - 1) % 4] for r in range(4)) + targets = candidates = matches = upgrades = 0 + for width in range(2, 31, 4): + base = spectra[width] + for total in range(1, 65): + dimension = total << width + for forward in range(total + 1): + inverse = total - forward + target = tuple(forward * base[r] + inverse * base[-r % 4] for r in range(4)) + actual = [] + for child in range(1, width + total.bit_length()): + if dimension % (1 << child): + continue + spectator = dimension >> child + for phase in range(4): + candidates += 1 + trial = tuple(spectator * spectra[child][(r - phase) % 4] for r in range(4)) + if target == trial: + actual.append((child, spectator, phase)) + predicted = classification(width, forward, inverse) + require(actual == ([] if predicted is None else [predicted]), "classification mismatch") + targets += 1 + matches += len(actual) + upgrades += int(predicted is not None and predicted[0] > width) + return {"targets": targets, "phase_candidates": candidates, "matches": matches, + "proper_width_upgrades": upgrades} + + +def gaussian_product(left, right): + a, b = left + c, d = right + return a * c - b * d, a * d + b * c + + +def gaussian_power(value, exponent): + result = (1, 0) + for _ in range(exponent): + result = gaussian_product(result, value) + return result + + +def kernel_numerator(width, inverse=False): + """Tensor coefficients, with common denominator 2**width.""" + values = [] + for distance in range(width + 1): + value = gaussian_product(gaussian_power((1, 1), width - distance), + gaussian_power((1, -1), distance)) + values.append((value[0], -value[1]) if inverse else value) + return values + + +def integer_product(left, right): + columns = tuple(zip(*right)) + return [[sum(a * b for a, b in zip(row, col)) for col in columns] for row in left] + + +def complex_left(left, right): + columns = tuple(zip(*right)) + return [[(sum(a[0] * b for a, b in zip(row, col)), + sum(a[1] * b for a, b in zip(row, col))) for col in columns] for row in left] + + +def complex_right(left, right): + columns = tuple(zip(*right)) + return [[(sum(a * b[0] for a, b in zip(row, col)), + sum(a * b[1] for a, b in zip(row, col))) for col in columns] for row in left] + + +def fixture(width, forward, inverse, padding): + choice = classification(width, forward, inverse) + require(choice is not None, "fixture has no solution") + child, spectator, phase = choice + lane_size, total = 1 << width, forward + inverse + active = lane_size * total + require(active <= 64 and 0 <= padding <= 3, "dense fixture capacity") + size = active + padding + target_eigen = [(lane, a, ((1 if lane < forward else -1) * a.bit_count()) % 4) + for lane in range(total) for a in range(lane_size)] + buckets = [[(a, s) for a in range(1 << child) for s in range(spectator) + if (phase + a.bit_count()) % 4 == r] for r in range(4)] + used = [0] * 4 + matched = [] + for _, _, eigen in target_eigen: + require(used[eigen] < len(buckets[eigen]), "eigenspace exhausted") + matched.append(buckets[eigen][used[eigen]]) + used[eigen] += 1 + require(used == list(map(len, buckets)), "unmatched eigenspace") + u = [[int(x // lane_size == lane) * (-1 if (x % lane_size & a).bit_count() % 2 else 1) + for lane, a, _ in target_eigen] for x in range(active)] + v = [[int(x % spectator == s) * (-1 if (x // spectator & a).bit_count() % 2 else 1) + for a, s in matched] for x in range(active)] + encoding = integer_product(v, list(zip(*u))) + decoding = integer_product(u, list(zip(*v))) + for matrix, denominator in ((encoding, 1 << width), (decoding, 1 << child)): + for row in matrix: + row.extend([0] * padding) + matrix.extend([[denominator * int(x == y) for y in range(size)] + for x in range(active, size)]) + return choice, encoding, decoding + + +def operators(width, forward, inverse, padding, choice): + child, spectator, phase = choice + lane_size = 1 << width + active = (forward + inverse) * lane_size + size = active + padding + kernels = (kernel_numerator(width), kernel_numerator(width, True)) + child_kernel = kernel_numerator(child) + unit = ((1, 0), (0, 1), (-1, 0), (0, -1))[phase] + target = [[(0, 0) for _ in range(size)] for _ in range(size)] + host = [[(0, 0) for _ in range(size)] for _ in range(size)] + for x in range(active): + for y in range(active): + if x // lane_size == y // lane_size: + target[x][y] = kernels[int(x // lane_size >= forward)][((x ^ y) % lane_size).bit_count()] + if x % spectator == y % spectator: + host[x][y] = gaussian_product(unit, child_kernel[((x // spectator) ^ (y // spectator)).bit_count()]) + for x in range(active, size): + target[x][x], host[x][x] = (1 << width, 0), (1 << child, 0) + return target, host + + +def intertwines(width, child, encoding, target, host): + size = len(encoding) + require(size > 0 and all(len(matrix) == size and all(len(row) == size for row in matrix) + for matrix in (encoding, target, host)), "square operator dimensions") + left = complex_left(host, encoding) + right = complex_right(encoding, target) + return all(a * (1 << width) == b * (1 << child) + for row_l, row_r in zip(left, right) + for pair_l, pair_r in zip(row_l, row_r) for a, b in zip(pair_l, pair_r)) + + +def dense_checks(): + results = [] + first = None + for width, forward, inverse, padding in ((2, 3, 1, 3), (2, 1, 3, 2), (2, 6, 2, 1), (2, 10, 6, 0)): + choice, encoding, decoding = fixture(width, forward, inverse, padding) + child, _, _ = choice + size = len(encoding) + target, host = operators(width, forward, inverse, padding, choice) + expected = [[(1 << (width + child)) * int(x == y) for y in range(size)] for x in range(size)] + require(integer_product(encoding, decoding) == expected, "right inverse") + require(integer_product(decoding, encoding) == expected, "left inverse") + require(intertwines(width, child, encoding, target, host), "full operator identity") + digest = hashlib.sha256(json.dumps([encoding, decoding], separators=(",", ":")).encode()).hexdigest() + results.append({"width": width, "forward": forward, "inverse": inverse, "padding": padding, + "child": list(choice), "matrix_entries": size * size, "basis_sha256": digest}) + if first is None: + first = encoding, target, host, choice + require(first is not None, "missing control fixture") + return results, first + + +def controls(first): + encoding, target, host, choice = first + child, spectator, phase = choice + wrong_phase = (child, spectator, (phase + 1) % 4) + _, bad_host = operators(2, 3, 1, 3, wrong_phase) + require(not intertwines(2, child, encoding, target, bad_host), "phase control") + wrong_target, _ = operators(2, 4, 0, 3, choice) + require(not intertwines(2, child, encoding, wrong_target, host), "direction control") + broken = [row[:] for row in encoding] + broken[0][0] += 1 + require(not intertwines(2, child, broken, target, host), "encoder control") + dirty_target = [row[:] for row in target] + dirty_target[-1][-1] = (0, 0) + require(not intertwines(2, child, encoding, dirty_target, host), "dirty restoration control") + require(classification(2, 1, 1) is None, "balanced control") + require(classification(2, 4, 2) is None, "nondyadic imbalance control") + require(classification(2, 3, 1) == (4, 1, 3), "first positive") + require(classification(2, 9, 7) is None, "spectator integrality control") + for args in ((True, 3, 1), (2, -1, 2), (2, 0, 0), (4, 3, 1)): + try: + classification(*args) + except ValueError: + continue + raise ValueError("invalid domain accepted") + return ["phase", "direction", "encoder", "dirty restoration", "balanced", + "nondyadic imbalance", "spectator integrality", "four invalid-domain cases"] + + +def main(): + sweep = spectral_sweep() + dense, first = dense_checks() + rejected = controls(first) + package = Path(__file__).resolve().parent + files = sorted(p for p in package.iterdir() if p.is_file()) + receipt = {"status": "PASS_MIXED_CLIFFORD_IMBALANCE", "claim_type": "scoped proof", + "spectral_sweep": sweep, "dense_fixtures": dense, "controls": rejected, + "sha256": {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in files}} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()