diff --git a/research/four-axis-sharp-cutoff/COEFFICIENTS.json b/research/four-axis-sharp-cutoff/COEFFICIENTS.json new file mode 100644 index 0000000000..643c496229 --- /dev/null +++ b/research/four-axis-sharp-cutoff/COEFFICIENTS.json @@ -0,0 +1,78 @@ +{ + "keys": [ + [ + 1, + 0, + 4 + ], + [ + 2, + 1, + 4 + ], + [ + 2, + 2, + 4 + ], + [ + 3, + 2, + 2 + ], + [ + 3, + 4, + 0 + ], + [ + 4, + 2, + 4 + ], + [ + 4, + 3, + 4 + ], + [ + 5, + 4, + 4 + ], + [ + 6, + 3, + 2 + ], + [ + 6, + 4, + 2 + ], + [ + 7, + 3, + 4 + ], + [ + 15, + 4, + 4 + ] + ], + "coefficients": [ + 21, + -3, + 1, + 0, + 0, + 1, + -1, + 1, + 0, + 0, + 0, + 0 + ] +} diff --git a/research/four-axis-sharp-cutoff/PROOF.md b/research/four-axis-sharp-cutoff/PROOF.md new file mode 100644 index 0000000000..57eb0b9d91 --- /dev/null +++ b/research/four-axis-sharp-cutoff/PROOF.md @@ -0,0 +1,207 @@ +# The sharp four-axis native window is 9 through 12 + +For the fixed affine/quadratic Gaussian monomial grammar on four axes, the +exact central-residue representation thresholds are + + (L_0,L_1,L_2,L_3) = (12,9,10,11). + +Thus the least uniform cutoff is nine. Four tests at widths 9,10,11,12 decide +all positive widths. Four residue tests are necessary, and no complete test +set can have maximum width below 12. This improves the prior sufficient +four-axis window 11,12,13,14 and proves the new window sharp. It changes no +physical invoice or complete kappa calculation. + +## 1. Grammar and source contract + +Let X = F_2^4. Use input-phase operators + + U(g,q)e_x = i^q(x) e_(g(x)), + q(x) = c + sum_j a_j x_j + 2 sum_(j= L_(f modulo 4). + +The grammar, central ideals, Fourier separation and complete endpoint contract +are from Ali Romman's +[PR #5369](https://github.com/CrocSwap/integer-mult-bounds/pull/5369). +His [PR #5529](https://github.com/CrocSwap/integer-mult-bounds/pull/5529) +gives the 2n+3 sufficient construction. Joseph Anglada's +[PR #5542](https://github.com/CrocSwap/integer-mult-bounds/pull/5542) +proves sharpness on three axes and asks for a higher-axis stabilizer witness. +SOURCES.json pins their proofs. No predecessor executable is imported. + +## 2. A finite GL(4,2) coset certificate + +For h in GL(4,2), define a(h) by the triple + + (order(h), rank(h-I), rank(h^2+h+I)). + +All ranks here are over F_2. The complete coefficient table is: + +| Triple | Number of maps | a(h) | +|---|---:|---:| +| (1,0,4) | 1 | 21 | +| (2,1,4) | 105 | -3 | +| (2,2,4) | 210 | 1 | +| (3,2,2) | 1120 | 0 | +| (3,4,0) | 112 | 0 | +| (4,2,4) | 1260 | 1 | +| (4,3,4) | 2520 | -1 | +| (5,4,4) | 1344 | 1 | +| (6,3,2) | 3360 | 0 | +| (6,4,2) | 1680 | 0 | +| (7,3,4) | 5760 | 0 | +| (15,4,4) | 2688 | 0 | + +For a linear hyperplane V, let K_V be its pointwise stabilizer. It has eight +elements. The exact certificate is + + sum_(h in g K_V) a(h) = 0 (1) + +for every g and every V. The checker reconstructs all 20160 invertible maps +in two ways: rank tests on all 65536 binary matrices, and successive choices +outside the span of the earlier columns. Their inventories agree. It checks +all 15 hyperplanes, all 2520 cosets per hyperplane and all eight members of +each coset. Thus (1) has 37800 exact integer checks. COEFFICIENTS.json supplies +the small table; no character table or floating-point rank is an input. + +The three defining invariants make a(h) a conjugacy-invariant function. This +also follows from order and polynomial-rank invariance under similarity. +The finite table can be found by solving the coset equations; the proof needs +only the complete verified sums and a(1)=21, not a representation-theory label. + +## 3. Affine cancellation, including the translation part + +Define the group-algebra element + + B = sum_(h in GL(4,2)) sum_(t in X) a(h) [x -> h x + t]. (2) + +The coefficient of an affine map depends only on its linear part. Conjugation +by an affine map conjugates that linear part, so these coefficients are +constant on affine conjugacy classes. Equation (1) therefore holds for the +pointwise stabilizer of every affine hyperplane, including a translated one. + +If an ordered tuple has proper affine span, place that span in an affine +hyperplane V. For each output tuple, the affine maps that produce it form +an empty set or a coset of its pointwise stabilizer. That stabilizer contains +K_V. Split the output fiber into K_V cosets and use (1). It follows that + + rho_f(B)e_tuple = 0 whenever the tuple has proper affine span. (3) + +For a tuple of full affine span, only the identity affine map fixes it. Its +diagonal coefficient under rho_f(B) is therefore a(1)=21. + +The translation sum in (2) is essential. The eight points with last coordinate +one have full linear span and proper affine span. The GL-only sum has diagonal +entry 21 there, whereas B has entry zero. The verifier checks both values. +Thus a GL-only witness cannot prove the required lower bound at width eight. + +This gives a reusable separation criterion: in this grammar, a phase character +has no full-span realization at a matching width f if and only if its Fourier component +contains a nonzero residual invisible at width f. Necessity uses B times its +phase projector. Sufficiency is the predecessor affine-bucket argument. A +similar criterion in another dimension needs its own nonzero coset certificate. + +## 4. Complete upper certificate + +The phase character of a tuple with multiplicities m_x is + + r = sum_x m_x modulo 4, + u_j = sum_x m_x x_j modulo 4, + v_jk = sum_x m_x x_j x_k modulo 2. + +There are 4*4^4*2^6=65536 such characters. WITNESSES.json.gz has one packed +multiplicity vector for each character. Four bits store each m_x. Its index +packs r in bits 0..1, u_j modulo two in bits 2..5, floor(u_j/2) in bits 6..9, +and the six pair parities in bits 10..15, in lexicographic (j,k) order. + +The checker recalculates each character from literal weighted counts and +checks full affine span by the rank of the homogeneous columns (1,x). +Every witness has length at most L_r and has residue r. Append groups of +four zero points to reach L_r or any larger width of that residue. This proves +that every character is realized with full span at each claimed width. + +For a residual outside I_r, Fourier inversion in the diagonal subgroup gives +an affine bucket with a nonzero character coefficient. Choose the full-span +tuple for that character. Distinct affine maps have different outputs on it, +so its matrix entry is exactly that nonzero coefficient. Hence the residual +cannot be in ker rho_f. The reverse inclusion I_r subset ker rho_f is direct. +This proves the upper kernel equality, not only a finite list of tests. + +The optional C++17 generator enumerates all 30421755 multisets of total length +at most 12. Its transition arithmetic differs from the literal Python checker. +Only the checked witnesses are premises of the upper proof; the generator's +minimum claims and search completeness are not needed for that implication. + +## 5. Exact lower bounds + +Take the character with every u_j and v_jk zero. The four binary coordinate +rows of any realizing tuple generate a doubly even, self-orthogonal code. +Indeed each row has weight divisible by four and distinct rows have even +intersection. The identity wt(a+b)=wt(a)+wt(b)-2|a intersect b| extends these +properties to their span. + +At lengths five, six or seven, a self-orthogonal binary code has dimension +at most floor(f/2), which is less than four. The tuple cannot have full affine +span. At length eight, if the four rows have rank less than four the same +conclusion holds. If they have rank four, the code is self-dual. Every row +is even, so the all-ones row is orthogonal to the code and hence lies in it. +The five homogeneous rows are dependent. Full affine span again fails. + +These four lengths are the last widths of their residues below (12,9,10,11). +If a smaller width in the same residue had a full-span zero-character tuple, +adding four zero points repeatedly would contradict the preceding argument. +The verifier separately enumerates all 730626 multisets at lengths five +through eight. All 439 zero-character multisets have proper affine span, +using a span-closure implementation separate from the upper rank check. + +Define the fixed phase projector and residual + + E_r = (1/65536) sum_(c,a,b) i^(-r c) [D_q], + P_r = B E_r. (4) + +Finite Fourier orthogonality makes rho_f(E_r) the zero-nonconstant-character +projector at residue r and zero at the other residues. Equations (3) and (4) +show rho_f(P_r)=0 at every positive width below L_r and at every wrong residue. +At L_r the certified zero-character full-span tuple has diagonal entry 21. +The same holds after four-zero padding. Thus P_r is a nonzero fixed residual, +is outside I_r, and proves strict kernel inclusion at every smaller matching +width. In particular P_0 vanishes at all positive widths below 12 and is +nonzero at 12. This completes all four sharp threshold proofs. + +The four central ideals have zero intersection. A set of widths decides all +fixed identities if and only if it contains a width at least L_r in each +residue r: the upper argument proves sufficiency; P_r proves necessity. + +## 6. Evidence, limitations and attribution + +Registered normal and optimized Python checks verify all witnesses, two full +group inventories, every hyperplane coset, the low-width multiset census and +five rejection controls. The controls cover the constant residue, a quadratic +phase, affine versus linear span, a wrong nonidentity coefficient and omission +of translations. All checks use exact arithmetic. Same-agent separate methods +are corroboration, not independent human or proof-kernel acceptance. + +The theorem applies entrywise to a single fixed complete register endpoint, +with all independent dirty inputs and required returns. It excludes Hadamards, +width-dependent programs or external coefficients, and undeclared aliases. +It does not provide an efficient group-algebra expansion or a physical supplier. +No source caller, compiler, stock, precision, tape, outer admission or selected +cold replay was run. Complete kappa and the selected frontier are unchanged. + +Credit Joseph Anglada / fluorine for the three-axis coset method and higher-axis +handoff; Ali Romman for the native grammar, Fourier method and sufficient phase +construction; Hiroki KUMAZAKI for +[PR #5522](https://github.com/CrocSwap/integer-mult-bounds/pull/5522) and the +representation-kernel distinction; Mihir Srivastava for +[PR #5521](https://github.com/CrocSwap/integer-mult-bounds/pull/5521). +Retain Jose Manuel, ywz65, Chris R and the native/phase/compiler source lineage. +Binary codes, group cosets and Fourier projectors are classical. The four-axis +certificate, affine translation extension and sharp threshold result are by +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/four-axis-sharp-cutoff/README.md b/research/four-axis-sharp-cutoff/README.md new file mode 100644 index 0000000000..e5ba4516ad --- /dev/null +++ b/research/four-axis-sharp-cutoff/README.md @@ -0,0 +1,47 @@ +# Sharp four-axis native cutoff + +The exact four-axis affine/quadratic Gaussian monomial thresholds are +**(12,9,10,11)** by residue. The least cutoff is **9**, and the test window +**9,10,11,12** is sharp. The former sufficient window was 11,12,13,14. +This reduces a native identity verification bound. Complete kappa is unchanged. + +Read [PROOF.md](PROOF.md), [RESULT.json](RESULT.json), +[COEFFICIENTS.json](COEFFICIENTS.json) and [SOURCES.json](SOURCES.json). + +```sh +python3 -B scripts/research_package.py --package research/four-axis-sharp-cutoff +``` + +Python 3.12 and the standard library suffice. Expected markers: +`PASS_FOUR_AXIS_SHARP_CUTOFF` and `PASS_REGISTERED_RESEARCH_PACKAGE`. +The normal and optimized runs check all 65536 phase witnesses, 20160 maps, +37800 hyperplane cosets, 730626 low-width multisets and five rejection controls. +The proof includes the all-width padding and kernel arguments. + +The finite witness file can also be rebuilt with C++17: + +```sh +c++ -O3 -std=c++17 research/four-axis-sharp-cutoff/build_certificate.cpp -o /tmp/four-axis-certificate +/tmp/four-axis-certificate > /tmp/four-axis-witnesses.txt +python3 research/four-axis-sharp-cutoff/pack_witnesses.py /tmp/four-axis-witnesses.txt /tmp/four-axis-witnesses.json.gz +``` + +The decoded witness vector must match WITNESSES.json.gz. Gzip headers can +differ between Python versions. Generation is optional; +the registered verifier checks every witness without trusting the generator. +No compiler, physical caller, selected cold replay or full multiplication proof +is included. The fixed grammar and full dirty-input/return contract are required. + +## Open next questions + +For higher dimensions, find a nonzero conjugacy-invariant GL(n,2) coefficient +function with zero pointwise-hyperplane coset sums. Translation summation then +extends it to the affine group as in this proof. Such a certificate would reduce +sharp representation thresholds to exact full-span phase-character realization. +A general all-dimension existence and optimal character bound remain open here. + +For physical use, bind a complete four-axis endpoint to the grammar before +using the smaller window. Its expansion and physical invoice remain separate. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. Predecessor +roles and classical methods are credited in the proof. diff --git a/research/four-axis-sharp-cutoff/RESULT.json b/research/four-axis-sharp-cutoff/RESULT.json new file mode 100644 index 0000000000..104c8a06e8 --- /dev/null +++ b/research/four-axis-sharp-cutoff/RESULT.json @@ -0,0 +1,137 @@ +{ + "status": "PASS_FOUR_AXIS_SHARP_CUTOFF", + "cutoff": 9, + "residue_thresholds": [ + 12, + 9, + 10, + 11 + ], + "phase_characters": 65536, + "witness_sha256": "7a9a369cdc9378a382e2769101b01de5167eeea77dc785815954a00daa046ed0", + "witness_length_histogram": { + "5": 2688, + "6": 10528, + "7": 15568, + "8": 16333, + "9": 13696, + "10": 5856, + "11": 816, + "12": 51 + }, + "gl4_elements": 20160, + "class_types": [ + [ + [ + 1, + 0, + 4 + ], + 1 + ], + [ + [ + 2, + 1, + 4 + ], + 105 + ], + [ + [ + 2, + 2, + 4 + ], + 210 + ], + [ + [ + 3, + 2, + 2 + ], + 1120 + ], + [ + [ + 3, + 4, + 0 + ], + 112 + ], + [ + [ + 4, + 2, + 4 + ], + 1260 + ], + [ + [ + 4, + 3, + 4 + ], + 2520 + ], + [ + [ + 5, + 4, + 4 + ], + 1344 + ], + [ + [ + 6, + 3, + 2 + ], + 3360 + ], + [ + [ + 6, + 4, + 2 + ], + 1680 + ], + [ + [ + 7, + 3, + 4 + ], + 5760 + ], + [ + [ + 15, + 4, + 4 + ], + 2688 + ] + ], + "hyperplane_cosets": 37800, + "lower_multisets": { + "5": 15504, + "6": 54264, + "7": 170544, + "8": 490314 + }, + "lower_zero_phase_multisets": { + "5": 16, + "6": 51, + "7": 66, + "8": 306 + }, + "threshold_diagonal_entry": 21, + "rejected_controls": 5, + "kappa_change": null +} diff --git a/research/four-axis-sharp-cutoff/SOURCES.json b/research/four-axis-sharp-cutoff/SOURCES.json new file mode 100644 index 0000000000..18af020061 --- /dev/null +++ b/research/four-axis-sharp-cutoff/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/native-tensor-cutoff/PROOF.md", + "usage": "input", + "git_blob": "2d92f17cd8e1064028656cd4ff06c1d38f14ebc0", + "sha256": "b2d31ea52b652f43cc8576affde6092a884d2832820221a43933e7e27dc07041" + }, + { + "path": "research/shorter-native-phase-witness/README.md", + "usage": "input", + "git_blob": "5b68f6be4a297f6ccc1ac1631f40d310ff2236b4", + "sha256": "abc1224cb79a7056d476636522100a375dbe7d51f2e9a985e667d0d7729f3212" + }, + { + "path": "research/three-axis-sharp-cutoff/PROOF.md", + "usage": "input", + "git_blob": "ef0be5ce6b06cecbd3e414a492eda35fca673dee", + "sha256": "6aeeb430e589e34481ea1e867bd99334e6094a5c59b252ce9b87fcce3cffe217" + } + ] +} diff --git a/research/four-axis-sharp-cutoff/TASK.json b/research/four-axis-sharp-cutoff/TASK.json new file mode 100644 index 0000000000..dbeab22248 --- /dev/null +++ b/research/four-axis-sharp-cutoff/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "6cf7a683f447b9f1e2333791907fd92be5009a63", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the sharp four-axis monomial native identity cutoff with complete phase witnesses and affine stabilizer cancellation.", + "scope_change_reason": "The PR5542 higher-axis handoff requests a mathematical cutoff theorem before formalization. Three-axis sharpness is already complete.", + "bottleneck_link": "Reduce the complete four-axis endpoint test window and prove its necessity; expose the affine translation obligation needed for sound native verification.", + "budget_minutes": 120, + "stop_rule": "Stop at all four sharp residue thresholds with exact certificates; do not split residues into separate contributions.", + "outcome": "completed", + "evidence": "PROOF.md; RESULT.json; WITNESSES.json.gz; COEFFICIENTS.json", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance with mathematics, enumeration, verification, code and writing.", + "open_questions": [ + { + "question": "Does the hyperplane-coset certificate exist in every higher dimension, and what are the exact character thresholds?", + "why_it_matters": "The affine extension would convert character bounds into sharp representation bounds.", + "first_step": "Construct a nonzero conjugacy-invariant coefficient function with zero coset sums, then solve full-span phase realization.", + "blocked_by": "No higher-dimensional certificate or optimal all-dimension character construction is provided here." + } + ] +} diff --git a/research/four-axis-sharp-cutoff/VERIFY.json b/research/four-axis-sharp-cutoff/VERIFY.json new file mode 100644 index 0000000000..2f8aeb05f4 --- /dev/null +++ b/research/four-axis-sharp-cutoff/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/native-tensor-cutoff/PROOF.md", + "research/shorter-native-phase-witness/README.md", + "research/three-axis-sharp-cutoff/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Every phase witness, two complete group inventories, all hyperplane cosets, the low-width census and five controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The complete exact certificate checks with assertions disabled." + } + ] +} diff --git a/research/four-axis-sharp-cutoff/WITNESSES.json.gz b/research/four-axis-sharp-cutoff/WITNESSES.json.gz new file mode 100644 index 0000000000..452b5ec0c2 Binary files /dev/null and b/research/four-axis-sharp-cutoff/WITNESSES.json.gz differ diff --git a/research/four-axis-sharp-cutoff/build_certificate.cpp b/research/four-axis-sharp-cutoff/build_certificate.cpp new file mode 100644 index 0000000000..71ca48f0cf --- /dev/null +++ b/research/four-axis-sharp-cutoff/build_certificate.cpp @@ -0,0 +1,79 @@ +// Enumerate all four-axis phase witnesses through width 12. +// Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +#include +#include +#include + +namespace { +constexpr int limit = 12; +std::array full_span{}; +std::array minimum; +std::array, 16> next_character; +std::array witness{}; +std::uint64_t visited = 0; + +void scan(int address, int remaining, int width, int character, + int support, std::uint64_t packed) { + if (address == 16) { + ++visited; + if (full_span[support] && width < minimum[character]) { + minimum[character] = width; + witness[character] = packed; + } + return; + } + scan(address + 1, remaining, width, character, support, packed); + for (int count = 1; count <= remaining; ++count) { + character = next_character[address][character]; + scan(address + 1, remaining - count, width + count, character, + support | (1 << address), + packed | (std::uint64_t(count) << (4 * address))); + } +} +} // namespace + +int main() { + minimum.fill(100); + for (int support = 1; support < 65536; ++support) { + std::array basis{}; + int rank = 0; + for (int x = 0; x < 16; ++x) { + if (!(support & (1 << x))) continue; + int vector = 16 | x; + for (int i = 4; i >= 0; --i) { + if (!(vector & (1 << i))) continue; + if (basis[i]) vector ^= basis[i]; + else { + basis[i] = vector; + ++rank; + break; + } + } + } + full_span[support] = rank == 5; + } + for (int x = 0; x < 16; ++x) { + int pairs = 0, bit = 0; + for (int i = 0; i < 4; ++i) { + for (int j = i + 1; j < 4; ++j, ++bit) { + if ((x & (1 << i)) && (x & (1 << j))) pairs |= 1 << bit; + } + } + for (int character = 0; character < 65536; ++character) { + int r = character & 3; + int low = (character >> 2) & 15; + int high = (character >> 6) & 15; + int cross = character >> 10; + next_character[x][character] = ((r + 1) & 3) | ((low ^ x) << 2) + | ((high ^ (low & x)) << 6) | ((cross ^ pairs) << 10); + } + } + scan(0, limit, 0, 0, 0, 0); + if (visited != 30421755) return 1; + for (int character = 0; character < 65536; ++character) { + if (minimum[character] > limit) return 2; + std::cout << character << ' ' << minimum[character] << ' ' + << witness[character] << '\n'; + } + std::cerr << "PASS_FOUR_AXIS_WITNESS_GENERATION " << visited << '\n'; +} diff --git a/research/four-axis-sharp-cutoff/pack_witnesses.py b/research/four-axis-sharp-cutoff/pack_witnesses.py new file mode 100644 index 0000000000..c9efe54059 --- /dev/null +++ b/research/four-axis-sharp-cutoff/pack_witnesses.py @@ -0,0 +1,13 @@ +"""Pack the optional C++ witness output. Ali Romman with Codex assistance.""" +from pathlib import Path +import gzip +import json +import sys + +rows = [list(map(int, line.split())) for line in Path(sys.argv[1]).read_text().splitlines()] +if len(rows) != 65536 or [row[0] for row in rows] != list(range(65536)): + raise ValueError('Complete ordered character inventory required') +if any(len(row) != 3 or not 0 <= row[2] < 2**64 for row in rows): + raise ValueError('Malformed witness row') +raw = json.dumps([row[2] for row in rows], separators=(',', ':')).encode() +Path(sys.argv[2]).write_bytes(gzip.compress(raw, mtime=0)) diff --git a/research/four-axis-sharp-cutoff/verify.py b/research/four-axis-sharp-cutoff/verify.py new file mode 100644 index 0000000000..e6b4a633f9 --- /dev/null +++ b/research/four-axis-sharp-cutoff/verify.py @@ -0,0 +1,204 @@ +"""Check the sharp four-axis native monomial cutoff. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +Predecessor roles are recorded in PROOF.md and SOURCES.json. +""" +from array import array +from collections import Counter +from hashlib import sha256 +from itertools import product +from pathlib import Path +import gzip +import json +import math +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +THRESHOLDS = (12, 9, 10, 11) +PAIRS = [(i, j) for i in range(4) for j in range(i + 1, 4)] + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def rank(vectors, dimension=4): + basis = [0] * dimension + for x in vectors: + for i in range(dimension - 1, -1, -1): + if (x >> i) & 1: + if basis[i]: + x ^= basis[i] + else: + basis[i] = x + break + return sum(bool(x) for x in basis) + + +def span(vectors): + out = {0} + for x in vectors: + out |= {x ^ y for y in out} + return out + + +def phase(counts): + width = sum(counts) + u = [sum(m for x, m in enumerate(counts) if (x >> i) & 1) % 4 for i in range(4)] + v = [sum(m for x, m in enumerate(counts) if ((x >> i) & 1) and ((x >> j) & 1)) % 2 + for i, j in PAIRS] + return (width % 4 | sum((z % 2) << (i + 2) for i, z in enumerate(u)) + | sum((z // 2) << (i + 6) for i, z in enumerate(u)) + | sum(z << (i + 10) for i, z in enumerate(v))) + + +def check_witness(character, packed): + need(isinstance(packed, int) and 0 <= packed < 2**64, 'Packed witness domain') + counts = [(packed >> (4 * x)) & 15 for x in range(16)] + need(phase(counts) == character, 'Complete literal phase character') + need(rank([16 | x for x, m in enumerate(counts) if m], 5) == 5, 'Full affine span') + need(sum(counts) <= THRESHOLDS[character % 4], 'Character threshold') + return counts + + +def image(columns): + values = [0] + for a in columns: + values += [x ^ a for x in values] + return tuple(values) + + +def order(g): + seen = set() + out = 1 + for x in range(16): + if x in seen: + continue + y, length = x, 0 + while y not in seen: + seen.add(y) + length += 1 + y = g[y] + out = math.lcm(out, length) + return out + + +def group_key(g): + return (order(g), rank([g[1 << i] ^ (1 << i) for i in range(4)]), + rank([g[g[1 << i]] ^ g[1 << i] ^ (1 << i) for i in range(4)])) + + +def group_certificate(coefficients): + columns = [c for c in product(range(16), repeat=4) if rank(c) == 4] + other = [] + for a in range(1, 16): + for b in set(range(16)) - span([a]): + for c in set(range(16)) - span([a, b]): + for d in set(range(16)) - span([a, b, c]): + other.append((a, b, c, d)) + need(len(columns) == 20160 and set(columns) == set(other), 'Two complete GL(4,2) inventories') + maps = [image(c) for c in columns] + weights = [coefficients[group_key(g)] for g in maps] + need(coefficients[group_key(tuple(range(16)))] == 21, 'Nonzero identity coefficient') + types = Counter(group_key(g) for g in maps) + cosets = 0 + for ell in range(1, 16): + plane = [x for x in range(16) if (ell & x).bit_count() % 2 == 0] + basis = [] + for x in plane: + if x not in span(basis): + basis.append(x) + need(len(basis) == 3, 'All linear hyperplanes') + sums, sizes = Counter(), Counter() + for g, a in zip(maps, weights): + key = tuple(g[x] for x in basis) + sums[key] += a + sizes[key] += 1 + need(len(sizes) == 2520 and set(sizes.values()) == {8}, 'Complete stabilizer cosets') + need(not any(sums.values()), 'Every hyperplane coset sum is zero') + cosets += len(sizes) + # A full linear span need not be a full affine span. + points = list(range(8, 16)) + linear_sum = sum(a for g, a in zip(maps, weights) if all(g[x] == x for x in points)) + affine_sum = sum(a for g, a in zip(maps, weights) + if all((g[x] ^ g[8] ^ 8) == x for x in points)) + need(linear_sum == 21 and affine_sum == 0, 'Translation average is necessary') + return cosets, sorted((list(k), v) for k, v in types.items()) + + +def lower_census(): + transitions = [] + for x in range(16): + pairs = sum((((x >> i) & 1) * ((x >> j) & 1)) << k for k, (i, j) in enumerate(PAIRS)) + row = array('H') + for c in range(65536): + p, q, v = (c >> 2) & 15, (c >> 6) & 15, c >> 10 + row.append(((c + 1) & 3) | ((p ^ x) << 2) | ((q ^ (p & x)) << 6) | ((v ^ pairs) << 10)) + transitions.append(row) + full = {} + totals, zeros = Counter(), Counter() + def visit(start, left, character, support, width): + if left == 0: + totals[width] += 1 + if character >> 2 == 0: + zeros[width] += 1 + if support not in full: + full[support] = len(span([16 | x for x in range(16) if support >> x & 1])) == 32 + need(not full[support], 'No low-width zero-phase tuple has full affine span') + return + for x in range(start, 16): + visit(x, left - 1, transitions[x][character], support | (1 << x), width) + for f in range(5, 9): + visit(0, f, 0, 0, f) + need(totals[f] == math.comb(15 + f, 15), 'Complete multiset census') + return dict(sorted(totals.items())), dict(sorted(zeros.items())) + + +def main(): + for pin in json.loads((HERE / 'SOURCES.json').read_text())['files']: + if pin['usage'] == 'input': + need(sha256((ROOT / pin['path']).read_bytes()).hexdigest() == pin['sha256'], 'Source bytes') + data = (HERE / 'WITNESSES.json.gz').read_bytes() + witnesses = json.loads(gzip.decompress(data)) + need(len(witnesses) == 65536, 'All phase characters') + histogram = Counter() + for c, packed in enumerate(witnesses): + histogram[sum(check_witness(c, packed))] += 1 + table = json.loads((HERE / 'COEFFICIENTS.json').read_text()) + coefficients = {tuple(k): v for k, v in zip(table['keys'], table['coefficients'])} + cosets, types = group_certificate(coefficients) + totals, zeros = lower_census() + bad = dict(coefficients) + bad[(2, 1, 4)] += 1 + controls = [lambda: check_witness(1, witnesses[0]), + lambda: check_witness(1024, witnesses[0]), + lambda: check_witness(0, sum(1 << (4 * x) for x in range(8, 16))), + lambda: group_certificate(bad), + lambda: need(21 == 0, 'Omitted translation average fails')] + rejected = 0 + for test in controls: + try: + test() + except ValueError: + rejected += 1 + else: + raise ValueError('Defective fixture accepted') + result = dict(status='PASS_FOUR_AXIS_SHARP_CUTOFF', cutoff=9, + residue_thresholds=list(THRESHOLDS), phase_characters=65536, + witness_sha256=sha256(data).hexdigest(), witness_length_histogram=dict(sorted(histogram.items())), + gl4_elements=20160, class_types=types, hyperplane_cosets=cosets, + lower_multisets=totals, lower_zero_phase_multisets=zeros, + threshold_diagonal_entry=21, rejected_controls=rejected, kappa_change=None) + # JSON normalizes integer dictionary keys for the receipt comparison. + result = json.loads(json.dumps(result)) + if '--write' in sys.argv: + (HERE / 'RESULT.json').write_text(json.dumps(result, indent=2) + '\n') + else: + need(result == json.loads((HERE / 'RESULT.json').read_text()), 'Committed receipt') + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main()