diff --git a/research/p104-contractive-gram-deflation/MISSING.json b/research/p104-contractive-gram-deflation/MISSING.json new file mode 100644 index 0000000000..d5f76681db --- /dev/null +++ b/research/p104-contractive-gram-deflation/MISSING.json @@ -0,0 +1,25 @@ +{ + "source_pr": 6166, + "source_author": "Matarener", + "source_head": "096938513138868f0ed27639061f1a5054900f96", + "source_path": "research/p104-carrier-code-uniqueness/e8/ports-d8.md", + "meaning": "Omitted root lines in the cited orthonormal D8 coordinates; doubled coordinates are these signs. Coordinate identification is a cited premise, not independently replayed.", + "signs": [ + "+++++---", + "++++-+++", + "++-----+", + "--++---+", + "++-++-+-", + "-++---+-", + "+--+--+-", + "-+-++-++", + "-+----++", + "+-+-+-++", + "+++-++++", + "+---+--+", + "++---+--", + "-+-+++-+", + "----+++-", + "-++-+---" + ] +} diff --git a/research/p104-contractive-gram-deflation/PROOF.md b/research/p104-contractive-gram-deflation/PROOF.md new file mode 100644 index 0000000000..2cf92ff47f --- /dev/null +++ b/research/p104-contractive-gram-deflation/PROOF.md @@ -0,0 +1,114 @@ +# A sharp error floor for contractive P104 Gram deflation + +## Contract and theorem + +Let P consist of the 56 unoriented D8 root lines e_i +/- e_j in R^8, +and any proper subset of the 64 half-spin root lines of one fixed parity. +Choose one root r_i of squared length 2 on every retained line. Let R +have these roots as rows and let K=RR^T/2. + +A contractive rank-seven approximation means + + K_D = R D R^T/2, + D real symmetric, 0 <= D <= I in positive-semidefinite order, + rank D <= 7. + +Then the exact minimum of max_{i,j}|K_ij-(K_D)_ij| is 1/4. Any omitted +half-spin root q gives an attaining matrix D=I-qq^T/2. It is an orthogonal +rank-seven projector. If the half-spin subset is empty the same witness +works; only one omitted half-spin root is required. + +This is a scoped proof about coefficient error. It does not give a lower +bound for unrestricted rank-seven matrices, nonsymmetric approximants, +noncontractive approximants, nonlinear processing, or masked exactness. + +## The D8 direction bound + +For every unit vector u in R^8, + + max_{r in D8} |r dot u|^2 >= 1/2. + +To prove it, arrange the absolute coordinates as x_1>=x_2>=...>=x_8>=0 +and put s=x_1+x_2. The largest absolute D8 inner product is s. Since +the remaining coordinates are at most x_2, + + 1 = sum x_i^2 <= (s-x_2)^2 + 7*x_2^2 <= 2*s^2. + +The last bound follows because this convex quadratic on 0<=x_2<=s/2 +is bounded by the larger endpoint value, max{s^2,2*s^2}. This proves +the direction bound. It is an elementary root-geometry inequality, not a +new general rank-approximation theorem. + +## Lower bound for every admissible D + +The rank cap gives a unit vector u in ker D. Symmetry and 0<=D<=I imply + + I-D >= u u^T. + +For example, use an orthonormal eigenbasis with u as a zero-eigenvalue +vector of D. In that basis I-D-u*u^T has only nonnegative eigenvalues. +Consequently the coefficient error E=K-K_D is positive semidefinite and + + E_ii = r_i^T (I-D) r_i /2 >= (r_i dot u)^2/2. + +The retained D8 subsystem supplies an i with E_ii>=1/4. A diagonal entry +already gives the required lower bound on maximum absolute entry. This +argument covers all real admissible D, not just rational or sampled D. + +## Exact attaining deflation + +Choose a half-spin root q whose line is omitted. It has squared norm 2, +so D=I-qq^T/2 is symmetric, idempotent, positive semidefinite and rank 7. +It lies between zero and I. Its error is + + E_ij = (r_i dot q)(r_j dot q)/4. + +For a D8 root the inner product with q is in {-1,0,1}. For another +half-spin root of the same parity, the sign patterns differ in an even +number of coordinates. Unless their lines agree, the inner product is +also in {-1,0,1}. The line of q is absent, so every retained root has +inner product at most one in absolute value. Thus every error entry is +at most 1/4. Some D8 root has inner product of absolute value one, so +the maximum is exactly 1/4. This proves sharpness constructively. + +## P104 binding and meaning for precision + +Matarener's PR6166 at 096938513138868f0ed27639061f1a5054900f96 identifies +the selected P104 ports with all 56 D8 lines and 48 half-spin lines in +orthonormal coordinates. Its e8/ports-d8.md lists the sixteen omitted +lines. That coordinate identification is a cited predecessor premise, +not a result independently checked here. MISSING.json retains just those +factual signs so the new deflation witnesses replay without the pending PR. +No predecessor certificate, code uniqueness, single-word weight, generalized +support weight, native operator or supplier replay is run. + +The coefficient convention K=RR^T/2 is the retained P104 Gram-channel +convention from Rohan Arun's PR1972 and Chafik Boukhalfa's PR1991 native +channel, with its credited root/frame lineage. This theorem introduces +contractive approximation of that channel as a changed mechanism. + +For every admissible D there is an input x=B e_i such that the i-th output +bias is at least |B|/4. Thus the approximation error is not o(|B|), uniformly +over arbitrary inputs. Increasing the arithmetic precision cannot remove +this mathematical bias. The attaining matrices even have dyadic rational +entries. Any supplier using this deletion must explicitly correct the +residual or justify a different consumer/error contract. No correction +cost is declared free and no complete signed-moment gain is claimed. + +The full scalar word may have other routes and cancellations. The theorem +only concerns replacing this Gram block by K_D while retaining the other +terms and demanding entrywise accuracy. It does not exclude changing the +side correction, targets, source encoding, masking or complete circuit. + +## Evidence + +The standard-library verifier constructs this root set from the retained +sign list, checks all sixteen rank-seven projectors by integer arithmetic, +and enumerates every coefficient of each new error matrix. It checks the +D8 inequality on the 6,560 nonzero vectors in {-1,0,1}^8. Those are finite +corroborations of the written proof, not extrapolations to arbitrary D. +The verifier also rejects wrong parity, duplicate missing lines and a +retained-root deflation falsely claimed to attain error 1/4. Normal and +optimized runs retain explicit exception checks. Source hashes bind the +generated receipt. Independent human and formal proof-kernel review remain +unclaimed. diff --git a/research/p104-contractive-gram-deflation/README.md b/research/p104-contractive-gram-deflation/README.md new file mode 100644 index 0000000000..d3a11f74d5 --- /dev/null +++ b/research/p104-contractive-gram-deflation/README.md @@ -0,0 +1,105 @@ +# Sharp error floor for contractive P104 Gram deflation + +Discarding one real carrier mode through a positive contractive approximation +of the P104 Gram channel has an exact maximum coefficient-error floor of +**1/4**. Projecting away any omitted half-spin root direction attains it. +This is a scoped obstruction with a written proof and exact finite witnesses. +No new kappa or physical supplier is claimed. + +Write R for the retained roots of squared norm 2 and K=RR^T/2. The theorem +covers K_D=RDR^T/2 with D real symmetric, 0<=D<=I, and rank D<=7. Its lower +bound uses only the retained D8 subsystem and applies to every admissible +real D. Its upper bound is the explicit dyadic projector D=I-qq^T/2 for an +omitted half-spin root q. [PROOF.md](PROOF.md) gives both arguments. + +For some input B e_i every such approximation has output bias at least +|B|/4. Increasing arithmetic precision cannot remove that fixed linear +bias. This blocks treating a contractive one-mode deletion as vanishing +roundoff while keeping the rest of the Gram decomposition fixed. A changed +side correction or consumer must account for the residual. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-contractive-gram-deflation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/p104-contractive-gram-deflation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-contractive-gram-deflation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-contractive-gram-deflation --check-source-history +``` + +The direct marker is `PASS_P104_CONTRACTIVE_GRAM_DEFLATION`. The registered +replay prints `PASS_REGISTERED_RESEARCH_PACKAGE`. A clean CPython 3.12 can +replace the absolute interpreter path. Replay reads without writing files. +The optional `--output PATH` generates a new receipt outside the checkout; +RESULT.json is generated and bound to every other package file's hashes. + +The verifier enumerates 173,056 entries of sixteen new error matrices, +checks the sixteen exact rank-seven projectors and 6,560 integer-direction +fixtures, and retains three rejection controls. These finite checks +corroborate the written all-real-D proof. They do not recheck predecessors. + +## Scope, sources and overlap + +The original coverage-law-change question is changed to contractive approximate +decoding. The connection to the current complex bottleneck is a possible +carrier-mode saving which exact decoding excludes. This result computes its +unavoidable residual before any native or caller expansion. It supplies no +complete signed invoice or card-level supplier admission. + +Base main is `3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision 8. +The selected frontier is unchanged. Historical provenance pins are in +SOURCES.json. The mathematical statement itself covers all D8 root lines +plus any proper subset of one half-spin shell. + +For the P104 application, Matarener's [PR6166](https://github.com/CrocSwap/integer-mult-bounds/pull/6166) +at `096938513138868f0ed27639061f1a5054900f96` supplies its orthonormal D8 +coordinate identification and sixteen omitted lines. [MISSING.json](MISSING.json) +retains those factual coordinates. This identification is a cited premise, +not independently verified here. Its ternary uniqueness, minimum weight and +code-support questions are separate. The new result concerns real contractive +approximation and introduces no question from that source's open-question list. + +Rohan Arun's PR1972 and Chafik Boukhalfa's PR1991 supply the retained Gram +channel convention. Their native/operator results are cited, not replayed. +Ali Romman's PR5526 concerns Clifford-history error versus paid returns; +it is a different approximation contract. The present result neither uses +nor checks its call-cap or native tensor arguments. + +## Limits and engineering notes + +Unrestricted rank-seven matrices, nonsymmetric or noncontractive filters, +masked-entry accuracy, changed source encodings and nonlinear consumers +remain outside the theorem. The bias might be corrected elsewhere in a new +word. No restoration, ordinary-cost, native, physical caller, precision/tape, +compiler, BIT, outer, Lean or full multiplication-theorem replay is supplied. +Independent human and formal proof-kernel review are unclaimed. + +The verifier has bounded loops, no recursion, functions below sixty lines +and explicit failure checks. Standard-library collection allocation is a +managed-runtime deviation from static allocation; +root tables have at most 120 rows of eight integers, and one error histogram +has at most 10,816 entries counted into integer bins. No shared code or +repository-wide diagnostics configuration is changed. + +## Open next questions + +- Can a noncontractive or nonsymmetric rank-seven factor beat 1/4 in maximum + entry error? It would escape the positive-error argument. Start with an + explicit rational factor and certify every coefficient; its physical + realization and stability would still need a separate bill. +- Can a changed side correction absorb the explicit rank-one residual with + a favorable full invoice? Start from one omitted-root projector and track + its residual through an actual scalar word. No such caller is supplied. + +## Credit + +This proof and verifier were produced by Nick Petalas. Matarener retains the +P104 D8 coordinates and omitted-root list. Rohan Arun, Chafik Boukhalfa and +their retained native/root/frame predecessors retain the Gram-channel +construction. Ali Romman, DreamingOfClouds, Cinna Davis, Pierre-Loic Doulcet, +icekylinx, zxv, Jacob Alan Sussman and the retained P104/helper/compiler/BIT +contributors retain their source results. Root geometry, orthogonal +projection and positive-semidefinite order are classical. No general +literature-priority claim is made. Apache-2.0. diff --git a/research/p104-contractive-gram-deflation/RESULT.json b/research/p104-contractive-gram-deflation/RESULT.json new file mode 100644 index 0000000000..f70b278a4a --- /dev/null +++ b/research/p104-contractive-gram-deflation/RESULT.json @@ -0,0 +1,314 @@ +{ + "schema_version": 1, + "claim_type": "scoped proof", + "sharp_max_entry_error": "1/4", + "d8_root_lines": 56, + "retained_root_lines": 104, + "omitted_root_witnesses": 16, + "witnesses": [ + { + "omitted_root_doubled": [ + 1, + -1, + -1, + -1, + 1, + -1, + -1, + 1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1344, + "0": 8112, + "16": 1360 + } + }, + { + "omitted_root_doubled": [ + 1, + -1, + -1, + 1, + -1, + -1, + 1, + -1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1320, + "0": 8112, + "16": 1384 + } + }, + { + "omitted_root_doubled": [ + 1, + -1, + -1, + 1, + -1, + 1, + 1, + 1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1280, + "0": 8112, + "16": 1424 + } + }, + { + "omitted_root_doubled": [ + 1, + -1, + -1, + 1, + 1, + 1, + -1, + 1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1224, + "0": 8112, + "16": 1480 + } + }, + { + "omitted_root_doubled": [ + 1, + -1, + 1, + -1, + -1, + -1, + 1, + -1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1302, + "0": 8112, + "16": 1402 + } + }, + { + "omitted_root_doubled": [ + 1, + -1, + 1, + -1, + -1, + 1, + -1, + -1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1280, + "0": 8112, + "16": 1424 + } + }, + { + "omitted_root_doubled": [ + 1, + -1, + 1, + -1, + 1, + -1, + 1, + 1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1224, + "0": 8112, + "16": 1480 + } + }, + { + "omitted_root_doubled": [ + 1, + -1, + 1, + 1, + 1, + 1, + -1, + -1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1014, + "0": 8112, + "16": 1690 + } + }, + { + "omitted_root_doubled": [ + 1, + 1, + -1, + -1, + -1, + -1, + -1, + 1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1302, + "0": 8112, + "16": 1402 + } + }, + { + "omitted_root_doubled": [ + 1, + 1, + -1, + -1, + -1, + 1, + -1, + -1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1254, + "0": 8112, + "16": 1450 + } + }, + { + "omitted_root_doubled": [ + 1, + 1, + -1, + -1, + 1, + 1, + 1, + -1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1110, + "0": 8112, + "16": 1594 + } + }, + { + "omitted_root_doubled": [ + 1, + 1, + -1, + 1, + 1, + -1, + 1, + -1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 1014, + "0": 8112, + "16": 1690 + } + }, + { + "omitted_root_doubled": [ + 1, + 1, + 1, + -1, + 1, + 1, + 1, + 1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 840, + "0": 8112, + "16": 1864 + } + }, + { + "omitted_root_doubled": [ + 1, + 1, + 1, + 1, + -1, + -1, + -1, + 1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 960, + "0": 8112, + "16": 1744 + } + }, + { + "omitted_root_doubled": [ + 1, + 1, + 1, + 1, + -1, + 1, + 1, + 1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 774, + "0": 8112, + "16": 1930 + } + }, + { + "omitted_root_doubled": [ + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1 + ], + "nonzero_mode_entries": 52, + "error_numerators_over_64": { + "-16": 774, + "0": 8112, + "16": 1930 + } + } + ], + "explicit_error_entries": 173056, + "integer_direction_fixtures": 6560, + "controls": [ + "wrong_half_spin_parity", + "duplicate_omitted_line", + "deflating_a_retained_root_is_worse" + ], + "source_sha256": { + "README.md": "5643af3d891e2731237c0f8a4ae97d5ae0515b03d369e835fbf80cc612821415", + "PROOF.md": "8e44fe3d11d777535131e0a4c7cdde8fbc4c0d2b69254e587432c71ce39a61a6", + "verify.py": "589f422045492d2a39bc6df38b83881cb4b6c141c83442ae776ae24eec106142", + "MISSING.json": "9ddfcf087912e02c46722d5a82eea5f1221a4a33d5037a0d90d392dfcd3c06d4", + "TASK.json": "74fce99e9bd12013d84f35ca7a00a926e49087dc6b8304e87d560dcc6799ec91", + "VERIFY.json": "d7726cb7124cf6b3f26a6fc4e8019beb8165c9a4a76996bdbe51f1972c2db188", + "SOURCES.json": "72a81605262ddff1dd112b67e8c5c505c45ffb3f22c5a07869e849c4edea5b7a" + } +} diff --git a/research/p104-contractive-gram-deflation/SOURCES.json b/research/p104-contractive-gram-deflation/SOURCES.json new file mode 100644 index 0000000000..5a49c4bf38 --- /dev/null +++ b/research/p104-contractive-gram-deflation/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/p104-native-channel/README.md", + "usage": "provenance", + "git_blob": "f187d1ac0b7792d08d2dedf4561380b798e541b5", + "sha256": "ef874f86415c98b553bda9199d5f8f2f7a4dd4f6a23e53712c3c1f7268ec5b23" + }, + { + "path": "research/p104-native-channel/PROOF.md", + "usage": "provenance", + "git_blob": "a69311b74f74a2f8e8f411c1451baacd9bacddce", + "sha256": "5d743145d389ffdfaffc66096fa7e32c7155b18f73d74755403151d0435bb94c" + } + ] +} diff --git a/research/p104-contractive-gram-deflation/TASK.json b/research/p104-contractive-gram-deflation/TASK.json new file mode 100644 index 0000000000..d5ac2a4c81 --- /dev/null +++ b/research/p104-contractive-gram-deflation/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact maximum-entry error floor for real symmetric positive contractive rank-seven approximation of the D8 plus partial half-spin Gram channel, with the P104 coordinate identification cited as a predecessor premise.", + "scope_change_reason": "Original contractive approximation question replacing exact Gram decoding with a positive semidefinite rank-seven filter. This is a side-result scope change, not an audit or an answer to a predecessor open question.", + "bottleneck_link": "The complex supplier binds. A proposed way to reduce carrier modes is to allow approximate Gram decoding and rely on precision. The sharp 1/4 bias floor rules out vanishing error for this contractive deletion model while leaving other approximation and correction contracts open. No complete physical invoice is supplied.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified sharp obstruction; do not extend to other approximation alphabets or a physical search.", + "outcome": "negative-result", + "evidence": "PROOF.md; generated RESULT.json with sixteen exact projectors, all 173056 error entries, 6560 finite integer-direction fixtures and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a nonsymmetric or noncontractive rank-seven factor beat maximum-entry error 1/4?", + "why_it_matters": "It would change the positivity hypothesis responsible for this obstruction.", + "first_step": "Give one exact rational factor and certify all Gram coefficient errors.", + "blocked_by": "No such factor or physical realization is supplied." + }, + { + "question": "Can a changed side correction cheaply absorb the explicit rank-one residual?", + "why_it_matters": "An explicit residual need not be a complete supplier obstruction.", + "first_step": "Track one omitted-root residual through an actual changed scalar word and price the full invoice.", + "blocked_by": "A physical caller and complete accounting are absent." + } + ] +} diff --git a/research/p104-contractive-gram-deflation/VERIFY.json b/research/p104-contractive-gram-deflation/VERIFY.json new file mode 100644 index 0000000000..565ed97cf5 --- /dev/null +++ b/research/p104-contractive-gram-deflation/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All new deflation coefficient entries, integer projector identities, D8 direction fixtures and explicit failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same generated receipt and failure controls with assertions disabled." + } + ] +} diff --git a/research/p104-contractive-gram-deflation/verify.py b/research/p104-contractive-gram-deflation/verify.py new file mode 100644 index 0000000000..73e57acbde --- /dev/null +++ b/research/p104-contractive-gram-deflation/verify.py @@ -0,0 +1,144 @@ +#!/usr/bin/env python3 +"""Exact contractive Gram deflation certificate; standard library only.""" + +import argparse +import hashlib +import itertools +import json +from collections import Counter +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(vector): + need(len(vector) == 8 and any(vector), "nonzero eight-coordinate root") + first = next(x for x in vector if x) + return tuple(x if first > 0 else -x for x in vector) + + +def dot(left, right): + return sum(x * y for x, y in zip(left, right, strict=True)) + + +def roots_and_missing(data): + signs = data["signs"] + need(isinstance(signs, list) and len(signs) == 16, "sixteen omitted lines") + missing = set() + for text in signs: + need(isinstance(text, str) and len(text) == 8 + and set(text) <= {"+", "-"}, "invalid sign row") + need(text.count("-") % 2 == 1, "half-spin parity") + missing.add(canonical(tuple(1 if s == "+" else -1 for s in text))) + need(len(missing) == 16, "duplicate omitted line") + d8 = set() + for i, j in itertools.combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + d8.add(tuple(row)) + half = {canonical((1, *tail)) for tail in itertools.product((-1, 1), repeat=7) + if tail.count(-1) % 2 == 1} + need(len(d8) == 56 and len(half) == 64, "root-shell sizes") + need(missing <= half, "omitted line outside half shell") + ports = sorted(d8 | (half - missing)) + need(len(ports) == 104 and all(dot(r, r) == 8 for r in ports), "port norms") + return sorted(d8), ports, sorted(missing) + + +def projector_check(q): + # Coordinates are doubled: D = I - q*q^T/8. + matrix = [[8 * (i == j) - q[i] * q[j] for j in range(8)] for i in range(8)] + need(dot(q, q) == 8, "projector normalization") + need(all(sum(matrix[i][k] * matrix[k][j] for k in range(8)) + == 8 * matrix[i][j] for i in range(8) for j in range(8)), + "idempotent projector") + need(all(dot(row, q) == 0 for row in matrix), "projector kernel") + need(sum(matrix[i][i] for i in range(8)) == 56, "rank-seven trace") + + +def witness(q, ports): + projector_check(q) + products = [dot(r, q) for r in ports] + histogram = Counter() + for left in products: + for right in products: + histogram[left * right] += 1 + # E_ij = numerator/64, for these doubled root coordinates. + need(max(abs(n) for n in histogram) == 16, "sharp quarter error") + need(set(histogram) <= {-16, 0, 16}, "coefficient error alphabet") + return {"omitted_root_doubled": list(q), "nonzero_mode_entries": sum(x != 0 for x in products), + "error_numerators_over_64": {str(k): histogram[k] for k in sorted(histogram)}} + + +def inequality_fixtures(d8): + count = 0 + for vector in itertools.product((-1, 0, 1), repeat=8): + norm = dot(vector, vector) + if norm == 0: + continue + largest = max(abs(dot(root, vector)) for root in d8) + # Actual D8 roots are root/2. No square roots enter this test. + need(largest * largest >= 2 * norm, "D8 unit-direction floor") + count += 1 + return count + + +def controls(data, ports): + invalid_parity = {**data, "signs": ["++++++++", *data["signs"][1:]]} + duplicate = {**data, "signs": [data["signs"][0], *data["signs"][:-1]]} + rejected = [] + for name, mutant in (("wrong_half_spin_parity", invalid_parity), + ("duplicate_omitted_line", duplicate)): + try: + roots_and_missing(mutant) + except ValueError: + rejected.append(name) + else: + raise ValueError("invalid input accepted: " + name) + try: + witness(ports[0], ports) + except ValueError as error: + need(str(error) == "sharp quarter error", "retained-root control diagnostic") + rejected.append("deflating_a_retained_root_is_worse") + else: + raise ValueError("retained-root deflation accepted at quarter error") + return rejected + + +def compute(package): + data = json.loads((package / "MISSING.json").read_text()) + d8, ports, missing = roots_and_missing(data) + witnesses = [witness(q, ports) for q in missing] + files = ("README.md", "PROOF.md", "verify.py", "MISSING.json", "TASK.json", "VERIFY.json", "SOURCES.json") + return {"schema_version": 1, "claim_type": "scoped proof", "sharp_max_entry_error": "1/4", + "d8_root_lines": len(d8), "retained_root_lines": len(ports), + "omitted_root_witnesses": len(witnesses), "witnesses": witnesses, + "explicit_error_entries": len(witnesses) * len(ports) ** 2, + "integer_direction_fixtures": inequality_fixtures(d8), + "controls": controls(data, ports), + "source_sha256": {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in files}} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="write a generated receipt outside checkout") + args = parser.parse_args() + package = Path(__file__).resolve().parent + result = compute(package) + if args.output is not None: + need(not args.output.resolve().is_relative_to(package.parents[1]), + "receipt output must be outside checkout") + args.output.write_text(json.dumps(result, indent=2) + "\n") + else: + expected = json.loads((package / "RESULT.json").read_text()) + need(result == expected, "generated receipt differs") + print("PASS_P104_CONTRACTIVE_GRAM_DEFLATION " + json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()