From 375aced69b88d996fb9f8faa8911fefeaaf1923b Mon Sep 17 00:00:00 2001 From: apoursh <8867770+apoursh@users.noreply.github.com> Date: Thu, 29 Oct 2026 11:36:28 -0400 Subject: [PATCH] Prove eight-call floor for two arbitrary signed rank-one frames --- research/bit-two-signed-frame-floor/PROOF.md | 209 ++++++++++++++ research/bit-two-signed-frame-floor/README.md | 143 ++++++++++ .../bit-two-signed-frame-floor/SOURCES.json | 30 ++ research/bit-two-signed-frame-floor/TASK.json | 72 +++++ .../bit-two-signed-frame-floor/VERIFY.json | 37 +++ .../bit-two-signed-frame-floor/independent.py | 266 ++++++++++++++++++ research/bit-two-signed-frame-floor/verify.py | 149 ++++++++++ 7 files changed, 906 insertions(+) create mode 100644 research/bit-two-signed-frame-floor/PROOF.md create mode 100644 research/bit-two-signed-frame-floor/README.md create mode 100644 research/bit-two-signed-frame-floor/SOURCES.json create mode 100644 research/bit-two-signed-frame-floor/TASK.json create mode 100644 research/bit-two-signed-frame-floor/VERIFY.json create mode 100644 research/bit-two-signed-frame-floor/independent.py create mode 100644 research/bit-two-signed-frame-floor/verify.py diff --git a/research/bit-two-signed-frame-floor/PROOF.md b/research/bit-two-signed-frame-floor/PROOF.md new file mode 100644 index 0000000000..3797e6b8dc --- /dev/null +++ b/research/bit-two-signed-frame-floor/PROOF.md @@ -0,0 +1,209 @@ +# Two signed added frames still require eight calls + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. + +## Model and dependencies + +Use Cinna Davis's PR2085/2112 formal register model. Addresses are rational +symmetric 2-by-2 matrices, with + +``` +A = diag(1,0), B = diag(0,1), +P = [[1,1],[1,1]]/2, Q = [[1,-1],[-1,1]]/2. +A+B = P+Q = I2. +``` + +Add two arbitrary nonzero symmetric rational rank-one addresses R,S. Either +sign is allowed, including equal addresses, opposite addresses and old-label +duplicates. A real symmetric rank-one matrix has exactly one nonzero real +eigenvalue: it is positive or negative semidefinite, never indefinite. + +Let Lambda be the additive lattice generated by A,B,P,R,S. Over F2[Lambda], +a paid factor is D_N(F)=I_w+([F]-1)N, where N is any binary rank-one idempotent +and F is one of the six labels. Arbitrary address-independent GL_w(F2) +maps are free. Every role initially contains arbitrary data. For any finite +w>=4 the required complete endpoint is + +``` +T_w = diag([A+P],[A+Q],[B+P],[B+Q],1,...,1). +``` + +Extra roles must be restored exactly; no clean workspace is assumed. The +objective is paid-call count only, with no physical native tariff asserted. + +**Theorem.** The exact minimum is eight, even with these two signed additions. + +The new result is the sign reduction below. The final positive-case +exclusion is **Josie Elliston's PR6111 theorem**, pinned in SOURCES.json; +the one-added-frame case is **apoursh's PR6079 theorem**, also pinned. +These are explicit theorem dependencies, not new proofs or fresh scientific +replays of those predecessors. The reduction itself is proved below without +relying on a search or on PR6111's finite support classification. + +## 1. Necessary invariants + +Normalize interspersed free maps into conjugates of paid factors and one +trailing free map. Augmentation [F]->1 sends every paid factor and T_w to +identity, so that trailing free map is identity. Conjugation preserves +rank-one idempotence. This is the normalization retained in PR6089. + +Write a,b,p,q,r,s for the six nonnegative label counts, and n=a+b+p+q. +For a hypothetical word of at most seven calls using both added labels, +r,s>=1 and n<=5. The rank-one determinant identity (PR2910) gives + +``` +rR+sS = M = 4I2 - aA - bB - pP - qQ. (1) +``` + +Indeed det D_N(F)=[F], and all free binary invertible maps have determinant +one. The target determinant is [4I2]; monomials in this torsion-free group +algebra are distinct. + +Expanding each paid factor as (I+N)+[F]N shows that every target exponent +H in {A+P,A+Q,B+P,B+Q} must be a subset sum of the paid labels, with each +occurrence used at most once. Cancellation can remove support; it cannot +create an exponent absent from every subset. This is necessary, not sufficient. + +For an additive character chi:Lambda->F2, substitute [F]->1+chi(F)e, +where e^2=0. The first-order equation implies + +``` +number of calls detected by chi >= number of targets detected by chi. (2) +``` + +This follows from rank subadditivity for the sum of the detected N's, and +holds at every restored width. These determinant, support and character +methods retain their predecessor attribution. + +## 2. Positive-definite residuals force positive summands + +If X,Y are nonzero real symmetric rank-one matrices and X+Y is positive +definite, both X and Y are positive semidefinite. Take nonzero v in ker Y. +Then v^T X v=v^T(X+Y)v>0, so the unique nonzero eigenvalue of X is positive. +Exchange X and Y. Apply this to X=rR,Y=sS; their positive integer +multiplicities preserve signs. + +Thus only non-positive-definite M could allow a negative added frame. + +## 3. Every indefinite residual fails target support + +Put d=a-b, e=p-q. Direct calculation gives + +``` +2M = [[8-n-d,-e],[-e,8-n+d]], +4 det M = (8-n)^2-d^2-e^2, +|d|+|e| <= n, d+e = n (mod 2). (3) +``` + +If n<=4, each old address is an orthogonal projector bounded above by I2, +so M>= (4-n)I2>=0. An indefinite M therefore requires n=5. Equation (3) +then requires d^2+e^2>9. Since |d|+|e| is odd and at most five, it must be +five: if it were at most three, d^2+e^2<=9. Equality with n says there is +no cancellation within either opposite pair. Hence all five old calls use +at most one E from {A,B} and at most one G from {P,Q}. If a pair is absent, +choose either of its members. Also r=s=1. + +The matrices E,G,I2 are linearly independent over Q. Define the rational +linear functional ell by ell(E)=ell(G)=0, ell(I2)=1. The four target +exponents have ell-values {0,1,1,2}, since the other two old frames are +I2-E and I2-G. Meanwhile (1) gives ell(R)+ell(S)=4. +All old calls have ell-value zero, and each of R,S occurs once. Therefore +every subset sum has ell-value in + +``` +{0, rho, 4-rho, 4}, where rho=ell(R). +``` + +This set cannot contain both one and two: containing one forces rho=1 +or rho=3, and then two is absent. At least one required target lacks +support. This excludes the indefinite case even without the rank-one +assumption on R,S. There are twenty such count profiles; enumeration is +only a corroboration of this argument. + +## 4. Every rank-one residual is also excluded + +Since tr M=8-n>=3, a singular residual is nonzero positive rank one. +If nonzero symmetric rank-one X,Y have rank(X+Y)=1, their image lines +coincide. Write X=c uu^T,Y=t vv^T with c,t nonzero; then + +``` +det(X+Y)=ct (u1*v2-u2*v1)^2. +``` + +Thus R,S lie on the whole rational line of M, regardless of their signs. + +Equation (3) and |d|+|e|<=n imply n>=4. At n=4 or n=5 the circles +d^2+e^2=16 or 9 have only axial integer solutions. Up to old-alphabet +symmetry, the possible old-call multisets are exactly: + +| Old calls | Residual | Exclusion | +|---|---|---| +| 4E | 4Eperp | Span | +| 4E+Eperp | 3Eperp | Span | +| 3E+G+Gperp | 3Eperp | Character | + +Here Eperp=I2-E, and {G,Gperp} is the other opposite pair. +The first row permits r+s<=3; the other rows force r=s=1. + +In the first two rows every available label lies in span_Q(E,Eperp). +Each target combines one frame from each pair and lies outside that span, +so target support fails. + +In the third row choose an integer-valued linear functional on the actual +lattice: 2*offdiag when E belongs to {A,B}, or first diagonal minus second +diagonal when E belongs to {P,Q}. It vanishes on the **entire rational** +line of Eperp as well as on E, and takes values +/-1 on G,Gperp. Thus its +reduction modulo two is well-defined even if R,S have even denominators. +It detects only the two G,Gperp calls, but all four targets. Equation (2) +gives the contradiction 2>=4. + +This excludes every rank-one residual. The finite count check has twenty +full profiles: sixteen span cases and four character cases. + +## 5. Conclusion and sharpness + +Every residual has positive trace, so the three cases above are exhaustive. +Any hypothetical <=7-call word using both R,S must have a positive-definite +residual, which forces both added frames positive. PR6111 excludes that +case for all directions, scales and finite restored widths. + +For words omitting one or both added labels, restrict to the subgroup +generated by the labels actually used and the target labels. Its group +algebra injects into F2[Lambda], so the equality also holds in that smaller +algebra. This restriction matters: unused fractional frames need not allow +old-lattice characters to extend to the original larger Lambda. + +If only one extra label occurs, PR6079 already proves the eight-call floor +for arbitrary signed scaling. If neither occurs, the two old-lattice +characters chi_AB and chi_PQ separately require a+b>=4 and p+q>=4, hence +at least eight calls. Assigning the two displayed summands of each H to +its own coordinate gives the familiar eight-call word, proving sharpness. + +The signed premise is meaningful at longer lengths: replace one A in this +direct word by 2A,-A on the same coordinate projector. This gives an exact +nine-call word using both a positive and a negative added frame. Thus the +reduction is a short-word statement, not an all-length positivity theorem. + +## 6. Independent exact corroboration + +independent.py separately enumerates all 462 six-count profiles, without +any sign or PSD filter. In basis (A,B,P), with X=rR and S=(M-X)/s, a +target subset with added multiplicities i,j satisfies + +``` +(s*i-r*j) X = r*s*(H-old_subset) - r*j*M. +``` + +A nonzero coefficient pins X; a zero coefficient gives a free solution +exactly when its right side is zero. Candidate pins are filtered only for +nonzero symmetric rank one, admitting both signs. Intersecting the four +target sets gives 435 empty profiles, seven free families, and 32 splits +across twenty other profiles. All pinned splits turn out positive, and +each free residual is positive definite. This agrees with the sign +reduction through an independent classification route. None of these +necessary-condition survivors is asserted to be a realizable word. + +Finite fixtures and mutation controls are implementation evidence. The +unbounded direction, denominator and width quantifiers come from the +written reduction and explicitly credited predecessor theorems. No +independent human review or formal proof-kernel acceptance is claimed. diff --git a/research/bit-two-signed-frame-floor/README.md b/research/bit-two-signed-frame-floor/README.md new file mode 100644 index 0000000000..b76192b707 --- /dev/null +++ b/research/bit-two-signed-frame-floor/README.md @@ -0,0 +1,143 @@ +# Two signed added rank-one frames still require eight calls + +**Scoped proof with exact corroboration.** Allowing either sign for two added +nonzero symmetric rational rank-one addresses does not lower the eight-call +minimum for the PR2085/2112 four-target endpoint. Arbitrary finite restored +dirty workspace and free address-independent binary mixing are allowed. +This closes the short-word non-positive-frame question in Josie Elliston's +[PR6111](https://github.com/CrocSwap/integer-mult-bounds/pull/6111). + +The new contribution is an elementary **signed-to-positive reduction**. +The final positive-case exclusion is PR6111's theorem; the one-extra case +uses [PR6079](https://github.com/CrocSwap/integer-mult-bounds/pull/6079). +Both sources are archived and `partially_reviewed` in the current central +ledger. They are explicit mathematical dependencies; their scientific +replays and independent acceptance are not claimed here. + +## Result and proof + +Let A=diag(1,0), B=diag(0,1), P=[[1,1],[1,1]]/2 and +Q=[[1,-1],[-1,1]]/2. The complete endpoint is +`diag([A+P],[A+Q],[B+P],[B+Q],1,...)`. Each paid factor is +`I+([F]-1)N`, with binary rank-one idempotent N and +`F in {A,B,P,Q,R,S}`. R and S may be positive, negative, coincident, +opposite, or duplicates of old frames. They remain nonzero and rank one. + +[PROOF.md](PROOF.md) gives all hypotheses and the width-independent proof. +For a hypothetical word using both additions in at most seven calls, +determinant conservation gives +`rR+sS=M=4I-aA-bB-pP-qQ`, with at most five old calls. + +- If M is indefinite, a scalar projection requires both 1 and 2 in + `{0,rho,4-rho,4}`, which is impossible. +- If M has rank one, both additions lie on its line. Exact target support + or a first-order character with capacity two and demand four excludes it. +- If M is positive definite, evaluating on the two kernels forces R and S + positive. PR6111 then applies. + +The direct eight-call word attains the minimum. Negative frames really can +appear at longer lengths: replace one A call by 2A followed by -A to get +an exact nine-call word. This is not an all-length positivity theorem. + +There is no native supplier, paid-profile saving, new κ or discharge of any +selected framework assumption. The selected conditional result remains +`781451/250000000`. Formal paid calls do not automatically price physical +operations, and all native/caller/compiler/precision/recovery obligations +remain separate. + +## Evidence and reproduction + +Python 3.12, standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/bit-two-signed-frame-floor +python3.12 -I -W error -B research/bit-two-signed-frame-floor/verify.py +python3.12 -I -O -W error -B research/bit-two-signed-frame-floor/verify.py +``` + +Expected markers are `PASS_SIGNED_TWO_FRAME_SUPPORT` and +`PASS_TWO_SIGNED_FRAME_REDUCTION`; the registered runner executes both modes. +The direct verifier needs only this package and its two declared README +inputs. It uses no Git, network, nonstandard package or predecessor code. + +The elementary check reconstructs all 462 profiles as 422 positive-definite, +20 indefinite, 16 singular-span and four singular-character cases. It also +checks the two-summand determinant/sign identity on 576 rational fixtures +and the three-summand counterexample `-A+2A+B=I` to any overgeneralization. + +The separately written checker uses integer subset equations in the rational +basis (A,B,P), rather than the primary check's physical matrix entries. +It applies **no PSD or positive-trace filter** to candidate splits. Its +complete classification gives 435 empty profiles, seven free families and +32 pinned splits across twenty profiles. Positivity of every pinned split +is checked afterward. All 148 concrete opposite-sign residual splits fail +literal target support. Twenty-four control checks include negative rotated +frames, zero/rank-two rejection, the nine-call signed word on four/six roles, +omitting its negative call, the ordinary eight-call positive control and +a changed target. Controls include positive fixtures; “24” is not a count +of rejected mutants. The independent inventory digest is +`ed1b074151ab497af3c585f532ad0b0dd4c0cecb4b764721e4109f448d434443`. + +These are exact finite checks, not finite extrapolation to arbitrary widths +or denominators. The written proof supplies those quantifiers. Local +environment: CPython 3.12.14, macOS arm64. Normal/optimized registered replay, +source metadata and committed-byte/export checks are separate obligations. +No formal proof kernel, independent human review or selected cold replay +is claimed. + +## Coordination, sources and scope + +Canonical main was fetched before work, and this branch starts at +`3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision 8. +[Canonical claim/status](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19270802). +Task `bit-new-register-model` has **changed scope**, recorded with the full +original card in [TASK.json](TASK.json): a formal alphabet theorem rather +than a native larger/nonabelian construction. + +The expansion decision is to settle this explicitly open sign hypothesis +before any implementation campaign. Three added positive frames were +considered as a different mechanism and remain unreserved. This result +does not justify more search inside the now-excluded two-frame short model. + +Current handoffs and all-state searches for signed/two/rank-one frames, +three positive frames and PR6111 were inspected on October 29, 2026. +PR6148 excludes one eight-call half-frame example; PR6186 accelerates +PR6111's positive checker. Neither supplies this signed reduction. +The offline helper searched 24 of 8,567 local notes with no usable remote +snapshot. Sparse local coverage and bounded live searches are not a proof +of novelty or coverage of unpublished work. + +The selected record, source manifest, certificate, review, baseline script +and all 1,227 previously materialized orientation inputs are unchanged from +the preceding successful binding-only orientation at main `721c03822`. +That orientation is reused after a Git-diff check, not described as a fresh +scientific replay. The selected record hash remains +`9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa`. + +[SOURCES.json](SOURCES.json) pins the exact canonical theorem READMEs: +PR6111 head `961b749fa40a1117d0746064528d2dfa290c57e0` and PR6079 head +`44745c427f710e406cb2d2c6de458b7f93d81f01`. Catalogue and selected record +are historical provenance. Predecessor bytes remain unchanged. + +## Open next questions + +Can three or more signed additions beat eight? The two-summand kernel +argument fails already at `-A+2A+B=I`. Start with one explicit three-frame +candidate and its determinant/support constraints; an exact word and full +native invoice would still be required for a multiplication improvement. +No larger search or follow-up is reserved. Structured relevance, first +step and blockers are in TASK.json. + +## Credit + +Prepared by **apoursh** with substantial OpenAI Codex assistance in proof, +implementation and separate agent mathematical/code audits. Apache-2.0. +Agent reviews are not independent human or proof-kernel acceptance. + +Josie Elliston/Claude retains PR6111's positive two-frame theorem and support +classification; JoyboyBrian retains #6104's question and split formulation; +apoursh retains PR6089/6079's classification and single-frame result; +Nick Petalas retains PR2910's determinant method; Cinna Davis retains the +PR2085/2112 model and endpoint; Philippe Van Velzen and the retained BIT +lineage keep their prior floor and framework credit. Kernel, determinant +and rank algebra are classical; no literature-wide priority is claimed. diff --git a/research/bit-two-signed-frame-floor/SOURCES.json b/research/bit-two-signed-frame-floor/SOURCES.json new file mode 100644 index 0000000000..cd51f5e5c4 --- /dev/null +++ b/research/bit-two-signed-frame-floor/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "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/bit-single-scaled-frame-floor/README.md", + "usage": "input", + "git_blob": "826e8e4e7a3a50a56bdec49e6af758069a8ed06f", + "sha256": "dae847a3e40b3999c2797b7222d2ff7ad2762e0193b251dd8e9c2a493ab0b27d" + }, + { + "path": "research/bit-two-positive-frames-seven-call/README.md", + "usage": "input", + "git_blob": "98eb6718d0ae424c129cf08b186fd2a5593ca783", + "sha256": "8832e843b129a1fc802e1f0db54d6f731eb9bd7b2b82f583c7809dbd9c0857d5" + } + ] +} diff --git a/research/bit-two-signed-frame-floor/TASK.json b/research/bit-two-signed-frame-floor/TASK.json new file mode 100644 index 0000000000..06afbf7387 --- /dev/null +++ b/research/bit-two-signed-frame-floor/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "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": "Resolve PR6111 non-positive-frame question at at most seven calls: two arbitrary signed nonzero symmetric rational rank-one additions, arbitrary finite restored dirty width, free binary mixing.", + "scope_change_reason": "The card asks for a larger/nonabelian native construction. This is a formal alphabet side result removing positivity from the two-added-frame lower bound; no native conversion or supplier is claimed.", + "bottleneck_link": "Closes the two-signed-frame short-word escape before any native implementation search. The relaxed paid-call floor stays eight, so this model offers no local call-count saving.", + "budget_minutes": 60, + "stop_rule": "Stop after a complete signed-to-positive reduction, a counterexample, or an explicit unresolved support family. Do not expand to three frames or price unconstructed native operations.", + "outcome": "completed", + "evidence": "Elementary indefinite/rank-one/positive-definite case proof; independent exact signed support census of462 profiles; negative-frame and longer-word controls. PR6111 positive-case and PR6079 one-frame theorems are explicitly inherited, not freshly replayed.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance with proof, independent code, and separate agent mathematical/code review; no independent human or formal-kernel approval.", + "open_questions": [ + { + "question": "Can three or more added signed rank-one frames lower the eight-call minimum?", + "why_it_matters": "This changes the two-summand hypothesis essential to the sign reduction.", + "first_step": "Test determinant and target support on one declared three-frame candidate; the identity -A+2A+B=I shows why positive-definite residuals no longer force positivity.", + "blocked_by": "No complete multi-frame support reduction or exact word is supplied. Native implementation and complete tariff remain separate obligations." + } + ], + "selection": { + "seed": "d0203126cca2e0dbd82a3ac5e20279ec", + "scope_key": "7084092dd726e7ba1f2f", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19270802", + "upstream_checked_utc": "2026-10-29T15:25:42Z", + "priority_revision": 8 + }, + "expansion_decision": "Narrow the explicitly open signed-premise question; compare the separate three-positive-frame route but leave it unreserved. No implementation expansion or selected-frontier change." +} diff --git a/research/bit-two-signed-frame-floor/VERIFY.json b/research/bit-two-signed-frame-floor/VERIFY.json new file mode 100644 index 0000000000..24a1065cb5 --- /dev/null +++ b/research/bit-two-signed-frame-floor/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-single-scaled-frame-floor/README.md", + "research/bit-two-positive-frames-seven-call/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source pins; elementary sign-reduction partition; independent signed support census; positive and negative controls. Predecessor theorem replays are not included." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source pins; elementary sign-reduction partition; independent signed support census; positive and negative controls. Predecessor theorem replays are not included." + } + ] +} diff --git a/research/bit-two-signed-frame-floor/independent.py b/research/bit-two-signed-frame-floor/independent.py new file mode 100644 index 0000000000..766ebc3456 --- /dev/null +++ b/research/bit-two-signed-frame-floor/independent.py @@ -0,0 +1,266 @@ +"""Exact signed two-frame support certificate; Python standard library. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +The determinant/support reduction is credited to Nick Petalas (PR2910), +apoursh (PR6089) and Josie Elliston (PR6111); this independently written +census removes both positivity filters from the latter question. + +All addresses use the rational basis (A,B,P), not physical matrix entries. +The six count variables are (A,B,P,Q,R,S), with Q=A+B-P. No predecessor +code, theorem checker, nonstandard dependency, Git or network is imported. +""" +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json + +ZERO = (Fraction(0),) * 3 +A = (Fraction(1), Fraction(0), Fraction(0)) +B = (Fraction(0), Fraction(1), Fraction(0)) +P = (Fraction(0), Fraction(0), Fraction(1)) +Q = (Fraction(1), Fraction(1), Fraction(-1)) +OLD = (A, B, P, Q) +TARGETS = ((1, 0, 1), (2, 1, -1), (0, 1, 1), (1, 2, -1)) +TOTAL = (4, 4, 0) +EXPECTED_FREE = { + (1, 1, 1, 1, 1, 1), (1, 1, 1, 1, 1, 2), (1, 1, 1, 1, 2, 1), + (2, 1, 1, 1, 1, 1), (1, 2, 1, 1, 1, 1), + (1, 1, 2, 1, 1, 1), (1, 1, 1, 2, 1, 1), +} + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def plus(left, right): + return tuple(x + y for x, y in zip(left, right)) + + +def minus(left, right): + return tuple(x - y for x, y in zip(left, right)) + + +def times(scale, vector): + return tuple(scale * x for x in vector) + + +def matrix(vector): + """Map basis coordinates to the physical rational symmetric matrix.""" + a, b, p = vector + return ((a + Fraction(p, 2), Fraction(p, 2)), + (Fraction(p, 2), b + Fraction(p, 2))) + + +def determinant_twice(vector): + a, b, p = vector + return 2*a*b + (a+b)*p + + +def trace(vector): + return sum(vector) + + +def signed_rank_one(vector): + # Nonzero symmetric real rank-one matrices are positive OR negative + # semidefinite. Trace may have either sign. The zero matrix is excluded. + return vector != ZERO and determinant_twice(vector) == 0 + + +def positive_rank_one(vector): + return signed_rank_one(vector) and trace(vector) > 0 + + +def positive_definite(vector): + return determinant_twice(vector) > 0 and trace(vector) > 0 + + +def old_address(counts): + a, b, p, q = counts[:4] + return (a+q, b+q, p-q) + + +def residual(counts): + return minus(TOTAL, old_address(counts)) + + +def profiles(limit=7): + """All nonnegative counts with r,s>=1 and total<=limit; no PSD filter.""" + def compositions(total, slots): + if slots == 1: + yield (total,) + return + for first in range(total + 1): + for rest in compositions(total-first, slots-1): + yield (first,) + rest + for length in range(2, limit+1): + for c in compositions(length-2, 6): + yield c[:4] + (c[4]+1, c[5]+1) + + +def target_splits(counts, target): + """None means every split has a support; otherwise return exact X=rR. + + Eliminate S=(M-X)/s from each bounded call subset. Integer arithmetic + forms (s*i-r*j) X = r*s*(target-old_subset)-r*j*M. Nonzero coefficients + pin X exactly; a zero coefficient is free iff the right side is zero. + Candidate membership checks signed rank-one only, before any sign test. + """ + r, s = counts[4:] + M = residual(counts) + pinned = set() + for old in product(*(range(c+1) for c in counts[:4])): + remainder = minus(target, old_address(old)) + for i in range(r+1): + for j in range(s+1): + denominator = s*i-r*j + numerator = minus(times(r*s, remainder), times(r*j, M)) + if denominator == 0: + if numerator == ZERO: + return None + else: + X = tuple(Fraction(x, denominator) for x in numerator) + if signed_rank_one(X) and signed_rank_one(minus(M, X)): + pinned.add(X) + return pinned + + +def classify(counts, targets=TARGETS): + constrained = [] + for target in targets: + values = target_splits(counts, target) + if values is not None: + if not values: + return set() + constrained.append(values) + return None if not constrained else set.intersection(*constrained) + + +def direct_support(counts, R, S, targets=TARGETS): + """Independent literal subset-sum route; no elimination or residual code.""" + sums = {ZERO} + for count, address in zip(counts, OLD+(R,S)): + sums = {plus(before, times(k, address)) for before in sums for k in range(count+1)} + return all(target in sums for target in targets) + + +def exact_total(counts, R, S): + total = ZERO + for count, address in zip(counts, OLD+(R,S)): + total = plus(total, times(count, address)) + return total + + +def inventory(): + free, pinned, empty, indefinite = [], [], [], [] + cases = list(profiles()) + require(len(cases) == 462 and len(set(cases)) == 462, 'complete count domain') + require({sum(c) for c in cases} == set(range(2,8)), 'all lengths 2 through 7') + for counts in cases: + M = residual(counts) + if determinant_twice(M) < 0: + indefinite.append(counts) + choices = classify(counts) + if choices is None: + free.append(counts) + require(positive_definite(M), 'every unconstrained family has definite residual') + elif not choices: + empty.append(counts) + else: + for X in sorted(choices): + R = times(Fraction(1,counts[4]),X) + S = times(Fraction(1,counts[5]),minus(M,X)) + # Positivity is an OUTPUT, never a candidate filter. + require(positive_rank_one(R) and positive_rank_one(S), 'pinned split positivity') + require(exact_total(counts,R,S) == TOTAL, 'pinned determinant identity') + require(direct_support(counts,R,S), 'pinned literal support corroboration') + pinned.append((counts,R,S)) + require(set(free)==EXPECTED_FREE, 'exact seven free families') + require(len(pinned)==32, 'exact signed pinned split inventory') + require(len(indefinite)==20 and all(c in empty for c in indefinite), + 'all twenty previously omitted indefinite residuals excluded by support') + return cases, free, pinned, empty, indefinite + + +def controls(): + checks=0 + # All four negative old directions, and non-coordinate rational negatives, + # really enter the candidate predicate; zero and rank-two matrices do not. + for v in OLD: + for scale in (Fraction(-1),Fraction(-2,3),Fraction(-7,2)): + require(signed_rank_one(times(scale,v)), 'negative frame silently filtered') + checks+=1 + for x,y,c in ((1,2,Fraction(-1,3)),(2,-3,Fraction(-5,7))): + physical=(c*x*x,c*y*y,c*x*y) + v=(physical[0]-physical[2],physical[1]-physical[2],2*physical[2]) + require(signed_rank_one(v) and trace(v)<0, 'negative rotated rank-one fixture') + checks+=1 + require(not signed_rank_one(ZERO),'zero rank-one mutant') + require(not signed_rank_one(plus(A,B)),'rank-two mutant') + checks+=2 + # Literal coordinate word at length nine: replace one A by 2A,-A. + # This shows the excluded negative premise is not globally impossible. + R,S=times(2,A),times(-1,A) + counts=(1,2,2,2,1,1) + require(exact_total(counts,R,S)==TOTAL and direct_support(counts,R,S), + 'nine-call signed positive control') + choices=classify(counts) + require(choices is None or R in choices,'nine-call signed split absent') + word=((R,0),(S,0),(P,0),(A,1),(Q,1),(B,2),(P,2),(B,3),(Q,3)) + for width in (4,6): + endpoint=[ZERO]*width + for address,role in word: + endpoint[role]=plus(endpoint[role],address) + require(tuple(endpoint)==TARGETS+(ZERO,)*(width-4),'signed coordinate word endpoint') + damaged=list(endpoint) + damaged[0]=minus(damaged[0],S) + require(tuple(damaged)!=TARGETS+(ZERO,)*(width-4),'omitted negative call mutant') + checks+=2 + checks+=2 + # Original eight-call endpoint survives; wrong target changes free list. + require(direct_support((1,1,2,2,1,1),A,B),'eight-call positive control') + require(classify((1,1,1,1,1,1),(times(9,A),)+TARGETS[1:]) != None, + 'changed target leaves free-family claim unchanged') + checks+=2 + # Direct support checks that the twenty indefinite residuals are truly + # allowed inputs. Rational split X=v v^T/(v^T M^-1 v) can have either sign. + signed_cases=accepted=0 + for counts in profiles(): + M=residual(counts) + if determinant_twice(M)>=0: + continue + m=matrix(M); d=m[0][0]*m[1][1]-m[0][1]*m[1][0] + for x,y in ((1,0),(0,1),(1,1),(1,-1),(1,2),(2,1),(1,-2),(2,-1)): + denominator=m[1][1]*x*x-2*m[0][1]*x*y+m[0][0]*y*y + if not denominator: + continue + c=d/denominator + physical=(c*x*x,c*y*y,c*x*y) + X=(physical[0]-physical[2],physical[1]-physical[2],2*physical[2]) + Y=minus(M,X) + require(signed_rank_one(X) and signed_rank_one(Y),'indefinite split parameterization') + require(trace(X)*trace(Y)<0,'indefinite split needs opposite signs') + R=times(Fraction(1,counts[4]),X);S=times(Fraction(1,counts[5]),Y) + signed_cases+=1 + if direct_support(counts,R,S):accepted+=1 + require(signed_cases>0 and accepted==0,'indefinite direct-support control') + return checks,signed_cases + + +def run(): + cases,free,pinned,empty,indefinite=inventory() + checks,signed_cases=controls() + serial={'free':free,'pinned':[(c,tuple(map(str,R)),tuple(map(str,S))) for c,R,S in pinned], + 'empty':empty,'indefinite':indefinite} + digest=sha256(json.dumps(serial,sort_keys=True,separators=(',',':')).encode()).hexdigest() + result={'profiles':len(cases),'free_families':len(free),'pinned_splits':len(pinned), + 'empty_profiles':len(empty),'indefinite_profiles':len(indefinite), + 'negative_pinned_splits':0,'signed_controls':signed_cases,'controls':checks, + 'inventory_sha256':digest} + print('PASS_SIGNED_TWO_FRAME_SUPPORT '+json.dumps(result,sort_keys=True)) + return result + + +if __name__=='__main__': + run() diff --git a/research/bit-two-signed-frame-floor/verify.py b/research/bit-two-signed-frame-floor/verify.py new file mode 100644 index 0000000000..d1a76d2914 --- /dev/null +++ b/research/bit-two-signed-frame-floor/verify.py @@ -0,0 +1,149 @@ +"""Source binding and elementary sign-reduction checks (standard library). + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +The mathematical dependencies are PR6111 and PR6079, not executed here. +""" +from collections import Counter +from fractions import Fraction as F +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +A, B, P, Q = ((F(1),F(0),F(0)), (F(0),F(1),F(0)), + (F(1,2),F(1,2),F(1,2)), (F(1,2),F(1,2),F(-1,2))) +OLD = (A,B,P,Q) # Physical entries (m11,m22,m12), independent of census basis. + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(x,y): + return tuple(a+b for a,b in zip(x,y)) + + +def scale(c,x): + return tuple(c*a for a in x) + + +def det(x): + return x[0]*x[1]-x[2]*x[2] + + +def rank_one(c,x,y): + return (c*x*x,c*y*y,c*x*y) + + +TARGETS = tuple(add(x,y) for x in (A,B) for y in (P,Q)) + + +def bind_sources(): + manifest = json.loads((PACKAGE/'SOURCES.json').read_text()) + declared = set(json.loads((PACKAGE/'VERIFY.json').read_text())['inputs']) + rows = [r for r in manifest['files'] if r['usage']=='input'] + require(len(rows)==2 and {r['path'] for r in rows}==declared, 'two theorem source pins') + for row in rows: + data = (ROOT/row['path']).read_bytes() + require(sha256(data).hexdigest()==row['sha256'], 'changed theorem source: '+row['path']) + return len(rows) + + +def elementary_counts(): + counts = Counter() + for old in product(range(6),repeat=4): + n=sum(old) + if n>5: + continue + M=(F(4),F(4),F(0)) + for c,frame in zip(old,OLD): + M=add(M,scale(-c,frame)) + d,e=old[0]-old[1],old[2]-old[3] + require(4*det(M)==(8-n)**2-d*d-e*e,'residual determinant identity') + require(M[0]+M[1]==8-n,'positive residual trace') + multiplicities=sum(1 for r in range(1,8-n) for s in range(1,8-n-r)) + if det(M)>0: + counts['definite']+=multiplicities + elif det(M)<0: + require(n==5 and abs(d)+abs(e)==5,'indefinite two-direction reduction') + require(not(old[0] and old[1]) and not(old[2] and old[3]),'no opposite old directions') + E=OLD[0 if old[0] else 1] + G=OLD[2 if old[2] else 3] + # Solve ell(E)=ell(G)=0, ell(I)=1 in physical coordinates. + c11=F(0) if E==A else F(1) + c22=1-c11 + c12=-F(1,2)/G[2] + ell=lambda x:c11*x[0]+c22*x[1]+c12*x[2] + require(ell(E)==ell(G)==0 and ell(add(A,B))==1,'projected-support functional') + require(sorted(ell(t) for t in TARGETS)==[0,1,1,2],'projected targets') + for rho in (F(1),F(3)): + require(F(2) not in {F(0),rho,4-rho,F(4)},'all possible rho admitting one') + counts['indefinite']+=multiplicities + else: + matched=False + for i,E in enumerate(OLD): + perpendicular=i^1 + other=(2,3) if i<2 else (0,1) + patterns=[] + for kind in range(3): + c=[0]*4 + c[i]=4 if kind<2 else 3 + if kind==1:c[perpendicular]=1 + if kind==2: + c[other[0]]=c[other[1]]=1 + patterns.append(tuple(c)) + if old not in patterns: + continue + require(not matched,'unique singular profile classification') + matched=True + character=(lambda x:2*x[2]) if i<2 else (lambda x:x[0]-x[1]) + require(character(E)==character(OLD[perpendicular])==0,'kill whole added line') + require(all(abs(character(t))==1 for t in TARGETS),'four detected targets') + if old==patterns[2]: + require(sum(c for c,x in zip(old,OLD) if character(x))==2,'two detected calls') + counts['singular_character']+=multiplicities + else: + require(all(character(x)==0 for c,x in zip(old,OLD) if c),'span control') + counts['singular_span']+=multiplicities + require(matched,'unclassified singular profile') + require(dict(counts)=={'definite':422,'indefinite':20,'singular_span':16,'singular_character':4}, + 'complete elementary partition') + return dict(counts) + + +def geometry_controls(): + checked=0 + vectors=((1,0),(0,1),(1,1),(1,-1),(1,2),(2,-3)) + for u,v,c,t in product(vectors,vectors,(F(-2),F(-1,3),F(2,5),F(3)),(F(-3),F(-1,5),F(1,2),F(4))): + X=rank_one(c,*u);Y=rank_one(t,*v);M=add(X,Y) + require(det(M)==c*t*(u[0]*v[1]-u[1]*v[0])**2,'rank-one sum determinant') + if det(M)>0 and M[0]+M[1]>0: + require(c>0 and t>0,'positive-definite sum forces signs') + if det(M)==0: + require(u[0]*v[1]==u[1]*v[0],'singular sum forces common line') + checked+=1 + # Three summands do not obey the two-summand sign lemma. + require(add(add(scale(-1,A),scale(2,A)),B)==add(A,B),'three-frame boundary') + return checked + + +def main(): + sources=bind_sources() + partition=elementary_counts() + geometry=geometry_controls() + path=PACKAGE/'independent.py' + namespace={'__name__':'independent_signed_support'} + # Execute current local source, never a stale .pyc. + exec(compile(path.read_bytes(),str(path),'exec'),namespace) + result=namespace['run']() + require(result['profiles']==sum(partition.values()),'independent total agrees') + print('PASS_TWO_SIGNED_FRAME_REDUCTION '+json.dumps({ + 'sources':sources,'partition':partition,'rank_one_sum_controls':geometry, + 'three_frame_boundary':1,'scope':'signed reduction; positive theorem inherited; no new kappa'},sort_keys=True)) + + +if __name__=='__main__': + main()