diff --git a/research/quotient-kernel-family/README.md b/research/quotient-kernel-family/README.md new file mode 100644 index 0000000000..dd1908db33 --- /dev/null +++ b/research/quotient-kernel-family/README.md @@ -0,0 +1,139 @@ +# Admissible quotient kernels of the #4596 word + +**Claim type: finite certificate with a scoped proof.** No κ is claimed. The +result is conditional on the open pull request #4596 and on the endpoint +question raised in #4604 (see [Conditions](#conditions)). + +DaysSky's open #4596 quotients the nine-axis ambient of the PR4470 complex word +by `span{511}`, re-pads one helper so the word still spans nine axes, and +reports a complex supplier saving of 0.012091850234. Its `PROOF.md` leaves +open "Whether `511` is the unique removable direction". This package answers that +question for the check #4596 itself ships. + +## Result + +Over all 511 nonzero directions `v` of F₂⁹, build the #4596 quotient word for +`span{v}` and replay it with the shipped literal replay +(`native_extensions.literal_replay` with the `verify_buffers.expected` +endpoint table, both orientations, owned C cleared). + +1. **Exactly 32 directions are accepted.** The other 479 all fail the same + shipped check, "Paid rank and source frame". +2. **The accepted set has an exact description.** The base word has eight centre + transports, each between the ground frame and a dim-8 frame, charged rank 8. + Those eight frames are hyperplanes of F₂⁹ with normals + {7, 25, 42, 52, 76, 82, 97, 127}, of GF(2) rank 4. A direction is accepted + exactly when it lies outside all eight hyperplanes, that is + `{v : λᵢ(v) = 1 for all i}`. This is a coset of a 5-dimensional subspace, so + it has 2⁵ = 32 points, and it does not contain 0. The normals use only bits + 0–6, and each normal is itself outside all eight hyperplanes, so the set is + `{h + 128i + 256j : h a normal, i, j ∈ {0, 1}}`. +3. **511 is not the best direction.** The best is `v = 153`: + + | Kernel | Main widths | Paid rank mass | Local deficit | Rank surplus | Complex saving | + |---|---|---|---|---|---| + | 511 (#4596) | {7: 112, 8: 112} | 4834 | 1744 | 2768 | 0.012091850234 | + | 153 | {7: 168, 8: 56} | 4778 | 1688 | 3776 | 0.016567169219 | + + The next two are 338 (0.016555611423) and 180 (0.016552449914), both with + deficit 1688 and surplus 3776. Twenty-four accepted directions, 153 and 511 + among them, keep the helper profile {3: 2, 4: 26, 6: 7, 7: 47, 8: 325, 9: 1}; + the other eight (7, 52, 82, 97, 391, 436, 466, 481) widen both rank-3 + helpers to rank 4. The saving is #4596's invoice and dual-moment screen + applied unchanged. +4. **No kernel of dimension 2 or more is accepted.** A 2-dimensional kernel + needs three nonzero vectors outside every centre hyperplane. The accepted + set is a coset that does not contain 0, so the sum of two accepted + directions lies in the difference subspace, which meets the coset nowhere. + The verifier checks this over all pairs. +5. **Under the stronger geometric condition, 511 is unique.** Require that + every dim-8 main final keeps dimension 8 under the quotient, that is, that + `v` lies outside all of them. The 112 distinct dim-8 main finals have + normals of full rank 9, and the only direction outside all of them is 511. + This is the condition #4596's construction meets; the shipped replay does + not check it. + +So the answer to #4596's question depends on the condition. 511 is the unique +direction that keeps every dim-8 main final at dimension 8, but 32 directions +pass the shipped replay, and 153 prices 37% higher on the complex side. + +## What this does not change + +The outer κ in #4596 is limited by the BIT side (0.0034), not by the complex +supplier. A larger complex saving does not move it until the BIT admission +chain moves. This package claims no κ. + +## Conditions + +- **#4596 is open.** The quotient construction, the helper re-padding and the + invoice are #4596's. This package re-uses them unchanged; if #4596 is not + accepted, this classification describes an unaccepted construction. +- **#4604's endpoint question applies here too.** pinterbanget's open #4604 + shows that under the 511 quotient every main output frame changes, and that + the shipped replay compares final frames with the word's own record, not + with required output charts. The 32 accepted directions pass that same + replay, so they inherit the same question. If output charts are part of the + supplier contract, none of the 32 quotient words, including 511, meets it. +- **The 479 rejections come from one hard-coded rank.** `synthesize` charges + every centre transport rank 8. A quotient is accepted only if each centre + frame keeps dimension 8, which is the hyperplane condition in item 2. A + pipeline that recomputed centre ranks would accept a different set; that + variant is not studied here. + +## Reproduce + +From the repository root, with CPython 3.12: + +```sh +python3.12 -W error -B research/quotient-kernel-family/verify.py # about 30 s +python3.12 -W error -B research/quotient-kernel-family/verify.py --scan 1 255 # about 100 s +python3.12 -W error -B research/quotient-kernel-family/verify.py --scan 256 511 # about 100 s +python3.12 -W error -B research/quotient-kernel-family/verify.py --physical 153 # exact lowering +python3.12 -W error -B research/quotient-kernel-family/verify.py --physical 511 +``` + +The default run checks items 2 to 5: it derives the eight centre hyperplanes +from the base word, checks the normals, rank, coset and pair conditions, checks +the 112 main-final hyperplanes, replays all 32 predicted directions, checks the +declared profiles for 153 and 511 and the two helper profiles, and replays +four rejected controls. The two `--scan` shards replay every +direction and require the shipped replay to accept exactly the predicted set +(item 1). `--physical` lowers every realised transport of one quotient word +exactly and requires Fourier rank equal to the absolute dimension difference, +the convention of the shipped evaluators (`native_extensions.py` line 127, +`verify_buffers.py` line 151). + +`quotient.py` builds the base word from the pinned main packages and the +quotient words; it writes no files. + +## Limitations + +- Finite certificate over one word. The base word is fixed; other words or + other quotient maps are not covered. +- The complex saving is computed with #4596's float bisection of the dual + screen. A directed-rounding recomputation during development agreed to + 2·10⁻¹⁷ for 153 and 7·10⁻¹⁷ for 511; that recomputation is not shipped. +- Physical lowering was checked for 153 and 511 only, not for the other 30 + accepted directions. +- No formal proof, no Lean, no selected-construction replay. + +## Open next questions + +- Does an operator-level endpoint check (#4604's open question) accept any of + the 32 quotient words, or does it reduce the admissible set to the empty set? +- If centre ranks are recomputed instead of hard-coded, which kernels pass, and + is any of them better than 153? +- Does a different base word have a centre-hyperplane family of lower rank, + and so a larger admissible coset? +- Does #4596's controller strictification hold when its controller targets come + from a quotient word? An unverified local substitution gave a negative margin + on the delta row for all 32 directions, 511 included. This needs an + independent check before any outer κ is claimed for the family. + +## Credit + +This package was produced by Nick Petalas. The quotient construction, helper +re-padding and invoice are DaysSky's (#4596). The base word is Cinna Davis's: query thinning +and helper retiming (#4441), the missing join frame (#4447) and joint helper +boundaries (#4470), on zxv's native supplier. The endpoint-contract question +is pinterbanget's (#4604). diff --git a/research/quotient-kernel-family/SOURCES.json b/research/quotient-kernel-family/SOURCES.json new file mode 100644 index 0000000000..94bd91e039 --- /dev/null +++ b/research/quotient-kernel-family/SOURCES.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/fresh-helper-boundary/CHANGES.json", + "usage": "input", + "git_blob": "45744fedd0e28967aa72586048b8bc0c72f419a9", + "sha256": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624" + }, + { + "path": "research/fresh-helper-boundary/native.py", + "usage": "input", + "git_blob": "1b36f6cb5f205c33bf48811e0b1b3621c55e8154", + "sha256": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29" + }, + { + "path": "research/joint-helper-lattice/PATCH.json", + "usage": "input", + "git_blob": "51304a6601061ed4e698f910b09135ef109555e3", + "sha256": "296d0e8c58cc70febe042c681ef30d6bb469818c0835fbcaac8aa8d330f5b727" + }, + { + "path": "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "usage": "input", + "git_blob": "5a55034ec9e6185d981e16c28e1e2e455069e2cb", + "sha256": "106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7" + }, + { + "path": "research/kappa-function-composition/complex/prune_native.py", + "usage": "input", + "git_blob": "8c3e11b2408fa96eefa3ebe7952d1b11b90b772b", + "sha256": "f2b37c183a10922eabc8e0436b426a08866430e96bd0adc7e178951c7fbb5257" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "usage": "input", + "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "usage": "input", + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39" + }, + { + "path": "research/kappa-rebuild/complex/native_extensions.py", + "usage": "input", + "git_blob": "7f84894efc309546a903d314c7ac1473e7f594a8", + "sha256": "50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3" + }, + { + "path": "research/kappa-rebuild/complex/power_two_balance.py", + "usage": "input", + "git_blob": "a55ae0ce78a1861965f899a82604b276260f636c", + "sha256": "76929bb3887911ccf100c4593574b8a1c82ee64e96f939a8aca196869438b424" + }, + { + "path": "research/kappa-rebuild/complex/rebuild_native.py", + "usage": "input", + "git_blob": "78a7b1b0e6e43a1347fb361f45c6e0eaff8dd27b", + "sha256": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5" + }, + { + "path": "research/missing-join-frame/PATCH.json", + "usage": "input", + "git_blob": "f96d295d40014d4dd503f58eb3cdabcbb4b8e101", + "sha256": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + } + ] +} diff --git a/research/quotient-kernel-family/TASK.json b/research/quotient-kernel-family/TASK.json new file mode 100644 index 0000000000..822eadfcf6 --- /dev/null +++ b/research/quotient-kernel-family/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "complex-rank-shape-decoder", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "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": "Classify the kernel directions v of F2^9 for which the ambient quotient of open PR #4596 passes the shipped literal replay, describe the admissible set exactly, and price its best member with #4596's invoice.", + "scope_change_reason": "PR #4596 answered this card with one quotient direction (511) and left open whether 511 is the unique removable direction. The classification answers that question for the shipped check; it is a complex-side result and does not change the outer kappa.", + "bottleneck_link": "Complex-side supplier result conditional on #4596. The outer kappa in #4596 is limited by the BIT side, so a better complex saving does not move it until the BIT admission chain moves; #4604's endpoint-chart question also applies.", + "budget_minutes": 120, + "stop_rule": "Stop at the exact one-dimensional classification under the shipped replay, its coset description, the dimension-two obstruction and exact lowering for 153 and 511. Do not study recomputed centre ranks or controller strictification.", + "outcome": "completed", + "evidence": "verify.py derives the eight centre hyperplanes and the 112 main-final hyperplanes from the pinned base word, checks the rank-4 coset and the pair condition, replays all 32 predicted directions and four rejected controls with the shipped literal replay; --scan shards replay all 511 directions; --physical lowers every transport of the 153 and 511 words exactly.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does an operator-level endpoint check accept any of the 32 quotient words?", + "why_it_matters": "If output charts are part of the supplier contract (#4604), the whole family, 511 included, may be inadmissible.", + "first_step": "Run #4604's endpoint-frame comparison on the v = 153 quotient word.", + "blocked_by": "The required output charts are not an input to the shipped replay." + }, + { + "question": "Which kernels pass if centre transport ranks are recomputed instead of hard-coded to 8?", + "why_it_matters": "The 479 rejections all come from the hard-coded centre rank; a recomputing pipeline would accept a different set.", + "first_step": "Recompute centre ranks in synthesize for one rejected direction and replay it.", + "blocked_by": "A changed synthesizer is a different certificate and needs its own review." + }, + { + "question": "Does #4596's controller strictification hold when the controller targets come from a quotient word?", + "why_it_matters": "An unverified local substitution gave a negative delta-row margin for all 32 directions, 511 included; an outer kappa for the family depends on it.", + "first_step": "Recompute the delta row of #4596's controller with the v = 511 targets.", + "blocked_by": "Requires the controller contract #4596 uses." + } + ] +} diff --git a/research/quotient-kernel-family/VERIFY.json b/research/quotient-kernel-family/VERIFY.json new file mode 100644 index 0000000000..f568adb0f7 --- /dev/null +++ b/research/quotient-kernel-family/VERIFY.json @@ -0,0 +1,87 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/fresh-helper-boundary/CHANGES.json", + "research/fresh-helper-boundary/native.py", + "research/joint-helper-lattice/PATCH.json", + "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "research/kappa-function-composition/complex/prune_native.py", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/kappa-rebuild/complex/native_extensions.py", + "research/kappa-rebuild/complex/power_two_balance.py", + "research/kappa-rebuild/complex/rebuild_native.py", + "research/missing-join-frame/PATCH.json", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Centre-hyperplane normals, rank-4 coset, closed form, dimension-two obstruction, main-final uniqueness of 511, shipped replay of all 32 predicted directions with declared 153/511 profiles and prices, rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--scan", + "1", + "255" + ], + "timeout_seconds": 240, + "checks": "Shipped literal replay of directions 1..255 accepts exactly the predicted directions." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--scan", + "256", + "511" + ], + "timeout_seconds": 240, + "checks": "Shipped literal replay of directions 256..511 accepts exactly the predicted directions." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--physical", + "153" + ], + "timeout_seconds": 300, + "checks": "Exact Clifford lowering of every realised transport of the v = 153 word, both orientations." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py", + "--physical", + "511" + ], + "timeout_seconds": 300, + "checks": "Exact Clifford lowering of every realised transport of the v = 511 word, both orientations." + } + ] +} diff --git a/research/quotient-kernel-family/quotient.py b/research/quotient-kernel-family/quotient.py new file mode 100644 index 0000000000..d708647291 --- /dev/null +++ b/research/quotient-kernel-family/quotient.py @@ -0,0 +1,301 @@ +#!/usr/bin/env python3 +"""Build and replay the ambient-quotient words of the PR #4596 family. + +Builds the pinned PR4470/PR4441/joint-patch word, then for a candidate kernel +vector v in F2^9 builds the quotient word (frames -> images under a linear +surjection with kernel span{v}), replays both orientations with the SHIPPED +evaluators, and reports the paid profile, helper profile and local deficit. + +The certificate for admissibility is the shipped literal replay +(research/kappa-rebuild/complex/native_extensions.py:literal_replay) plus the +shipped endpoint table (research/kappa-causal-continuation/buffer-borrowing/ +verify_buffers.py:expected) -- this script never re-implements the semantics. +The quotient, the helper re-padding and the invoice constants follow DaysSky's +PR #4596 (research/complex-quotient-511); the base word is Cinna Davis's PR4470 +word with the PR4441 and joint-helper patches. + +Imported by verify.py; this module writes no files. +""" +import sys +from collections import Counter +from copy import deepcopy +from pathlib import Path + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(ROOT/'research/fresh-helper-boundary')) +sys.path.insert(0, str(ROOT/'research/joint-helper-lattice')) + +import native as F # noqa: E402 + +JOINT = ROOT/'research/joint-helper-lattice' +ROLES = 632 +MAINS = 224 +BLOCK = 8 +PORTS = 112 +PAIRS = 16 +SPLIT = 7 +CALLS = 18 + + +# ---------------------------------------------------------------- base word +def build_base(): + """The pinned word of PR4470 + PR4441 + the joint-helper patch (as PR4596).""" + patch = F.read(JOINT/'PATCH.json') + c = F.read(F.BASE/'THREE-base-FULL-IDENTITY-CANONICAL.json.gz') + original = F.read(F.BASE/'THREE-base-FULL-IDENTITY-NATIVE.json.gz') + parent = F.read(F.HERE/'CHANGES.json') + maps = {d: F.gates(p) for d, p in original.items()} + F.need(set(maps['forward']) == set(maps['backward']), 'Same scalar contact inventory') + for key, field in [('entrances', 'start'), ('exits', 'final')]: + for r, old, new in parent[key]: + F.need(c[field][r] == old, 'Parent boundary pin') + c[field][r] = new + for phase, ordinal, old, new in parent['gates']: + for d, p in original.items(): + i = maps[d][phase, ordinal] + F.need(p[i][2] == old, 'Parent scalar pin') + p[i][2] = new + prior = F.read(ROOT/'research/missing-join-frame/PATCH.json') + F.need(prior['phase'] == 'B' and prior['ordinal'] == 480, 'Exact prior contact') + prior_frame = len(c['frames']) + c['frames'].append(prior['new_basis']) + for d, p in original.items(): + i = maps[d]['B', 480] + F.need(p[i][2] == prior['old_frame'], 'Missing-span parent pin') + p[i][2] = prior_frame + labels = {frozenset(F.span(b)): i for i, b in enumerate(c['frames'])} + + def label(b): + s = frozenset(F.span(b)) + F.need(len(s) == 2**len(b), 'Independent binary basis') + if s not in labels: + labels[s] = len(c['frames']) + c['frames'].append(b) + return labels[s] + + for move in patch['changes']: + phase, r = move['phase'], move['ordinal'] + a, b = F.span(move['old']), F.span(move['new']) + F.need(a != b, 'No unchanged patch entry') + f = label(move['new']) + if phase in ('entrance', 'exit'): + field = 'start' if phase == 'entrance' else 'final' + F.need(F.span(c['frames'][c[field][r]]) == a, 'Current source pin') + c[field][r] = f + else: + for d, p in original.items(): + i = maps[d][phase, r] + F.need(F.span(c['frames'][p[i][2]]) == a, 'Current scalar source pin') + p[i][2] = f + return c, original + + +# ---------------------------------------------------------------- quotient +def span_of(vectors): + out = {0} + for v in vectors: + out |= {x ^ v for x in out} + return frozenset(out) + + +def dedupe(vectors): + pivots = {} + keep = [] + for v in vectors: + y = v + while y: + bit = y.bit_length()-1 + if bit in pivots: + y ^= pivots[bit] + else: + pivots[bit] = y + keep.append(v) + break + return keep + + +def projector(v): + """Linear map pi_v with kernel span{v}; image = {x : x_p = 0}, p = top bit.""" + p = v.bit_length()-1 + mask = 1 << p + def pi(x): + return (x ^ v) if (x & mask) else x + return pi, p + + +def quotient(c, programs, v): + """Return (word, programs, remap) with every frame replaced by pi_v(image).""" + pi, _ = projector(v) + frames = c['frames'] + span_index = {} + new_frames = [] + + def frame_index(basis): + mapped = dedupe([pi(x) for x in basis]) + key = span_of(mapped) + if key not in span_index: + span_index[key] = len(new_frames) + new_frames.append(mapped) + return span_index[key] + + remap = {i: frame_index(basis) for i, basis in enumerate(frames)} + word = deepcopy(c) + for r in range(len(word['start'])): + word['start'][r] = remap[word['start'][r]] + word['final'][r] = remap[word['final'][r]] + out_programs = {} + for direction, program in programs.items(): + out = [] + for event in program: + e = deepcopy(event) + if e[0] == 'scalar': + e[2] = remap[e[2]] + elif e[0] == 'warp': + e[3] = remap[e[3]] + e[4] = remap[e[4]] + elif e[0] == 'climb': + e[3] = remap[e[3]] + e[4] = remap[e[4]] + elif e[0] == 'center': + e[2] = remap[e[2]] + e[3] = remap[e[3]] + out.append(e) + out_programs[direction] = out + word['frames'] = new_frames + return word, out_programs, remap + + +def pad_ambient(word, p): + """Spend the unused axis on one helper so the word occupies nine axes.""" + axis = 1 << p + frames = word['frames'] + for role in range(MAINS, ROLES): + final = word['final'][role] + if axis in span_of(frames[final]): + continue + new = dedupe(frames[final]+[axis]) + if len(new) != len(frames[final])+1: + continue + frames.append(new) + word['final'][role] = len(frames)-1 + return role + return None + + +# ---------------------------------------------------------------- pricing +def moment(profile, exponent): + return sum(n*(r**exponent) for r, n in profile.items() if n and r > 0) + + +def rank_mass(profile): + return sum(r*n for r, n in profile.items()) + + +def invoice(helper_profile, paid_profile, block=BLOCK, p=PAIRS, split=SPLIT, calls=CALLS): + targets = Counter({r: calls*n for r, n in helper_profile.items()}) + paid = Counter({r: calls*n for r, n in paid_profile.items()}) + thin = PORTS*(2*p+1-calls) + paid[1] += thin + targets[1+block*(p+2)] += 2*PORTS + for length in (split, p-1-split): + for j in range(1, length+1): + targets[1+block*(j+1)] += 2*PORTS + paid[block*(j+1)] += 2*PORTS + surplus = rank_mass(targets)-rank_mass(paid) + return targets, paid, surplus, thin + + +def dual_ok(T, P, kappa, u=0.2, c=20.0, gamma=0.97): + t = 1.0-kappa + return moment(P, t) < moment(T, t) and moment(P, t+u) < gamma*(c**u)*moment(T, t) + + +def admissible_kappa(T, P, lo=1e-7, hi=0.25, steps=2400): + best = None + prev = None + for i in range(steps+1): + k = lo+(hi-lo)*i/steps + if dual_ok(T, P, k): + best, prev = k, k + elif prev is not None and best == prev: + a, b = prev, k + for _ in range(90): + mid = (a+b)/2 + if dual_ok(T, P, mid): + a = mid + else: + b = mid + return a + return best + + +# ---------------------------------------------------------------- evaluation +def evaluate(base_word, base_programs, v, V, X): + """Return a record for the kernel span{v}; record['admissible'] says it replayed.""" + rec = {'kernel': v, 'admissible': False, 'reason': None} + try: + word, programs, remap = quotient(base_word, base_programs, v) + except Exception as exc: # noqa: BLE001 + rec['reason'] = 'quotient:%s' % exc + return rec + p = v.bit_length()-1 + padded = pad_ambient(word, p) + if padded is None: + rec['reason'] = 'no helper absorbs the unused axis' + return rec + rec['padded_helper'] = padded + frames = word['frames'] + union = set() + for basis in frames: + union |= span_of(basis) + ambient = len(union).bit_length()-1 + rec['ambient_dim'] = ambient + if ambient != BLOCK+1: + rec['reason'] = 'ambient dim %d (block-8 charge invalid)' % ambient + return rec + ranks = [len(b) for b in frames] + mains = [ranks[word['final'][r]]-ranks[word['start'][r]] for r in range(MAINS)] + helpers = Counter(ranks[word['final'][r]]-ranks[word['start'][r]] for r in range(MAINS, ROLES)) + rec['main_widths'] = dict(sorted(Counter(mains).items())) + rec['main_rank_mass'] = sum(mains) + rec['helper_widths'] = dict(sorted(helpers.items())) + rec['helper_rank_mass'] = rank_mass(helpers) + try: + profiles = {} + for direction in ('forward', 'backward'): + program = [list(e) for e in programs[direction]] + synthesized = F.synthesize({'frames': frames, 'start': word['start'], + 'final': word['final'], 'precondition': [], 'A': [], + 'B': [], 'cut': [], 'compensation': [], 'cleanup': [], + 'tail': []}, program) + rows, receipt = X.literal_replay(V, {'frames': frames, 'start': word['start'], + 'final': word['final'], 'v': PORTS, 'R': 408}, + synthesized, direction == 'backward') + bad = [r for r in range(ROLES) + if rows['L', r] != V.expected(('L', r), [], direction == 'backward', False)] + if bad: + rec['reason'] = '%s: %d endpoint failures (first %s)' % (direction, len(bad), bad[:5]) + return rec + if rows[('C', 0)]: + rec['reason'] = '%s: owned C not cleared' % direction + return rec + profiles[direction] = Counter({int(k): val for k, val in receipt['paid_profile'].items()}) + if profiles['forward'] != profiles['backward']: + rec['reason'] = 'directions disagree' + return rec + except Exception as exc: # noqa: BLE001 + rec['reason'] = 'replay:%s' % exc + return rec + paid = profiles['forward'] + rec['paid_profile'] = dict(sorted(paid.items())) + rec['paid_rank_mass'] = rank_mass(paid) + rec['local_deficit'] = rec['paid_rank_mass']-rec['helper_rank_mass'] + targets, paidc, surplus, thin = invoice(dict(helpers), dict(paid)) + rec['surplus'] = surplus + rec['thin'] = thin + kappa = admissible_kappa(targets, paidc) + rec['kappa'] = kappa + rec['admissible'] = True + return rec diff --git a/research/quotient-kernel-family/verify.py b/research/quotient-kernel-family/verify.py new file mode 100644 index 0000000000..8d91eb0e30 --- /dev/null +++ b/research/quotient-kernel-family/verify.py @@ -0,0 +1,265 @@ +#!/usr/bin/env python3 +"""Classify the ambient-quotient kernels of the PR #4596 word. + +Default run (about 30 s): + 1. reads the centre transports of the pinned base word (ground <-> dim-8 + frame, charged rank 8) and checks that the eight frames they reach are + hyperplanes of F2^9 with the declared normals; + 2. checks that the normals have GF(2) rank 4, so the directions outside all + eight hyperplanes form a coset of a 5-dimensional subspace with 32 points; + 3. checks that this coset meets its own difference subspace nowhere, so no + 2-dimensional kernel has all three nonzero vectors outside the hyperplanes; + 4. replays every one of the 32 predicted directions with the shipped literal + replay (both orientations, 632/632 endpoints, owned C cleared) and checks + the declared profiles and prices for v = 153 and v = 511; + 5. replays rejection controls, which must fail the shipped paid-rank check; + 6. checks that 511 is the only direction outside all 112 dim-8 main finals. + +Options: + --scan LO HI replay every direction LO <= v <= HI and require that the + shipped replay accepts exactly the predicted directions + --physical V lower every realised transport of the v = V word exactly and + require Fourier rank = |dim difference| (the shipped convention) + +Exit status is non-zero on any mismatch. +""" +import sys +from pathlib import Path + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) + +import quotient as Q # noqa: E402 + +F = Q.F +ROOT = Q.ROOT +NORMALS = [42, 7, 25, 52, 82, 127, 97, 76] +PREDICTED = [7, 25, 42, 52, 76, 82, 97, 127, 135, 153, 170, 180, 204, 210, 225, 255, + 263, 281, 298, 308, 332, 338, 353, 383, 391, 409, 426, 436, 460, 466, 481, 511] +DECLARED = { + 153: {'main_widths': {7: 168, 8: 56}, + 'helper_widths': {3: 2, 4: 26, 6: 7, 7: 47, 8: 325, 9: 1}, + 'paid_profile': {1: 1991, 2: 424, 3: 389, 4: 147, 5: 24, 8: 8}, + 'paid_rank_mass': 4778, 'helper_rank_mass': 3090, 'local_deficit': 1688, + 'surplus': 3776, 'thin': 1680, 'kappa': 0.016567169219161848}, + 511: {'main_widths': {7: 112, 8: 112}, + 'helper_widths': {3: 2, 4: 26, 6: 7, 7: 47, 8: 325, 9: 1}, + 'paid_profile': {1: 2034, 2: 382, 3: 412, 4: 139, 5: 36, 8: 8}, + 'paid_rank_mass': 4834, 'helper_rank_mass': 3090, 'local_deficit': 1744, + 'surplus': 2768, 'thin': 1680, 'kappa': 0.012091850233828692}, +} +WIDENED_HELPERS = [7, 52, 82, 97, 391, 436, 466, 481] +REJECTED_CONTROLS = [1, 2, 256, 510] +PAID_RANK_REASON = 'replay:Paid rank and source frame' + + +def need(ok, message): + if not ok: + raise SystemExit('FAIL: ' + message) + + +def parity(a, b): + return bin(a & b).count('1') & 1 + + +def gf2_rank(vectors): + pivots = [] + for v in vectors: + for p in pivots: + v = min(v, v ^ p) + if v: + pivots.append(v) + return len(pivots) + + +def evaluators(): + V = F.load(ROOT/'research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py', 'qkf_rows') + X = F.load(ROOT/'research/kappa-rebuild/complex/native_extensions.py', 'qkf_literal') + return V, X + + +def synthesized(word, programs, direction): + return F.synthesize({'frames': word['frames'], 'start': word['start'], 'final': word['final'], + 'precondition': [], 'A': [], 'B': [], 'cut': [], 'compensation': [], + 'cleanup': [], 'tail': []}, [list(e) for e in programs[direction]]) + + +def centre_hyperplanes(word, programs): + """The dim-8 frames joined to the ground frame by centre transports, as vector sets. + + Forward centre events run frame -> ground and backward events run + ground -> frame; both orientations must name the same eight frames. + """ + seen = {} + for direction in ('forward', 'backward'): + frames = [] + for e in synthesized(word, programs, direction): + if e[0] == 'center': + need(e[4] == 8, 'centre transport charged rank %s, expected 8' % e[4]) + ends = sorted((e[2], e[3]), key=lambda i: len(word['frames'][i])) + need([len(word['frames'][i]) for i in ends] == [0, 8], 'centre edge is not ground <-> dim 8') + frames.append(ends[1]) + seen[direction] = sorted(frames) + need(seen['forward'] == seen['backward'], 'orientations disagree on the centre frames') + out = [] + for i in seen['forward']: + span = Q.span_of(word['frames'][i]) + if span not in out: + out.append(span) + return out + + +def check_structure(word, programs): + hyperplanes = centre_hyperplanes(word, programs) + need(len(hyperplanes) == 8, 'expected 8 distinct centre source frames, got %d' % len(hyperplanes)) + normals = [] + for h in hyperplanes: + need(len(h) == 256, 'centre source frame is not a hyperplane of F2^9') + found = [lam for lam in range(1, 512) if all(parity(lam, x) == 0 for x in h)] + need(len(found) == 1, 'hyperplane normal is not unique') + normals.append(found[0]) + need(sorted(normals) == sorted(NORMALS), 'normals %s != declared %s' % (normals, NORMALS)) + rank = gf2_rank(normals) + need(rank == 4, 'normal rank %d != 4' % rank) + union = set().union(*hyperplanes) + outside = sorted(v for v in range(1, 512) if v not in union) + need(len(union) == 480, 'union has %d vectors, expected 480' % len(union)) + need(outside == PREDICTED, 'outside-set differs from the declared 32 directions') + need(outside == [v for v in range(1, 512) if all(parity(lam, v) for lam in normals)], + 'outside-set is not {v : lambda_i(v) = 1 for all i}') + base = outside[0] + difference = {v ^ base for v in outside} + need(len(difference) == 32 and all(a ^ b in difference for a in difference for b in difference), + 'outside-set is not a coset of a 5-dimensional subspace') + need(not difference & set(outside), 'outside-set meets its difference subspace') + need(all(lam < 128 for lam in normals) and + outside == sorted(h + 128*i + 256*j for h in normals for i in (0, 1) for j in (0, 1)), + 'outside-set is not {normal + 128 i + 256 j}') + pairs = sum(1 for u in outside for w in outside if u < w and u ^ w in set(outside)) + need(pairs == 0, '%d two-dimensional kernels survive' % pairs) + print('centre source frames: 8 hyperplanes, normals %s, GF(2) rank %d' % (sorted(normals), rank)) + print('outside-set: 32 directions, a coset of a 5-dimensional subspace; ' + 'two-dimensional kernels inside it: 0') + + +def check_geometric(word): + """Under the main-final condition, 511 is the only direction outside every dim-8 main final.""" + finals = [] + for r in range(Q.MAINS): + basis = word['frames'][word['final'][r]] + if len(basis) == 8: + span = Q.span_of(basis) + if span not in finals: + finals.append(span) + need(len(finals) == 112, 'expected 112 distinct dim-8 main finals, got %d' % len(finals)) + normals = [] + for h in finals: + found = [lam for lam in range(1, 512) if all(parity(lam, x) == 0 for x in h)] + need(len(found) == 1, 'main-final normal is not unique') + normals.append(found[0]) + need(gf2_rank(normals) == 9, 'main-final normals do not have full rank 9') + outside = [v for v in range(1, 512) if not any(v in h for h in finals)] + need(outside == [511], 'directions outside every main final: %s' % outside) + print('main finals: 112 dim-8 hyperplanes, normals of GF(2) rank 9; only 511 lies outside all') + + +def check_member(rec, v): + want = DECLARED[v] + for key, value in want.items(): + got = rec.get(key) + need(got == value, 'v=%d %s: got %r, declared %r' % (v, key, got, value)) + + +def check_family(word, programs, V, X): + records = {} + for v in PREDICTED: + rec = Q.evaluate(word, programs, v, V, X) + need(rec['admissible'], 'predicted direction %d rejected: %s' % (v, rec['reason'])) + records[v] = rec + for v in DECLARED: + check_member(records[v], v) + widened = sorted(v for v, r in records.items() + if r['helper_widths'] != DECLARED[153]['helper_widths']) + need(widened == WIDENED_HELPERS, 'directions with a widened helper profile: %s' % widened) + need(all(records[v]['helper_widths'] == {4: 28, 6: 7, 7: 47, 8: 325, 9: 1} for v in widened), + 'unexpected widened helper profile') + ranking = sorted(PREDICTED, key=lambda v: -records[v]['kappa']) + need(ranking[0] == 153, 'best direction is %d, not 153' % ranking[0]) + for v in REJECTED_CONTROLS: + rec = Q.evaluate(word, programs, v, V, X) + need(not rec['admissible'] and rec['reason'] == PAID_RANK_REASON, + 'control %d: admissible=%s reason=%r' % (v, rec['admissible'], rec['reason'])) + print('replayed all 32 predicted directions: 632/632 endpoints, both orientations, C cleared') + for v in ranking[:3] + [511]: + r = records[v] + print(' v=%3d deficit %d surplus %d complex saving %.12f' + % (v, r['local_deficit'], r['surplus'], r['kappa'])) + print('rejection controls %s: shipped paid-rank check rejects each' % REJECTED_CONTROLS) + + +def scan(word, programs, V, X, lo, hi): + need(1 <= lo <= hi <= 511, 'scan range must lie in 1..511') + accepted = [] + for v in range(lo, hi+1): + rec = Q.evaluate(word, programs, v, V, X) + need(rec['admissible'] == (v in PREDICTED), + 'v=%d admissible=%s, predicted %s (%s)' % (v, rec['admissible'], v in PREDICTED, rec['reason'])) + if not rec['admissible']: + need(rec['reason'] == PAID_RANK_REASON, 'v=%d rejected for %r' % (v, rec['reason'])) + else: + accepted.append(v) + print('scan %d..%d: %d directions, %d accepted, all as predicted' + % (lo, hi, hi-lo+1, len(accepted))) + + +def physical(word, programs, v): + need(v in PREDICTED, 'physical check needs an admissible direction') + ce = F.load(ROOT/'research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py', + 'qkf_clifford') + P = F.load(ROOT/'research/kappa-function-composition/complex/prune_native.py', 'qkf_lowering') + X = F.load(ROOT/'research/kappa-rebuild/complex/native_extensions.py', 'qkf_literal_physical') + qword, qprograms, _ = Q.quotient(word, programs, v) + need(Q.pad_ambient(qword, v.bit_length()-1) is not None, 'no helper absorbs the unused axis') + frames = qword['frames'] + edges = set() + for direction in ('forward', 'backward'): + for e in synthesized(qword, qprograms, direction): + if e[0] == 'climb': + edges.add((e[3], e[4])) + elif e[0] == 'center': + edges.add((e[2], e[3])) + for r in range(Q.MAINS, Q.ROLES): + edges.add((qword['start'][r], qword['final'][r])) + bad = 0 + for a, b in sorted(edges): + want = abs(len(frames[b])-len(frames[a])) + op = ce.canonical_frame(9, frames[a]).adjoint().then(ce.canonical_frame(9, frames[b])) + for actual in (op, P.conjugate(ce, op)): + if X.N.lower_exact(P, ce, actual)['rank'] != want: + bad += 1 + need(bad == 0, 'v=%d: %d lowering mismatches' % (v, bad)) + print('physical lowering v=%d: %d distinct edges, both orientations, 0 mismatches' % (v, len(edges))) + + +def main(): + args = sys.argv[1:] + word, programs = Q.build_base() + if '--physical' in args: + physical(word, programs, int(args[args.index('--physical')+1])) + print('PASS_QUOTIENT_KERNEL_PHYSICAL') + return + V, X = evaluators() + if '--scan' in args: + i = args.index('--scan') + scan(word, programs, V, X, int(args[i+1]), int(args[i+2])) + print('PASS_QUOTIENT_KERNEL_SCAN') + return + check_structure(word, programs) + check_geometric(word) + check_family(word, programs, V, X) + print('PASS_QUOTIENT_KERNEL_FAMILY') + + +if __name__ == '__main__': + main()