diff --git a/research/semilinear-two-normal-prices/PROOF.md b/research/semilinear-two-normal-prices/PROOF.md new file mode 100644 index 0000000000..ec579d6869 --- /dev/null +++ b/research/semilinear-two-normal-prices/PROOF.md @@ -0,0 +1,169 @@ +# Exact weighted price for two normal targets + +This is a scoped written proof. It answers the two-target first experiment +in Open next question 1 of Krzysztof Wojt's PR5242. The earlier unit-price +semilinear theorem, scalar normalization and natural representation retain +their predecessor credit. The new contribution is the quotient-loop rigidity, +including repeated labels, and its weighted tariff consequence. Josie Elliston / PR6048 +already excludes three calls for distinct pair targets in every group when +no paid label is a target. Its distinct-target floor is credited rather than +claimed as new here. The proof below does not need that predecessor as an +assumption; it also covers the repeated-label case excluded there. + +## Contract + +Let p be any odd prime, F = F_(2^p), and G = F* semidirect C_p, with + + (a,j)(b,k) = (a b^(2^j), j+k mod p). + +Work in Mat_r(F2[G]) for any finite r >= 2. All roles start independently +arbitrary. A paid call is D_P(g) = I + P tensor ([g]+[1]), where g != 1 +and P = u v^T is a binary rank-one idempotent, v^T u = 1. Free operations +are arbitrary GL_r(F2) scalar maps. The exact full formal endpoint is + + diag([h_1], [h_2], [1], ..., [1]), + +where h_1 and h_2 are nonidentity normal elements, meaning (a,0), a != 1. +Repeated labels are allowed. Thus every other dirty role must be restored. +A normal call costs a > 0 and an outside call costs b > 0, uniformly within +each type. There are no other free address maps or higher-rank paid calls. + +**Theorem.** The exact minimum price is 2 min(a, 2b). +In particular, the minimum number of outside-only calls is four. +The prices are arbitrary positive real numbers. They are formal complete +per-call prices within this contract, not a claimed physical supplier bill. + +## A three-factor quotient lemma + +Let K be any extension of F2. For i = 1,2,3 let P_i be binary rank-one +idempotents and let lambda_i be nonzero elements of K different from 1. +Set A_i = I + (lambda_i+1) P_i. Then + + A_3 A_2 A_1 = I implies P_1 = P_2 = P_3. + +It also implies lambda_1 lambda_2 lambda_3 = 1. + +Write P_i = u_i v_i^T with binary vectors and v_i^T u_i = 1. +Since A_3 is invertible, + + A_2 A_1 - I = (lambda_3^(-1)+1) P_3 + +has rank one. Put c_i = lambda_i+1 != 0. Direct multiplication gives + + A_2 A_1 - I = c_1 u_1 v_1^T + c_2 u_2 v_2^T + + c_1 c_2 (v_2^T u_1) u_2 v_1^T. + +If both the two columns u_1,u_2 and the two rows v_1,v_2 are independent, +this expression factors as a full-column-rank matrix, an invertible 2 by 2 +triangular matrix with diagonal c_1,c_2, and a full-row-rank matrix. +Its rank is two, a contradiction. Consequently either u_1=u_2 or v_1=v_2. +Nonzero binary vectors that are proportional over K are equal. + +Suppose u_1=u_2=u. If v_1 != v_2, the product difference is + + u (lambda_2 c_1 v_1^T + c_2 v_2^T). + +Both row coefficients are nonzero. Its column space is Ku, so the binary +column in P_3 must be u. Also + + span_K(v_1,v_2) intersect F2^r = span_F2(v_1,v_2). + +For completeness, binary independent rows admit binary coordinate duals; +applying these to a binary vector in their K-span recovers binary +coefficients. The only possible nonzero v_3 are v_1, v_2 and v_1+v_2. +The first two are excluded because both displayed coefficients are nonzero. +The last satisfies (v_1+v_2)^T u = 0, contradicting idempotence of P_3. +Therefore v_1=v_2. The common-row case follows by transposing the two-factor +product and using the same argument in reversed order. Thus P_1=P_2. +Their product is I+(lambda_1 lambda_2+1)P_1. It cannot be I because +A_3 != I. Comparison with A_3^(-1) yields P_3=P_1 and the scalar identity. +This proves the lemma for every finite r, without a dimension census. + +The binary restriction matters. Over F4, let w^2+w+1=0 and use common +column e_1 with rows (1,0), (1,1), (1,w). All three projectors are +idempotent and different. Taking lambda_i=w gives A_3 A_2 A_1=I. +The verifier checks this boundary exactly. It is outside the contract. + +## Three outside calls cannot deliver the two normal targets + +Move all free scalar maps to the right using + + S D_P(g) = D_(S P S^(-1))(g) S. + +Augmentation [g] -> 1 sends every paid factor and the required target to I, +so the remaining free scalar product is I. Normalization preserves binary +rank-one idempotence, labels and prices. This is PR5242's normalization. + +Choose a characteristic-two extension K containing a primitive p-th root +zeta. The quotient character chi(a,j)=zeta^j extends to the group algebra. +Every outside label has chi(g) != 1 and every normal target has character 1. +Thus a hypothetical three-outside-call word gives A_3 A_2 A_1=I in this +representation. The lemma forces all three normalized projectors to be P. +In the full formal algebra, their product then equals D_P(g_3 g_2 g_1). +This equality follows from P^2=P and (I-P)P=P(I-P)=0; no commutation of +the group labels is assumed. + +A single such projector cannot equal the two-target endpoint. Define a +binary linear functional ell on F2[G] that sends [1] to zero and both +[h_1] and [h_2] to one. This is well-defined even when h_1=h_2, since the +normal targets are nonidentity basis labels. Apply ell entry by entry to +the difference from I. The target gives diag(1,1,0,...,0), of rank two. +D_P(g_3 g_2 g_1)-I gives a scalar multiple of P, of rank at most one. +This contradiction proves the new obstruction, including arbitrary +restored dirty workspace. + +## Lower bound for arbitrary mixtures and prices + +Use the natural representation rho(a,j)(z)=a z^(2^j) on F. PR5242 proves +its displacement rank is p on normal labels and p-1 on outside labels. +Rank telescoping therefore gives, for N normal and O outside calls, + + p N + (p-1) O >= 2p. + +This cited premise is used without replaying the predecessor theorem. +If N >= 2, the price is at least 2a. If N=1, the inequality excludes O<=1, +so the price is at least a+2b. If N=0, it excludes O<=2, and the new +three-call obstruction excludes O=3. The price is then at least 4b. +Every legal word consequently costs at least + + min(2a, a+2b, 4b) = 2 min(a,2b). + +This is a case split over all possible call counts, not a bounded search. + +## Attainment + +One coordinate normal call on each of the two target roles costs 2a. +Every nonidentity normal element h=(c,0) factors as + + h = (c,-1) (1,1). + +Both factors are outside because p is odd. Applying the two corresponding +calls successively on the same coordinate projector gives D_(E_ii)(h). +Doing this on each target role costs 4b, restores every other role, and +attains the full formal endpoint. Replacing only one role gives the +intermediate price a+2b. Choosing the cheaper endpoint price proves the +theorem. The attaining words use no clean workspace. + +## Limits and credit + +The all-prime and all-workspace quantifiers rest on this written proof. +Finite checks corroborate the new quotient lemma and attaining words. +They are not independent human review or formal proof-kernel acceptance. +Three or more normal targets, mixed target lists, arbitrary per-label +prices, nonbinary free mixing and higher-rank paid calls remain outside +this theorem. No universal optimum for all semilinear target lists is claimed. + +Native realization, physical movement, ownership, restoration implementation, +precision, stock/compiler, recursive and outer invoices remain unpriced. +No new kappa, supplier admission, complete multiplication theorem or +selected-frontier change follows. + +This proof and its verifier were produced by Nick Petalas. Credit Krzysztof +Wojt / PR5242 for the question, quotient character, mixed unit-price theorem +and support-rigidity method; Nick Petalas / PR5202 for the normal-C7 rank +bound; Cinna Davis / PR2011 and PR3893 for the model and representation +precedent; eumemic / PR288 and the retained register-model lineage. +Josie Elliston / PR6048 supplies the distinct-label all-group short-word +obstruction, following Nick Petalas / PR6038. The source statements are +pinned as provenance in SOURCES.json. +Apache-2.0. diff --git a/research/semilinear-two-normal-prices/README.md b/research/semilinear-two-normal-prices/README.md new file mode 100644 index 0000000000..667420cc20 --- /dev/null +++ b/research/semilinear-two-normal-prices/README.md @@ -0,0 +1,103 @@ +# Exact weighted tariff for two normal semilinear targets + +**Scoped written proof with exact finite corroboration; no new kappa.** +For every odd prime p, two nonidentity normal targets in +F2[F_(2^p)* semidirect C_p] have exact price + + 2 min(a, 2b), + +when every normal call costs a>0 and every outside call costs b>0. +The theorem permits repeated target labels, arbitrary finite restored dirty +workspace and free binary scalar mixing. Paid factors are rank-one +idempotents, and the endpoint is the complete formal group-algebra operator. + +This settles the two-normal-target first experiment in Open next question 1 +of [Krzysztof Wojt's PR5242](https://github.com/CrocSwap/integer-mult-bounds/pull/5242). +The new step excludes three outside calls. In the quotient character, +a three-call identity forces all three binary projectors to coincide; +one shared projector cannot deliver two independent nonidentity outputs. +Four outside calls attain the target, by factoring each normal label into +two outside labels. The [written proof](PROOF.md) combines that obstruction +with PR5242's credited natural-rank budget to settle every mixture and price. +Josie Elliston's [PR6048](https://github.com/CrocSwap/integer-mult-bounds/pull/6048) +already excludes three calls for distinct pair targets in every group when +no paid label is itself a target. That prior distinct-label floor is credited. +The new quotient-loop rigidity also treats repeated labels, which PR6048 +explicitly excludes, and yields the weighted tariff above. No new +distinct-pair unit-price floor is claimed. No predecessor census is rerun +as a deliverable. + +## Exact finite evidence + +The deterministic verifier checks the new three-factor lemma over F4 and +F8, with one to three roles. It enumerates 32,840 ordered factor pairs and +all 1,120 resulting three-factor loops; every loop has one common projector. +It also checks 4,116 literal three-outside-call words in the full order-21 +algebra and 144 attaining words for all 36 ordered pairs of normal targets, +including their arbitrary third dirty role. Each full endpoint comparison +checks every formal coefficient. A 13,203-case bounded count/price screen +corroborates the written unbounded case split. Eleven rejection controls and +an explicit nonbinary three-projector counterexample check the hypotheses. +A separate direct triple loop checks all 1,728 F4 two-role triples, without +the pair/inverse lookup used by the main finite census. +The finite fields and sizes do not prove the universal quantifiers. + +The verifier prints a freshly generated JSON receipt with hashes of all +package files. It writes no files and has no external runtime inputs. +[SOURCES.json](SOURCES.json) pins the original question and cited proof as +provenance, alongside the catalogue and selected record at canonical main +7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8. +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360644) +records the target before substantial work. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/semilinear-two-normal-prices/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/semilinear-two-normal-prices/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/semilinear-two-normal-prices +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/semilinear-two-normal-prices --check-source-history +``` + +Another CPython 3.12 path works. The registered normal and optimized commands +have a 60-second bound each. The direct checker also runs without Git in an +export containing this package. Package and publication checks authenticate +bytes and source history separately from the mathematical argument. + +## Scope and remaining obligations + +This is a formal weighted tariff, not an implemented physical supplier. +Native address operations, hosting/owners, physical restoration, movement, +precision, stock/compiler and a complete recursive/outer bill are unknown. +No new kappa, selected-frontier change or multiplication theorem is claimed. +Independent human and formal proof-kernel review are unclaimed. Lean, Docker +and the selected scientific cold replay are not part of this package. + +## Open next questions + +- Does a joint saving become possible for three normal targets with unequal + type prices? The three-call loop lemma does not classify longer quotient + identities. Start with the cheapest outside-only counts allowed by the + natural-rank inequality and prove their full formal endpoint, rather than + treating the rank relaxation as attainable. The blocker is a longer-word + structure theorem or an explicit sharing construction. +- Can one actual native caller realize the two-outside factorization with + a physical price below its normal call? First price both outside maps, + binary role changes, routing and restoration at one named boundary. + A legal source-bound physical interface is missing. + +These questions are unreserved and structured in [TASK.json](TASK.json). +The result is shipped at this first proved improvement. + +## Credit + +This contribution was produced by Nick Petalas. Krzysztof Wojt / PR5242 +supplies the question, quotient-character method and natural-rank premise; +Nick Petalas / PR5202 supplies the normal-C7 theorem; Cinna Davis / PR2011 +and PR3893 supply the semilinear model and representation precedent; +Josie Elliston / PR6048 supplies the distinct-label short-word obstruction, +building on Nick Petalas / PR6038; eumemic / PR288 and the retained +register-model lineage keep their credit. +No predecessor files or credit lines are changed. Apache-2.0. diff --git a/research/semilinear-two-normal-prices/SOURCES.json b/research/semilinear-two-normal-prices/SOURCES.json new file mode 100644 index 0000000000..fd21e2e2d7 --- /dev/null +++ b/research/semilinear-two-normal-prices/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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/conjugate-pair-group-free-audit/README.md", + "usage": "provenance", + "git_blob": "c0ae47bf6c566c69466e150661641d61fd9ff636", + "sha256": "3adf65a79d27ea7a60ec8978fa6b45f75d65c07c3aed019080b64431078f28f3" + }, + { + "path": "research/semilinear-mixed-tariff/PROOF.md", + "usage": "provenance", + "git_blob": "bc81fbd7ec32d8aeed9aa93fa3cf40396fef51bc", + "sha256": "171129b057490dea131aeeaab6941d4ae55b756143356f5a3656215ccfb44b2f" + }, + { + "path": "research/semilinear-mixed-tariff/README.md", + "usage": "provenance", + "git_blob": "dc95473ba57ec799194c33fc030f1f82dba484d2", + "sha256": "edecd78f1ab2661ac4115c09cd7b47d06274672f4a6a7a20202d9b5812a84c80" + } + ] +} diff --git a/research/semilinear-two-normal-prices/TASK.json b/research/semilinear-two-normal-prices/TASK.json new file mode 100644 index 0000000000..4859f1125b --- /dev/null +++ b/research/semilinear-two-normal-prices/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. 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", + "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": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact arbitrary-positive type-price tariff 2 min(a,2b) for two normal targets in every odd-prime-degree binary semilinear group, with arbitrary finite restored dirty workspace and free binary scalar mixing.", + "scope_change_reason": "Answer PR5242 Open next question 1 at its specified two-normal-target first experiment. The new three-outside-call obstruction closes the gap left by the existing natural-rank relaxation; no predecessor audit or full nonuniform multi-target theorem is claimed.", + "bottleneck_link": "A scoped obstruction to replacing normal calls cheaply in this nonabelian BIT register family. Physical per-call tariffs and a complete supplier remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved original weighted two-target tariff and its bounded verifier; do not extend to larger target lists.", + "outcome": "completed", + "evidence": "PROOF.md; exact quotient-loop census, literal group-algebra loops, all 36 order-21 target-pair attainments, bounded price/count corroboration and semantic controls in verify.py.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can three normal targets share outside calls under unequal normal/outside prices?", + "why_it_matters": "The two-target tariff excludes a proposed cheap exchange but does not settle longer quotient identities.", + "first_step": "Use the natural-rank inequality to select one candidate outside-only count, then derive or refute its full formal endpoint.", + "blocked_by": "No longer-word structure theorem or sharing construction is supplied." + }, + { + "question": "Can a native caller price the two-outside factorization below one normal call?", + "why_it_matters": "The exact formal weighted tariff has physical value only with legal complete call prices.", + "first_step": "Bind one source/consumer boundary and price both outside maps, role changes, movement and restoration.", + "blocked_by": "A source-bound native implementation and full physical bill are missing." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360644", + "question_source": { + "pr": 5242, + "author": "krzysztofwojt", + "question": "Open next question 1, two-normal-target first experiment" + }, + "novelty_boundary": "PR6048 already proves the distinct-label three-call floor. Claim new quotient-loop rigidity, repeated-label case and unequal type-price tariff; do not claim a new distinct-pair unit-price floor." +} diff --git a/research/semilinear-two-normal-prices/VALIDATION.md b/research/semilinear-two-normal-prices/VALIDATION.md new file mode 100644 index 0000000000..df440e811e --- /dev/null +++ b/research/semilinear-two-normal-prices/VALIDATION.md @@ -0,0 +1,70 @@ +# Verification contract and limits + +The claim is a written all-prime, all-finite-workspace theorem. The verifier +provides exact finite corroboration of its new quotient-loop lemma and +attaining endpoints. PR5242's natural-rank theorem is a cited premise, not +an independently checked deliverable. PR6048's distinct-label floor is +credited prior work. The repeated-label extension and weighted formula are +covered by the proof in this package. + +## Bounded checks + +The registered normal and optimized commands use CPython 3.12 and no third +party dependencies. Both run the complete verifier. Explicit `require` +checks remain active with assertions disabled. On local CPython 3.12.15, +macOS arm64, the direct commands take less than one second each; the +registered pair takes about one second. Each manifest command has a +60-second timeout. These are check-duration observations, not a speedup. +Fresh JSON receipts are printed to stdout and bind every package file by +SHA256. No stored PASS receipt or generated mathematical artifact is read. + +The pair/inverse lookup checks 32,840 pairs and 1,120 loops. A direct +triple enumeration independently checks the finite F4 two-role subcase, +including all 1,728 triples and its 12 loops. This is a second algorithm +in the same verifier, not independent human or proof-kernel review. +Full formal endpoints are compared coefficient by coefficient. Eleven +rejection controls exercise nonbinary, rank-two and nilpotent projectors, +invalid scalars and coefficient ranges, a character-only false positive, unrestored dirty output +and an altered scalar in a loop. The nonbinary counterexample passes in +its enlarged alphabet and demonstrates a real hypothesis boundary. + +## Code constraints + +Only `algebra.py` and `verify.py` are new executable code. They read no +external mathematical inputs, spawn no processes and write no files. +They use no recursion, dynamic evaluation, decorators or global mutable +state. All arithmetic is exact integer arithmetic over finite fields or +bitsets in the 21-dimensional group algebra. Direct calls and data access +are shallow. The verifier's finite sizes are fixed, not user-controlled. + +Every loop is bounded by these constants or finite collections derived +from them: at most three roles, fields of size at most eight, 28 binary +projectors per size, 168 factors per census, 28,224 factor pairs in one +census, 21 group labels, 14 outside labels, six normal labels, 13 count +values per type and nine positive integer prices per type. The group +coefficient extractor has an explicit 21-iteration cap and rejects excess +bits. Field inversion has at most six multiplications. The largest +function is below 60 physical lines. Structured exception controls catch +only the expected `ValueError`; other failures propagate. + +Rule 3 deviation: CPython allocates arithmetic objects and collections +inside loops. Fixed allocation after initialization cannot be guaranteed +in this managed runtime. Scope is this finite verifier, with the bounds +above limiting live matrices to 3 by 3, group elements to 21 bits, and one +census list to 168 factors. Pair and triple products are consumed one at +a time. There are no unbounded queues, retained histories or child processes. +The registered timeout is an additional guard. A future parameterized +search must enforce new size/capacity limits before accepting inputs. + +Warning-strict source compilation, function-length inspection and normal, +optimized and registered execution cover the changed code. No Python +linter or type checker is installed in the local interpreter; those +checks are unrun. Shared CI or analysis configuration is unchanged. + +## Unrun obligations + +Independent human review, formal proof-kernel acceptance, native realization, +physical pricing, supplier admission and the selected scientific cold replay +remain unrun. Lean and Docker were not invoked. Hosted replay verifies the +registered finite checks and source metadata, not these obligations or the +universal mathematical proof. No selected-frontier update is requested. diff --git a/research/semilinear-two-normal-prices/VERIFY.json b/research/semilinear-two-normal-prices/VERIFY.json new file mode 100644 index 0000000000..906357cf57 --- /dev/null +++ b/research/semilinear-two-normal-prices/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact new quotient-loop lemma corroboration, literal full-formal endpoints, weighted count screen and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact new quotient-loop lemma corroboration, literal full-formal endpoints, weighted count screen and semantic rejection controls." + } + ] +} diff --git a/research/semilinear-two-normal-prices/algebra.py b/research/semilinear-two-normal-prices/algebra.py new file mode 100644 index 0000000000..bd889ecb0e --- /dev/null +++ b/research/semilinear-two-normal-prices/algebra.py @@ -0,0 +1,149 @@ +"""Exact finite corroboration for the weighted two-normal theorem. + +Produced by Nick Petalas. Apache-2.0. +""" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def mul(a, b, degree, polynomial): + result = 0 + for _ in range(degree): + if b & 1: + result ^= a + b >>= 1 + a <<= 1 + if a & (1 << degree): + a ^= polynomial + return result + + +def inverse(value, degree, polynomial): + require(0 < value < 1 << degree, "nonzero field element required") + result = 1 + for _ in range((1 << degree) - 2): + result = mul(result, value, degree, polynomial) + return result + + +def identity(size): + return tuple(tuple(int(i == j) for j in range(size)) for i in range(size)) + + +def multiply(left, right, degree, polynomial): + size = len(left) + rows = [[0] * size for _ in range(size)] + for i in range(size): + for j in range(size): + for k in range(size): + rows[i][j] ^= mul(left[i][k], right[k][j], degree, polynomial) + return tuple(tuple(row) for row in rows) + + +def projectors(size): + result = [] + for u in range(1, 1 << size): + for v in range(1, 1 << size): + if (u & v).bit_count() % 2: + result.append(tuple(tuple(((u >> i) & 1) * ((v >> j) & 1) + for j in range(size)) for i in range(size))) + return tuple(result) + + +def validate_projector(projector): + size = len(projector) + require(1 <= size <= 3, "finite checker supports one to three roles") + require(all(len(row) == size for row in projector), "square projector required") + require(all(value in (0, 1) for row in projector for value in row), "binary projector required") + require(projector in projectors(size), "rank-one idempotent required") + + +def gate(projector, scalar, degree, polynomial): + validate_projector(projector) + require(2 <= scalar < 1 << degree, "nonidentity invertible scalar required") + size = len(projector) + return tuple(tuple(int(i == j) ^ mul(scalar ^ 1, projector[i][j], degree, polynomial) + for j in range(size)) for i in range(size)) + + +def quotient_census(degree, polynomial, size): + factors = [(p, scalar, gate(p, scalar, degree, polynomial)) + for p in projectors(size) for scalar in range(2, 1 << degree)] + inverse_gates = {gate(p, inverse(scalar, degree, polynomial), degree, polynomial): (p, scalar) + for p, scalar, _ in factors} + require(len(inverse_gates) == len(factors), "injective gate parameterization") + closures = 0 + for p, scalar, first in factors: + for q, other, second in factors: + third = inverse_gates.get(multiply(second, first, degree, polynomial)) + if third is not None: + r, last = third + require(p == q == r, "three-call quotient loop has a common projector") + require(mul(mul(scalar, other, degree, polynomial), last, degree, polynomial) == 1, + "scalar product is one") + closures += 1 + expected = len(projectors(size)) * ((1 << degree) - 2) * ((1 << degree) - 3) + require(closures == expected, "complete quotient-loop count") + return {"degree": degree, "roles": size, "pairs": len(factors) ** 2, "loops": closures} + + +def group_table(): + labels = tuple((a, j) for a in range(1, 8) for j in range(3)) + lookup = {label: index for index, label in enumerate(labels)} + table = [] + for a, j in labels: + row = [] + for b, k in labels: + twisted = b + for _ in range(j): + twisted = mul(twisted, twisted, 3, 11) + row.append(lookup[(mul(a, twisted, 3, 11), (j + k) % 3)]) + table.append(tuple(row)) + return labels, tuple(table) + + +def coefficients(value): + require(0 <= value < 1 << 21, "group algebra coefficient range") + result = [] + for _ in range(21): + if not value: + break + lowest = value & -value + result.append(lowest.bit_length() - 1) + value ^= lowest + require(value == 0, "group algebra has exactly 21 labels") + return result + + +def formal_mul(left, right, table): + value = 0 + for i in coefficients(left): + for j in coefficients(right): + value ^= 1 << table[i][j] + return value + + +def formal_product(left, right, table): + size = len(left) + rows = [[0] * size for _ in range(size)] + for i in range(size): + for j in range(size): + for k in range(size): + rows[i][j] ^= formal_mul(left[i][k], right[k][j], table) + return tuple(tuple(row) for row in rows) + + +def formal_gate(projector, label): + validate_projector(projector) + require(0 <= label < 21, "formal label range") + size = len(projector) + return tuple(tuple(int(i == j) ^ (projector[i][j] * ((1 << label) ^ 1)) + for j in range(size)) for i in range(size)) + + +def target(labels): + return tuple(tuple((1 << label) if i == j else 0 for j in range(len(labels))) + for i, label in enumerate(labels)) diff --git a/research/semilinear-two-normal-prices/verify.py b/research/semilinear-two-normal-prices/verify.py new file mode 100644 index 0000000000..18b7ed6404 --- /dev/null +++ b/research/semilinear-two-normal-prices/verify.py @@ -0,0 +1,169 @@ +"""Finite evidence for a written all-prime, all-workspace theorem. + +Produced by Nick Petalas. Apache-2.0. No external runtime inputs. +""" + +import hashlib +import json +from pathlib import Path + +from algebra import ( + coefficients, formal_gate, formal_product, gate, group_table, identity, inverse, + mul, multiply, projectors, quotient_census, require, target, +) + + +def expect_rejection(operation, message): + try: + operation() + except ValueError: + return 1 + raise ValueError("control accepted: " + message) + + +def formal_loops(): + labels, table = group_table() + outside = [i for i, (_, j) in enumerate(labels) if j] + loops = 0 + products = set() + for a in outside: + for b in outside: + for c in outside: + completed = table[c][table[b][a]] + if labels[completed][1]: + continue + for p in projectors(2): + actual = formal_product(formal_gate(p, b), formal_gate(p, a), table) + actual = formal_product(formal_gate(p, c), actual, table) + require(actual == formal_gate(p, completed), "literal full-formal loop endpoint") + loops += 1 + products.add(completed) + require(products == {i for i, (_, j) in enumerate(labels) if not j}, "all kernel labels reached") + return loops + + +def attaining_words(): + labels, table = group_table() + lookup = {label: i for i, label in enumerate(labels)} + normals = [i for i, (a, j) in enumerate(labels) if a != 1 and j == 0] + endpoints = 0 + words = 0 + for first in normals: + for second in normals: + desired = target((first, second, 0)) + for replaced in ((), (0,), (1,), (0, 1)): + actual = target((0, 0, 0)) + for role, label in enumerate((first, second)): + p = tuple(tuple(int(i == role == j) for j in range(3)) for i in range(3)) + sequence = (label,) + if role in replaced: + sequence = (lookup[(1, 1)], lookup[(labels[label][0], 2)]) + for paid in sequence: + actual = formal_product(formal_gate(p, paid), actual, table) + require(actual == desired, "all formal coefficients and arbitrary dirty role restored") + words += 1 + endpoints += 1 + return {"target_pairs": endpoints, "words": words, "roles": 3, "group_labels": 21} + + +def weighted_screen(): + cases = 0 + for a in range(1, 10): + for b in range(1, 10): + expected = 2 * min(a, 2 * b) + witnesses = (2 * a, a + 2 * b, 4 * b) + require(min(witnesses) == expected, "attaining weighted envelope") + for normal in range(13): + for outside in range(13): + if 3 * normal + 2 * outside < 6: + continue + if normal == 0 and outside < 4: + continue + require(a * normal + b * outside >= expected, "rank plus loop lower envelope") + cases += 1 + return cases + + +def direct_triples(): + factors = [(p, gate(p, scalar, 2, 7)) + for p in projectors(2) for scalar in (2, 3)] + loops = 0 + for p, first in factors: + for q, second in factors: + for r, third in factors: + actual = multiply(third, multiply(second, first, 2, 7), 2, 7) + if actual == identity(2): + require(p == q == r, "direct triple loop has a common projector") + loops += 1 + require(loops == 12, "direct triples agree with pair/inverse census") + return {"triples": len(factors) ** 3, "loops": loops} + + +def character_matrix(matrix, labels): + rows = [] + for row in matrix: + result = [] + for entry in row: + value = 0 + for index, (_, exponent) in enumerate(labels): + if (entry >> index) & 1: + value ^= (1, 2, 3)[exponent] + result.append(value) + rows.append(tuple(result)) + return tuple(rows) + + +def controls(): + p = ((1, 0), (0, 0)) + total = 0 + for bad in (((1, 2), (0, 0)), ((1, 0), (0, 1)), ((0, 1), (0, 0))): + total += expect_rejection(lambda bad=bad: gate(bad, 2, 2, 7), "projector domain") + for bad in (0, 1, 4): + total += expect_rejection(lambda bad=bad: gate(p, bad, 2, 7), "scalar domain") + for bad in (-1, 1 << 21): + total += expect_rejection(lambda bad=bad: coefficients(bad), "coefficient domain") + # Dropping the binary restriction really changes the three-factor theorem. + nonbinary = (((2, 0), (0, 1)), ((2, 3), (0, 1)), ((2, 1), (0, 1))) + actual = multiply(nonbinary[2], multiply(nonbinary[1], nonbinary[0], 2, 7), 2, 7) + require(actual == identity(2), "nonbinary counterexample closes") + require(len(set(nonbinary)) == 3, "nonbinary projectors differ") + labels, table = group_table() + lookup = {label: i for i, label in enumerate(labels)} + one_output = formal_gate(p, lookup[(2, 0)]) + fake_pair = target((lookup[(2, 0)], lookup[(3, 0)])) + require(character_matrix(one_output, labels) == character_matrix(fake_pair, labels) == identity(2), + "quotient alone accepts the wrong full endpoint") + total += expect_rejection(lambda: require(one_output == fake_pair, "full endpoint"), "quotient-only test") + dirty = formal_gate(((1, 0, 0), (0, 0, 0), (1, 0, 0)), lookup[(2, 0)]) + total += expect_rejection(lambda: require(dirty == target((lookup[(2, 0)], 0, 0)), "restoration"), + "omitted dirty-output restoration") + altered = multiply(gate(p, 3, 2, 7), multiply(gate(p, 2, 2, 7), gate(p, 2, 2, 7), 2, 7), 2, 7) + total += expect_rejection(lambda: require(altered == identity(2), "altered loop"), "changed scalar") + return total + + +def main(): + fields = ((2, 7), (3, 11)) + for degree, polynomial in fields: + for value in range(1, 1 << degree): + require(mul(value, inverse(value, degree, polynomial), degree, polynomial) == 1, + "finite-field inverse") + receipt = { + "status": "PASS_SEMILINEAR_TWO_NORMAL_PRICES", + "claim_type": "scoped written proof with exact finite corroboration", + "tariff": "2 min(a, 2b)", + "quotient": [quotient_census(d, f, r) for d, f in fields for r in range(1, 4)], + "direct_triples": direct_triples(), + "literal_outside_loops": formal_loops(), + "attainment": attaining_words(), + "weighted_grid_cases": weighted_screen(), + "rejection_controls": controls(), + } + package = Path(__file__).resolve().parent + receipt["sha256"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()