diff --git a/research/conjugate-pair-group-free-audit/PROOF.md b/research/conjugate-pair-group-free-audit/PROOF.md new file mode 100644 index 0000000000..a92cbe6f25 --- /dev/null +++ b/research/conjugate-pair-group-free-audit/PROOF.md @@ -0,0 +1,122 @@ +# A four-call floor that uses only the single labels + +**Scoped written theorem in the formal group-algebra model of #4089 / #6038; no +new κ.** It strengthens the length-three exclusion of +[PR #6038](https://github.com/CrocSwap/integer-mult-bounds/pull/6038) +(`research/conjugate-pair-every-group`, head +`0cee0e104b68ce6f06bf84af03f46ac30680e64c`) and replaces its eight-pattern case +analysis with two cases. + +## Statement + +Let `G` be a group, `F` a field and `r ≥ 2`. Let `a, b ∈ G` be distinct and +both different from `e`, and let + +```text +T = diag([a], [b], [e], …, [e]) ∈ M_r(F[G]). +``` + +A paid call is `D_N(g) = [g] N + N̄` with `N̄ = I - N`, where `N` is a rank-one +idempotent of `M_r(F)` and `g ∈ L` for a label set `L ⊆ G`. + +**Theorem S.** If no label equals `e`, `a` or `b`, then no product of at most +three paid calls equals `T`. This holds for every label set and whatever +coincidences hold among products of labels. + +A call with label `e` is the identity matrix, so `e ∉ L` costs nothing: drop +such calls. The only hypothesis that matters is that no single label equals `a` +or `b`. + +**Corollary (PR6038's length-three step).** Take `L = {x, y}` with `xy ≠ yx`, +`a = xy` and `b = yx`. Then `a ≠ b` and `a, b ≠ e`, and `x, y ∉ {e, xy, yx}` +by cancellation, which is #6038's (F1). Theorem S excludes every word of length +at most three. #6038's facts (F2) and (F3) and its pattern-by-pattern analysis +are not needed. With #6038's four-call direct word, the minimum is four. + +## Proof + +Expand `D_{N_1}(g_1) ⋯ D_{N_k}(g_k) = Σ_U [g_U] P_U` as in #6038, where +`P_U = X_1 ⋯ X_k`, `X_i = N_i` if `i ∈ U` and `N̄_i` otherwise. Group the +subsets by value into three classes: `𝔸 = {U : g_U = a}`, `𝔹 = {U : g_U = b}` +and `𝔼 = {U : g_U = e}`. Since `[w] E_ij` is a basis, the word realizes `T` +only if + +```text +Σ_{U∈𝔸} P_U = E_00, Σ_{U∈𝔹} P_U = E_11, Σ_{U∈𝔼} P_U = T_e := I - E_00 - E_11. +``` + +The proof uses only these three equations. The equations at other group +elements are never used. By hypothesis, `∅ ∈ 𝔼`, and no singleton lies in +`𝔸`, `𝔹` or `𝔼`. + +**k ≤ 2.** `𝔸` and `𝔹` are disjoint and nonempty, because `E_00, E_11 ≠ 0`. +They lie in the subsets of size at least two, and there is at most one such +subset. Contradiction. + +**k = 3.** Write `N_i = u_i v_iᵀ` with `v_iᵀu_i = 1`. Then `𝔸, 𝔹 ⊆ S := +{12, 13, 23, 123}`, and + +```text +P_12 = u_1 (v_1ᵀu_2)(v_2ᵀN̄_3), P_13 = u_1 (v_1ᵀN̄_2u_3) v_3ᵀ, +P_23 = (N̄_1u_2)(v_2ᵀu_3) v_3ᵀ, P_123 = u_1 (v_1ᵀu_2)(v_2ᵀu_3) v_3ᵀ, +P_2 = (N̄_1u_2)(v_2ᵀN̄_3), P_∅ + P_2 = N̄_1 N̄_3. +``` + +Corner rules (as in #6038): `N_1 P_U = P_U` if `1 ∈ U` and `0` otherwise; +`N̄_1 P_U` is the complement. The same holds on the right with `N_3` and +position 3. + +*Step 1: `23 ∈ 𝔸 ∪ 𝔹` and `12 ∈ 𝔸 ∪ 𝔹`.* Every `P_U` with `U ∈ S \ {23}` +has column space in `span(u_1)`. If neither `𝔸` nor `𝔹` contained `23`, then +`E_00` and `E_11` would both have column space in `span(u_1)`. Then `u_1` would +be parallel to both `e_0` and `e_1`, which is impossible. The same argument +with row spaces and `v_3ᵀ` gives `12`. So the cases are (up to the symmetry +below): (1) `12, 23 ∈ 𝔸`, or (2) `23 ∈ 𝔸` and `12 ∈ 𝔹`. + +*Symmetry.* Exchanging `a ↔ b` together with the coordinates `0 ↔ 1` +(conjugation by a permutation matrix maps rank-one idempotents to rank-one +idempotents) exchanges `𝔸` and `𝔹`. The hypotheses are symmetric, so the +other two placements reduce to these. + +*Case 1: `12, 23 ∈ 𝔸`.* Then `𝔹 ⊆ {13, 123}`, so `E_11` is a multiple of +`u_1 v_3ᵀ`, and `u_1 ∥ e_1`, `v_3 ∥ e_1`. Within `S`, only `12` omits position +3, so `E_00 N̄_3 = P_12`. The left side has column space in `span(e_0)`. The +right side has column space in `span(u_1) = span(e_1)`. So `P_12 = 0`. +Likewise only `23` omits position 1, so `N̄_1 E_00 = P_23`. The left side has +row space `span(e_0ᵀ)` and the right side has row space `span(v_3ᵀ) = +span(e_1ᵀ)`, so `P_23 = 0`. Then `E_00 = N_1 E_00 N_3`, a multiple of +`u_1 v_3ᵀ ∥ e_1 e_1ᵀ`. Contradiction. + +*Case 2: `23 ∈ 𝔸`, `12 ∈ 𝔹`.* `𝔸` omits `12`, so every member of `𝔸` +contains position 3. Hence `E_00 N̄_3 = 0`, and `E_00` has row space in +`span(v_3ᵀ)`, so `v_3 ∥ e_0`. `𝔹` omits `23`, so every member contains +position 1. Hence `N̄_1 E_11 = 0` and `u_1 ∥ e_1`. + +* `P_12 ≠ 0`: within `𝔹` only `12` omits position 3, so `E_11 N̄_3 = P_12`. + If this were zero, `E_11 = E_11 N_3` would be a multiple of + `e_1 v_3ᵀ ∥ e_1 e_0ᵀ`, which is false. +* `P_23 ≠ 0`: within `𝔸` only `23` omits position 1, so `N̄_1 E_00 = P_23`. + If this were zero, `E_00 = N_1 E_00` would be a multiple of + `u_1 e_0ᵀ ∥ e_1 e_0ᵀ`, which is false. +* Hence `v_2ᵀN̄_3 ≠ 0` and `N̄_1 u_2 ≠ 0`, so `P_2 ≠ 0`. +* The corner `(N̄_1, N̄_3)` keeps `∅` and `{2}`. Only `∅` lies in `𝔼`, so + `P_∅ = N̄_1 T_e N̄_3 = N̄_1 N̄_3 - N̄_1 E_00 N̄_3 - N̄_1 E_11 N̄_3 = N̄_1 N̄_3`, + using `E_00 N̄_3 = 0` and `N̄_1 E_11 = 0`. With `P_∅ + P_2 = N̄_1 N̄_3`, + this gives `P_2 = 0`. Contradiction. ∎ + +## What is used + +The proof uses three things: the three class equations, `∅ ∈ 𝔼`, and the +fact that no singleton is in a target class. It uses no element of `L`, no +relation among labels, no field characteristic and no width beyond `r ≥ 2`. +It does not use the equations at the other group elements; dropping them only +enlarges the set of systems excluded. The verifier's `singleton` tier searches +exactly this relaxed system over small prime fields and widths and finds no +solution. Its controls show the search is not vacuous: it finds four-call +solutions, and a single label allowed to equal `xy` reopens length three. + +## Scope + +This is a statement in the formal group-algebra model. It prices no native +address operation, conversion, restoration or caller and changes no κ. No +proof-kernel check and no independent human review is claimed. diff --git a/research/conjugate-pair-group-free-audit/README.md b/research/conjugate-pair-group-free-audit/README.md new file mode 100644 index 0000000000..c0ae47bf6c --- /dev/null +++ b/research/conjugate-pair-group-free-audit/README.md @@ -0,0 +1,153 @@ +# Independent audit of #6038: a group-free four-call floor + +**Independent proof audit, a stronger written theorem and a group-free finite +certificate. No new κ.** This package is by Josie Elliston, with substantial +Claude (Anthropic) assistance. New work is Apache-2.0. + +Subject: Nick Petalas's [PR #6038](https://github.com/CrocSwap/integer-mult-bounds/pull/6038) +(`research/conjugate-pair-every-group`) at exact head +`0cee0e104b68ce6f06bf84af03f46ac30680e64c`. In the rank-one-idempotent +register model of Wentao Li's +[#4089](https://github.com/CrocSwap/integer-mult-bounds/pull/4089), #6038 claims +that `diag([xy],[yx],[e],…,[e])` needs exactly four paid calls, for every group, +field and width `r ≥ 2`. The package does not read #6038's files and imports no +code from #6038 or #4089. + +## Results + +**1. Audit of #6038's PROOF.md: no error found.** I checked each step against +the model. The model and factor form match #4089's `research/a5-conjugate-any-registers/PROOF.md` +over `F2`. I checked the facts (F1)-(F3) by cancellation, the corner +identities, Lemmas 1-3 and all eight length-three patterns. For `xxy`, `yyx`, +`xyy` and `yxx` I also checked that no other subset can take the value `xy` or +`yx`. Two remarks, neither affecting correctness: + +* The last clause of (F3), "`x³, y³` cannot both equal `xy` and `yx`", is + weaker than the truth. `x³` equals neither, since `x³ = xy` or `x³ = yx` + gives `y = x²`. The weaker clause is enough for the `xxx` pattern. +* In the `xyx` case the "corner split and Lemma 2" are unnecessary. + `T_xy = P_12` follows directly, because `{1,2}` is the only subset with value + `xy`. + +An OpenAI Codex read-only adversarial review of the same PROOF.md and of this +verifier also reported no error. A second Codex review of this package's +Theorem S proof reported no error either. These are machine checks, not human +review. + +**2. A stronger theorem with a shorter proof ([PROOF.md](PROOF.md)).** Fix +distinct `a, b ≠ e` and the target `diag([a],[b],[e],…,[e])`. If no label +equals `a` or `b`, no product of at most three paid calls reaches the target. +This holds for every label set, every coincidence among products of labels, +every field and every `r ≥ 2`. The proof uses only the coefficient equations at +`a`, `b` and `e`. It has two cases and needs neither #6038's facts (F2)/(F3) nor +its eight-pattern analysis. #6038's length-three step is the special case +`L = {x, y}`, `a = xy`, `b = yx`. + +**3. A group-free finite certificate ([verify.py](verify.py)).** #6038's +finite check covers 26 coincidence keys collected from S3, S4, S5, Q8 and the +free group. This check instead lets each subset word `g_U` of a length 0-3 word +over `{x, y}` take any class in `{e, xy, yx, other}` that the single equation +`g_U = class` allows when `xy ≠ yx`. Each of the 90 equations is decided by an +exact rule: + +* *allowed*: an explicit noncommuting witness pair in S3, S4 or S5 (38 + equations); +* *forbidden*: after cyclic free reduction of `g_U · class⁻¹`, one generator + occurs exactly once, or the relator is a cyclic conjugate of `[x,y]^{±1}`. + Either way `xy = yx` would follow (52 equations). + +The verifier fails if any equation is undecided. The search drops joint +consistency and the zero equations at "other" elements. Its feasible set +therefore contains the labeling of every actual group. It searches every tuple +of rank-one idempotents in two tiers. The *full* tier uses the table above. +The *singleton* tier constrains only the single letters, exactly as in +Theorem S. + +| width r | field | tuples at k = 3 | full tier | singleton tier | +|---:|---:|---:|---|---| +| 2 | F2 | 216 | no solution | no solution | +| 2 | F3 | 1,728 | no solution | no solution | +| 2 | F5 | 27,000 | no solution | no solution | +| 3 | F2 | 21,952 | no solution | no solution | +| 2 | F7 | 175,616 | no solution | no solution (local run, 87 s) | +| 3 | F3 | 1,601,613 | no solution | no solution (local run, 1,124 s) | + +The first four rows are registered. The last two are local runs of the same +verifier (`--cases 2:7`, `--cases 3:3`). Lengths 0, 1 and 2 are also excluded +in every row. A local `--cases 4:2` run hit its 1,500 s timeout before +finishing and is not claimed. + +Controls, all registered: + +* the direct word `D_{E00}(x) D_{E00}(y) D_{E11}(y) D_{E11}(x)` satisfies the + relaxation, and the search finds a length-four solution by itself; +* with every nonempty subset allowed in any class (pure linear algebra), a + length-two word fits; +* wrongly allowing one single label to equal `xy` (`y = xy`) reopens length + three (pattern `yxy`). + +The search confirms that the single-label facts are the essential ones. In a +local exploratory run at `r = 2` over `F2` (not registered), I flipped each of +the 32 forbidden equations with words of length at most three, one at a time. +Only the four that put `x` or `y` in the `xy` or `yx` class reopened a short +word. + +## What this does not cover + +* The finite tiers cover only prime fields at the sizes in the table. Prime-power + fields such as F4 and widths `r ≥ 4` rely on the written proofs. +* Neither proof addresses native address operations, conversion, restoration, + a caller or any BIT supplier. The selected κ (#6030) is unchanged. +* No independent human or proof-kernel review is claimed. + +## Reproduce + +From the repository root, standard-library CPython 3.12: + +```sh +python3.12 -B -W error research/conjugate-pair-group-free-audit/verify.py +python3.12 -O -B -W error research/conjugate-pair-group-free-audit/verify.py +python3.12 -B research/conjugate-pair-group-free-audit/verify.py --cases 2:7 # optional, about 90 s +python3.12 -B research/conjugate-pair-group-free-audit/verify.py --cases 3:3 # optional, about 19 min +python3.12 -B scripts/research_package.py --package research/conjugate-pair-group-free-audit +``` + +Expected marker: `PASS_CONJUGATE_PAIR_GROUP_FREE_AUDIT`, in about 30 s per mode. + +## Open next questions + +1. **Longer diagonal pair targets (#6038 open question 1).** Theorem S is a + uniform floor of 4 for any pair target whose entries are not labels. Is + there a uniform floor of 6 for `diag([g],[h])` when neither entry is a + product of at most two labels, for example `diag([xyx],[yxy])`? *Why:* it + would replace per-group pair censuses with one argument. *What fails + already (local probe, not registered):* the support-only analogue of + Theorem S does not hold. I kept `∅` in the `e` class, kept the singletons out + of all three classes and let only subsets of size at least three carry `g` + or `h`. A NumPy subset-sum search at `r = 2` over `F2` then finds solutions + at length 4 (20 of 1,296 idempotent tuples) and at length 5 (938 of + 7,776). The control with threshold two reproduces Theorem S: no solution + up to length 3, and 264 at length 4. So a floor of 6, if true, must use + relations among the labels, not just support sizes. A second local probe + (stdlib, not registered) solves the exact equations in the free group on + `x, y`: no word of length at most 5 reaches `diag([xyx],[yxy])` at `r = 2` + over `F2`. The same code finds the four-call words for `(xy, yx)`. A + free-group solution would map to every group, so any saving below 6 needs + a relation among the labels. *First step:* use this + package's full tier for the labels `{x, y}` and the target `(xyx, yxy)`. + That needs sound rules for when a single equation forces `xyx = yxy`; the + commutation rule used here does not imply that. Then check whether the + length-4 relaxed solutions survive. *Blocker:* the consistency rules + for the new hypothesis. +2. **Formalization.** Theorem S involves only rank-one matrices over a field + and suits a proof assistant. No Lean build was attempted. + +## Credit + +Nick Petalas (#6038) supplied the all-group theorem, the corner-sandwich +method, the expansion and the direct word that this package audits and builds +on. Wentao Li (#4089, #4093) supplied the model and the A5 and PSL(2,7) +results; Cinna Davis (#2246) supplied the original A5 target. Their cited +statements were not re-audited beyond what is described above. Theorem S, its +two-case proof, the group-free relaxation and the verifier are new here. +Source pins are in [SOURCES.json](SOURCES.json). diff --git a/research/conjugate-pair-group-free-audit/SOURCES.json b/research/conjugate-pair-group-free-audit/SOURCES.json new file mode 100644 index 0000000000..508b3dd13b --- /dev/null +++ b/research/conjugate-pair-group-free-audit/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/a5-conjugate-any-registers/PROOF.md", + "usage": "provenance", + "git_blob": "a72b89bdd2428b78c6424d2d2299bdb1ac2981d3", + "sha256": "921a84d24148d27932aad24a9a5d74bd235de0c1b2f27c2b9bfc5d37fcf51dcf" + } + ] +} diff --git a/research/conjugate-pair-group-free-audit/TASK.json b/research/conjugate-pair-group-free-audit/TASK.json new file mode 100644 index 0000000000..da8df950f9 --- /dev/null +++ b/research/conjugate-pair-group-free-audit/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "Independent audit of Nick Petalas's PR #6038 (research/conjugate-pair-every-group, head 0cee0e104b68ce6f06bf84af03f46ac30680e64c): line-by-line check of its written all-group four-call theorem; a stronger written theorem (Theorem S: any label set avoiding the two target entries, any coincidences, any field, r >= 2) with a two-case proof; and a group-free finite certificate over small prime fields and widths.", + "scope_change_reason": "The chooser drew independent-verification. independent-moment on the selected #6030 word already has two audits (maintainer review and #6043), and no open PR claims a higher kappa. #6038 is a fresh unreviewed all-group theorem that answers #4089's open question 2. Its finite check depends on coincidence keys from five named groups. An independent proof check plus a check free of group-specific inputs is the missing implication for that claim. formal-interface-lemma is the closest card: this binds a theorem to a certificate, without a proof-assistant build.", + "bottleneck_link": "Side result for the BIT register-model line. It confirms that the conjugate-pair alphabet offers no call saving in any group. Theorem S extends this to every label set that avoids the target entries, so a nonabelian-alphabet BIT proposal must find its gain elsewhere. No kappa effect.", + "budget_minutes": 60, + "stop_rule": "Stop at the first error in #6038's proof or the first relaxed solution at length <= 3; otherwise stop after the written strengthening and the registered finite tiers.", + "outcome": "completed", + "evidence": "PROOF.md (Theorem S, two-case proof); README audit notes on #6038 PROOF.md; verify.py, a stdlib group-free relaxation over r,q = (2,2),(2,3),(2,5),(3,2) with full and singleton tiers and positive/negative controls; local run at (2,7).", + "author": "Josie Elliston", + "ai_assistance": "Claude (Anthropic) assisted with the audit, the proof, the code and the writing. An OpenAI Codex read-only adversarial review of #6038's PROOF.md and of verify.py reported no error.", + "open_questions": [ + { + "question": "Is there a uniform floor of 6 calls for diag([g],[h]) when neither entry is a product of at most two labels, e.g. diag([xyx],[yxy])? (#6038 open question 1)", + "why_it_matters": "It would replace per-group pair censuses with one uniform argument.", + "first_step": "The support-only analogue of Theorem S fails. A local probe at r=2 over F2, with only size>=3 subsets allowed to carry g or h, finds relaxed solutions at length 4 (20/1296 tuples) and 5 (938/7776). Next, add the label relations: a full-tier table for labels {x,y} and target (xyx, yxy), then test whether those length-4 solutions survive.", + "blocked_by": "Sound single-equation rules for the hypothesis xyx != yxy; the commutation rule used here does not imply it." + }, + { + "question": "Formalize Theorem S in a proof assistant.", + "why_it_matters": "It is a short statement about rank-one matrices over a field and would give a kernel-checked floor.", + "first_step": "State the three class equations and the corner rules for k = 3 over an arbitrary field.", + "blocked_by": "No Lean build was attempted; it needs a separate proof-assistant budget." + } + ] +} diff --git a/research/conjugate-pair-group-free-audit/VERIFY.json b/research/conjugate-pair-group-free-audit/VERIFY.json new file mode 100644 index 0000000000..9a6f5df2f2 --- /dev/null +++ b/research/conjugate-pair-group-free-audit/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/a5-conjugate-any-registers/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Group-free relaxation excludes every word of length 0..3 at widths/fields (r,q) = (2,2),(2,3),(2,5),(3,2) under both the full single-equation consistency table and the singleton-only table; every one of 90 equations decided by an S3/S4/S5 witness or a sound cancellation rule; positive controls: direct four-call word and an independent length-4 hit; failure controls: unrestricted linear algebra fits at length 2, one wrong singleton bit reopens length 3." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same checks under python -O. Every check raises SystemExit explicitly (no assert statements), so -O skips nothing." + } + ] +} diff --git a/research/conjugate-pair-group-free-audit/verify.py b/research/conjugate-pair-group-free-audit/verify.py new file mode 100644 index 0000000000..fa9bc7931d --- /dev/null +++ b/research/conjugate-pair-group-free-audit/verify.py @@ -0,0 +1,356 @@ +#!/usr/bin/env python3 +"""Group-free independent check of the PR6038 conjugate-pair four-call floor. + +Standard library only. Imports nothing from PR6038 or #4089. + +Model (PR6038 / #4089): paid factor D_N(g) = [g] N + (I - N), g in {x, y}, +N a rank-one idempotent of M_r(F_q); target T = diag([xy], [yx], [e], ..., [e]). +A word D_{N_1}(g_1) ... D_{N_k}(g_k) expands as sum_U [g_U] P_U. + +Relaxation (the point of this check): instead of fixing a group, each subset +word g_U may be put in any class among {e, xy, yx, other} that is *individually* +consistent with xy != yx. Joint consistency of several coincidences, and the +requirement that every "other" group element gets coefficient zero separately, +are dropped. Every actual group G and pair x, y with xy != yx therefore gives +one of the allowed labelings, so infeasibility of the relaxation for a field +and width excludes the word for *every* group at once. + +Consistency of a single equation g_U = c is decided by exact rules only: + * consistent -> an explicit noncommuting witness pair in S3, S4 or S5; + * inconsistent -> after cyclic free reduction of g_U c^-1, either one + generator occurs exactly once (so it lies in the cyclic + group of the other and the pair commutes), or the relator + is a cyclic conjugate of the commutator [x, y]^(+-1). +Any equation decided by neither rule makes the verifier fail. + +Two tiers are searched. "full" uses the table above. "singleton" keeps only +the facts about single letters (x, y not in {e, xy, yx}) and lets every subset +of size >= 2 join any class; this is exactly the relaxed system of Theorem S +in PROOF.md. +""" + +from __future__ import annotations + +import argparse +import itertools +import sys +import time + +MARKER = "PASS_CONJUGATE_PAIR_GROUP_FREE_AUDIT" + +def require(cond, msg): + """Explicit check that also runs under python -O.""" + if not cond: + raise SystemExit(f"FAIL {msg}") + + +# ---------------------------------------------------------------- free words +INV = {"x": "X", "X": "x", "y": "Y", "Y": "y"} + + +def free_reduce(word: str) -> str: + out: list[str] = [] + for ch in word: + if out and out[-1] == INV[ch]: + out.pop() + else: + out.append(ch) + return "".join(out) + + +def cyclic_reduce(word: str) -> str: + w = free_reduce(word) + while len(w) >= 2 and w[0] == INV[w[-1]]: + w = w[1:-1] + return w + + +def inverse(word: str) -> str: + return "".join(INV[ch] for ch in reversed(word)) + + +def forces_commutation(relator: str) -> bool: + """Sound sufficient test: some generator occurs exactly once cyclically.""" + w = cyclic_reduce(relator) + if w == "": + return False # trivial relation, no information + commutators = {c[i:] + c[:i] for c in ("xyXY", "yxYX") for i in range(4)} + if w in commutators: + return True # the relation is xy = yx itself + for gen in "xy": + if sum(ch in (gen, INV[gen]) for ch in w) == 1: + return True + return False + + +# ------------------------------------------------------- permutation witnesses +def perm_mul(p, q): + """Composition (p*q)[i] = p[q[i]]. Any fixed associative convention gives a + group, and only equalities of word values are tested.""" + return tuple(p[i] for i in q) + + +def perm_inv(p): + inv = [0] * len(p) + for i, pi in enumerate(p): + inv[pi] = i + return tuple(inv) + + +def evaluate(word: str, x, y): + ident = tuple(range(len(x))) + table = {"x": x, "y": y, "X": perm_inv(x), "Y": perm_inv(y)} + acc = ident + for ch in word: + acc = perm_mul(acc, table[ch]) + return acc + + +def witness_pairs(): + for n in (3, 4, 5): + elems = list(itertools.permutations(range(n))) + for x in elems: + for y in elems: + if perm_mul(x, y) != perm_mul(y, x): + yield n, x, y + + +TARGET_WORDS = {"E": "", "XY": "xy", "YX": "yx"} + + +def classify_equations(words: list[str]): + """Return {(word, cls): bool consistent} and evidence counts.""" + pending = {(w, c) for w in words for c in TARGET_WORDS} + result: dict[tuple[str, str], bool] = {} + evidence = {"witness": 0, "forced_commutation": 0} + for (w, c) in list(pending): + if forces_commutation(w + inverse(TARGET_WORDS[c])): + result[(w, c)] = False + evidence["forced_commutation"] += 1 + pending.discard((w, c)) + for _n, x, y in witness_pairs(): + if not pending: + break + for (w, c) in list(pending): + if evaluate(w, x, y) == evaluate(TARGET_WORDS[c], x, y): + result[(w, c)] = True + evidence["witness"] += 1 + pending.discard((w, c)) + if pending: + raise SystemExit(f"FAIL undecided equations: {sorted(pending)}") + return result, evidence + + +# ------------------------------------------------------------- field algebra +def mat_mul(a, b, q): + r = len(a) + return tuple( + tuple(sum(a[i][t] * b[t][j] for t in range(r)) % q for j in range(r)) + for i in range(r) + ) + + +def mat_add(a, b, q): + return tuple(tuple((u + v) % q for u, v in zip(ra, rb)) for ra, rb in zip(a, b)) + + +def identity(r): + return tuple(tuple(1 if i == j else 0 for j in range(r)) for i in range(r)) + + +def zero(r): + return tuple(tuple(0 for _ in range(r)) for _ in range(r)) + + +def unit(r, a): + return tuple(tuple(1 if i == j == a else 0 for j in range(r)) for i in range(r)) + + +def rank_one_idempotents(r, q): + out = set() + vecs = [v for v in itertools.product(range(q), repeat=r) if any(v)] + for u in vecs: + for v in vecs: + if sum(a * b for a, b in zip(u, v)) % q == 1: + out.add(tuple(tuple(ui * vj % q for vj in v) for ui in u)) + return sorted(out) + + +def subset_products(ns, q, r): + """P_U for every U (bitmask over positions 0..k-1), chronological order.""" + ident = identity(r) + bars = [tuple(tuple((ident[i][j] - n[i][j]) % q for j in range(r)) for i in range(r)) for n in ns] + k = len(ns) + level = {0: ident} + for pos in range(k): + nxt = {} + for mask, m in level.items(): + nxt[mask | (1 << pos)] = mat_mul(m, ns[pos], q) + nxt[mask] = mat_mul(m, bars[pos], q) + level = nxt + return level + + +# ------------------------------------------------------------ the relaxation +def label_word(pattern: str, mask: int) -> str: + return "".join(ch for i, ch in enumerate(pattern) if mask >> i & 1) + + +def allowed_labels(pattern: str, consistent): + k = len(pattern) + allowed = {} + for mask in range(1 << k): + w = label_word(pattern, mask) + if mask == 0: + allowed[mask] = {"E"} # the empty subset has value e + else: + allowed[mask] = {c for c in TARGET_WORDS if consistent[(w, c)]} + return allowed + + +def sub_masks(items): + for n in range(len(items) + 1): + for combo in itertools.combinations(items, n): + yield combo + + +def relaxed_feasible(prods, allowed, r, q, everything_allowed=False): + t_xy = unit(r, 0) + t_yx = unit(r, 1) + t_e = identity(r) + t_e = tuple(tuple((t_e[i][j] - t_xy[i][j] - t_yx[i][j]) % q for j in range(r)) for i in range(r)) + masks = list(prods) + z = zero(r) + + def candidates(cls, target, forced=()): + pool = [m for m in masks if m not in forced and (everything_allowed and m != 0 or cls in allowed[m])] + if cls == "E": + pool = [m for m in pool if m != 0] + hits = [] + for combo in sub_masks(pool): + s = z + for m in forced: + s = mat_add(s, prods[m], q) + for m in combo: + s = mat_add(s, prods[m], q) + if s == target: + hits.append(frozenset(combo) | frozenset(forced)) + return hits + + xy_sets = candidates("XY", t_xy) + if not xy_sets: + return None + yx_sets = candidates("YX", t_yx) + if not yx_sets: + return None + e_sets = candidates("E", t_e, forced=(0,)) + for a in xy_sets: + for b in yx_sets: + if a & b: + continue + for c in e_sets: + if not (c & a) and not (c & b): + return (a, b, c) + return None + + +def run_case(k, r, q, consistent, everything_allowed=False, stop_at_first=True): + idem = rank_one_idempotents(r, q) + patterns = ["".join(p) for p in itertools.product("xy", repeat=k)] + allowed = {p: allowed_labels(p, consistent) for p in patterns} + found = [] + tuples = 0 + for ns in itertools.product(idem, repeat=k): + tuples += 1 + prods = subset_products(ns, q, r) + for p in patterns: + hit = relaxed_feasible(prods, allowed[p], r, q, everything_allowed) + if hit is not None: + found.append((p, ns, hit)) + if stop_at_first: + return len(idem), tuples, found + return len(idem), tuples, found + + +def main(argv=None): + ap = argparse.ArgumentParser() + ap.add_argument("--cases", default="2:2,2:3,2:5,3:2", + help="comma list r:q of width:prime for the length<=3 exclusion") + args = ap.parse_args(argv) + t0 = time.time() + + # all positive subwords of words of length <= 4 over {x, y} + words = sorted({label_word("".join(p), m) + for k in range(5) for p in itertools.product("xy", repeat=k) + for m in range(1, 1 << k)}) + consistent, evidence = classify_equations(words) + + # spot-check the rules against facts that are known independently + must_be_false = [("x", "E"), ("x", "XY"), ("xx", "XY"), ("yy", "YX"), ("xxx", "XY"), + ("xxy", "XY"), ("xyx", "XY"), ("xyx", "YX"), ("xy", "YX")] + must_be_true = [("xx", "E"), ("xxy", "YX"), ("yyx", "XY"), ("xyy", "YX"), ("yxx", "XY"), + ("xxx", "E"), ("xy", "XY")] + for key in must_be_false: + require(consistent[key] is False, f"expected inconsistent {key}") + for key in must_be_true: + require(consistent[key] is True, f"expected consistent {key}") + # x^3 can equal neither xy nor yx (y would be x^2); PR6038's (F3) states a weaker form + require(not consistent[("xxx", "XY")] and not consistent[("xxx", "YX")], "x^3 rule") + + # singleton-only table: keep only the facts that a single label x or y + # is not e, xy or yx; every subset of size >= 2 may join any class. + singleton_only = {key: (val if len(key[0]) <= 1 else True) for key, val in consistent.items()} + + summary = [] + for spec in args.cases.split(","): + r, q = (int(s) for s in spec.split(":")) + for k in range(0, 4): + for name, table in (("full", consistent), ("singleton", singleton_only)): + n_idem, tuples, found = run_case(k, r, q, table) + if found: + raise SystemExit(f"FAIL length {k} {name} relaxed solution at r={r} q={q}: {found[0]}") + summary.append(f"r{r}q{q}k{k}:{tuples}") + + # positive control 1: the direct four-call word satisfies the relaxation + r, q = 2, 2 + e00, e11 = unit(r, 0), unit(r, 1) + pattern = "xyyx" + prods = subset_products((e00, e00, e11, e11), q, r) + require(relaxed_feasible(prods, allowed_labels(pattern, consistent), r, q) is not None, "direct word") + # and the search finds length-4 solutions on its own + _, _, found4 = run_case(4, 2, 2, consistent) + require(found4, "length-4 search found nothing") + + # control 2: without the group-theoretic labels (pure linear algebra, + # every nonempty subset may join any class) some length <= 3 word fits, + # so the exclusion above really uses the support facts. + control_k = None + for k in range(1, 4): + _, _, f = run_case(k, 2, 2, consistent, everything_allowed=True) + if f: + control_k = k + break + require(control_k is not None, "unrestricted control found no short solution") + + # control 3: one wrong consistency bit (allow y = xy, which forces x = e) + # must reopen a length <= 3 word at r=2, q=2. + bad = dict(consistent) + bad[("y", "XY")] = True + reopened = None + for k in range(1, 4): + _, _, f = run_case(k, 2, 2, bad) + if f: + reopened = (k, f[0][0]) + break + require(reopened is not None, "mutated consistency table did not reopen") + + n_true = sum(consistent.values()) + print(f"{MARKER} equations={len(consistent)} consistent={n_true} " + f"witnessed={evidence['witness']} forced={evidence['forced_commutation']} " + f"cases={' '.join(summary)} length4_found=1 unrestricted_control_k={control_k} " + f"mutated_reopens={reopened[0]}:{reopened[1]} seconds={time.time() - t0:.1f}") + return 0 + + +if __name__ == "__main__": + sys.exit(main())