Prove production Gaussian positivity and retained matrix perturbation

research/gaussian-production-matrix-guard/PROOF.md

@@ -0,0 +1,113 @@
+# Production guards imply positive weights and a retained-band error bound
+
+JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0.
+This is a source-relative written proof, not a formal proof-kernel check or
+independent human review. The live scientific source is canonical main
+721c03822c421b7f7fcbb2598993b947c4d88419; physical Gaussian code last changed at
+7ab67b4a84d28cd562b9711aa315ca5b47822b37. No predecessor bytes are changed.
+
+## Precise dependency and claim
+
+Use the scalar theorem of [PR6085](https://github.com/CrocSwap/integer-mult-bounds/pull/6085)
+at 9fc80f1db55d4939c7b53c0799e6840cce35fbf8, PROOF.md in
+`research/encoded-gaussian-directed-coefficient-audit`: for P,F>=1 and rational
+0<=f<=F, the unchanged encoded coefficient routine returns a dyadic c with
+0<=c<=exp(-pi*f) and exp(-pi*f)-c<2 eta, eta=2^-P. Its Axis argument-domain
+lemma is cited but the particular arguments used here are checked below.
+This is a mathematical dependency, not imported pending receipt/code and not
+an independently repeated scalar audit. Exact Count/Rational arithmetic and
+its ownership semantics remain the retained runtime contract.
+
+For every canonical parameter tuple admitted by ProductionPlan and the Axis
+layout guards, let H be the entries prescribed by Axis.matrix_entry, before
+its separate validate_rows acceptance check. Define N_w on residues 0..s-1:
+diagonal one; zero when neither signed cyclic displacement has modulus <=w;
+on every other position choose the unique such displacement delta and set
+
+    (N_w)ij = exp(-pi*u*((rho*delta+beta_i)^2-beta_j^2)),
+    rho=t/s, theta=rho-1, q_j=floor(rho*j+1/2), beta_j=rho*j-q_j.
+
+Then every prepared similarity weight is >2^(-8p-1) and
+
+    ||H-N_w||_infinity < p*2^(16p+4)*eta < p*2^(16p+7)*eta.
+
+This concludes one retained-band perturbation implication. It does not prove
+that Axis.validate_rows succeeds for every tuple, the ideal infinite-matrix
+tail bound, global ideal rowgap, inverse/LU validity, full production page,
+online solve, tensor/CRT admission, physical total cost or a new kappa.
+
+## Production inequalities and positive weights
+
+ProductionPlan checks p>=101, s<t<2s, u>=ceil(log2(8p)), ud<=p,
+4d(t-s)>s, (2d-1)(t-s)<s, and d>4w+2. It computes P=32768p
+and w=ceil(sqrt(16p/u))+2: the loop seeks the least integer whose square
+is >=ceil(16p/u), equivalent to >=16p/u. Remaining width/window/halo guards
+restrict this domain further. Axis separately checks 2w<s.
+
+The half-up nearest convention gives -1/2<=beta_j<1/2, also at ties.
+Thus F_j=u*(1/4-beta_j^2)/theta lies in [0,u/(4theta)] and
+
+    F_j < ud <= p,    0<a_j=exp(-pi*F_j)<=1.
+
+Using pi<4 and e<4 gives exp(pi*p)<exp(4p)<2^(8p), hence a_j>2^-8p.
+These classical loose inequalities suffice; no numerical pi oracle is used.
+The prepared argument ceiling is >=u/(4theta), so the scalar theorem applies.
+Reflection reuse preserves a_j: q_{s-j}=t-q_j off ties, whereas both beta
+values equal -1/2 at a half-integer tie. Their squared offsets agree.
+
+Since P=32768p>8p+2, 2eta<2^(-8p-1). Consequently
+
+    a_hat_j > a_j-2eta > 2^(-8p-1) > 0.
+
+This proves the prepare_weights positivity guard from production parameters
+and the scalar contract, rather than assuming it because a finite page passed.
+
+## The original-coordinate identity and physical cuts
+
+For a direct pair delta=j-i with equal phase q_i-i=q_j-j,
+q_j-q_i=delta and beta_j-beta_i=theta*delta. Therefore
+
+    F_i + u*rho*delta^2 - F_j
+      = u*((rho*delta+beta_i)^2-beta_j^2).
+
+It follows exactly that a_i*G_delta/a_j=(N_w)ij, where
+G_delta=exp(-pi*u*rho*delta^2). This is the original-coordinate entry;
+the bare Toeplitz kernel G_delta is not interchangeable with it.
+
+Axis takes that ratio only when raw displacement is direct AND phases agree.
+Every wrapped pair takes the coefficient branch, even if a lifted phase label
+would agree across a physical-period seam. Every direct different-phase pair
+also takes it. For these nonzero integral delta,
+|rho*delta+beta_i|>=rho-1/2>1/2>=|beta_j|, so the decay argument is positive.
+It is at most u*(rho*w+1/2)^2, covered by argument_bound. The kernel argument
+u*rho*delta^2 is covered too, since rho>1. Thus the scalar theorem applies to
+all retained coefficient branches. The diagonal bypass returns exactly one;
+nonretained positions return exactly zero, both matching N_w without error.
+
+The definition of N_w deliberately uses the source's cyclic displacement and
+physical cut. Identifying it with a particular infinite-periodized ideal
+matrix requires an additional tail/comparison theorem; it is not implicit here.
+
+## Ratio error and row sum
+
+For a same-cell entry write x=a_i, y=a_j, g=G_delta and put hats on the
+rounded values. All lie in [0,1], y>2^-8p and y_hat>2^(-8p-1).
+The directed scalar contract gives each scalar difference <2eta. Consequently
+
+    |x_hat*g_hat-x*g| <= |x_hat-x|*g_hat + x*|g_hat-g| < 4eta,
+    |x_hat*g_hat/y_hat-x*g/y|
+      <= |x_hat*g_hat-x*g|/y_hat + x*g*|y-y_hat|/(y*y_hat)
+      < (2^(8p+3)+2^(16p+2))*eta
+      < 2^(16p+4)*eta.
+
+The last inequality holds for p>=1. No additional rounding occurs: the actual
+consumer uses exact Rational.times followed by Rational.over. This error need
+not be downward, since dividing by a downward denominator can increase it.
+Other retained off-diagonal entries have error <2eta, hence obey the same cap.
+Since 2w<s there are exactly 2w potential retained off-diagonal positions per
+row. The production guards u>=1, ud<=p and d>4w+2 imply 2w<p. Summing proves
+the asserted infinity-norm bound. Principal restrictions can only reduce it.
+
+If a separately proved ideal comparison ||N_w-N||<=2^-46p is supplied, the
+triangle inequality yields the original weaker p*2^(16p+7)*eta+2^-46p budget.
+Neither that comparison nor a rowgap of N is established by this package.

research/gaussian-production-matrix-guard/README.md

@@ -0,0 +1,53 @@
+# Actual Gaussian production positivity and matrix perturbation
+
+The actual ProductionPlan guards, together with the cited scalar enclosure
+[PR6085](https://github.com/CrocSwap/integer-mult-bounds/pull/6085) at
+9fc80f1db55d4939c7b53c0799e6840cce35fbf8, imply every rounded similarity weight
+is >2^(-8p-1). [PROOF.md](PROOF.md) proves the unchanged Axis.matrix_entry
+consumer differs from its ideal truncated original-coordinate matrix by
+less than p*2^(16p+4)*2^-P in infinity norm, stronger than the requested
+p*2^(16p+7)*2^-P. It handles exact diagonals, holes, same-cell ratios,
+cross-cell coefficients and physical-period cuts explicitly.
+
+The scalar result is a cited mathematical dependency, not replayed or imported
+pending bytes. All live scientific inputs are from main721c03822. This does
+not discharge analytic_recovery or the selected frontier's five assumptions.
+
+## Reproduction and evidence
+
+Python3.12, standard library only, from repository root:
+
+```
+python3 scripts/research_package.py --package research/gaussian-production-matrix-guard
+```
+
+Direct export replay: `python3 -I -B research/gaussian-production-matrix-guard/verify.py`.
+The checker authenticates live source hashes before imports, executes the actual
+encoded ProductionPlan metadata example, and calls unchanged Axis.matrix_entry
+with supplied rational coefficient fields. These fields exercise the consumer;
+they are not a full Axis construction or production coefficient page. Exact
+rational identities on 150 retained pairs, 3,645 denominator-sensitive scalar
+perturbations and five failure controls corroborate the proof. The actual
+consumer fixture executes 64 entries; the metadata fixture has seven rejection
+controls. Normal and
+optimized registered commands use explicit checks surviving Python -O.
+
+## Open next questions
+
+Bind the ideal truncated matrix to the intended infinite/periodized ideal
+matrix with the claimed 2^-46p tail, then establish its uniform rowgap before
+asserting production Axis admission. Start with physical-period seams and the
+exact nearest convention in this proof. The retained ideal estimates and their
+actual source hypotheses remain blockers. LU/Schur, online accuracy, complete
+production pages and physical total cost remain separate obligations.
+
+## Credit and scope
+
+JoyboyBrian, with substantial OpenAI Codex assistance; Apache-2.0. Credit
+Jose Manuel/jmbarrancoml PR3851 for the physical producer and original
+precision/phase-cell argument; JoyboyBrian PR6085 for the scalar audit;
+James Reed's gaussian-gauge-column for the distinct conditional column
+argument; mihir-s-05 PR4449 for abstract across-cell rounding; RaD/hipotures,
+Chafik Boukhalfa and the preserved Gaussian/physical-word lineage. No frozen
+source is modified. Written proof and finite checks are by the same AI-assisted
+contributor, not independent human or formal-kernel acceptance. No new kappa.

research/gaussian-production-matrix-guard/SOURCES.json

@@ -0,0 +1,102 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_axis.py",
+      "usage": "input",
+      "git_blob": "edc443a7281e83536a00e9f9fa950d7d854705a3",
+      "sha256": "d416918d7442c5033e43fba94ccc5ed33badc3aebe90ddd479b0b6c020de9724"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_check_production.py",
+      "usage": "input",
+      "git_blob": "64c5e9f65c1dd621ee8bbacc9446b9f6dc741680",
+      "sha256": "08a0b2f4c3dc602ff3d8b98a37351a1910610c0bf1ea18fe7ff5378c373d1024"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_exponentials.py",
+      "usage": "input",
+      "git_blob": "8f0f32d7090554b47c112142e300c88fb8e5db4d",
+      "sha256": "f7a27cacbb27c0cfa4a63054e83feba2beae91b3fa9d3c37f903620b3899e67b"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_matrix.py",
+      "usage": "input",
+      "git_blob": "fc41183a42f5e1af5ea2294c295a0519abbcdb6c",
+      "sha256": "5bb982c6f36083b646bd5a5ab2ea4059c203fa0cc824e9f28132c0f323824bac"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_prepare.py",
+      "usage": "input",
+      "git_blob": "32e18686b653a09804941f5fd81b715973337aeb",
+      "sha256": "38aa123f80c68f7fcb9e60acae79543cf55f6fd37e12a548cffae11a9b50c1e5"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_rationals.py",
+      "usage": "input",
+      "git_blob": "053404d91c1bef0d4bb0f6647491847bf5879aaf",
+      "sha256": "6f9a380c8c7b4233c3bc338a6206d65cc85bee2e4f5625c2a212065f04f4b73d"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_sources.py",
+      "usage": "input",
+      "git_blob": "ce521f91997775e189f984ba7dd68a15bf9ecd9b",
+      "sha256": "c5889a97a11a9c6c6c44deb8a2042498ddc3f55703de15269132b8f198e24b15"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_window.py",
+      "usage": "input",
+      "git_blob": "335e0e2d2ee67302a67d1c5ba7c63baecc9b02d8",
+      "sha256": "d10eb4ac559a5dc3ef4a6178ab4cac7dfdcdb5e84ef8acf372bd22c81ab64996"
+    },
+    {
+      "path": "research/physical-gaussian-core/inputs/branchfree-source.tar",
+      "usage": "input",
+      "git_blob": "48dc77f5145d649bfed6745e38ab18b11772d597",
+      "sha256": "e6cdacd59a067189a99bfe03f4448913bb8d518ed4a9b1d981a68c5c666529c7"
+    },
+    {
+      "path": "research/physical-gaussian-core/inputs/word-export.tar",
+      "usage": "input",
+      "git_blob": "885794cf3328941209034ee2d946ed76dbea8ce3",
+      "sha256": "d428e8b6aef4d348fa2e922ca64c4cfd634bbb2f0c150033273e65fcf4600b49"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_boundary.py",
+      "usage": "input",
+      "git_blob": "840b90a239a3d76fd42dffc8cdbd7857f7173bad",
+      "sha256": "02303c11978baa4cbc707afb116b8cdb3314dbb2246fa4fe54dafc585d3e5122"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_convolution.py",
+      "usage": "input",
+      "git_blob": "611c6c6d4ab04e404e17dff6d2e0b65d5383546d",
+      "sha256": "57fc34acfef9921d805c8c3bdcd0227e67c2ba6b5114c1b373446680e29e3210"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_interior.py",
+      "usage": "input",
+      "git_blob": "8c7fed2531e69967958096cbb3602dbc9be79734",
+      "sha256": "38ffb65cbb40a60ac8d9b45665e752abc34dd2bf403dbc64c89f25a34b7fc2ae"
+    },
+    {
+      "path": "research/physical-gaussian-core/gaussian_rows.py",
+      "usage": "input",
+      "git_blob": "4b786bf2774fb317762b6148864f5192292da8e7",
+      "sha256": "821fd15a9b82f182f28055d4b83340e697906203f0728a36dc03196eca13c535"
+    }
+  ]
+}

research/gaussian-production-matrix-guard/TASK.json

@@ -0,0 +1,83 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?",
+    "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.",
+    "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.",
+    "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": [
+      "native_all_columns",
+      "owned_erasure",
+      "compiler",
+      "precision_tape",
+      "analytic_recovery"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "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": "refined",
+  "actual_scope": "Production Gaussian guards imply positive rounded weights and original-coordinate retained-band perturbation bound, conditional on PR6085 scalar theorem.",
+  "scope_change_reason": "One analytic_recovery implication at actual physical Gaussian consumer, following PR6085 handoff.",
+  "bottleneck_link": "Closes denominator positivity and retained matrix error composition; ideal tails and gap remain.",
+  "budget_minutes": 30,
+  "stop_rule": "Seven-minute feasibility gate; stop at scoped implication within twenty minutes, ten minutes validation.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and registered verify.py finite corroboration",
+  "author": "JoyboyBrian, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance",
+  "open_questions": [
+    {
+      "question": "Prove ideal truncated-to-infinite comparison and global ideal rowgap at physical-period seams.",
+      "why_it_matters": "Needed before uniform Axis.validate_rows and inverse admission.",
+      "first_step": "Bind nearest convention and cyclic displacement to retained ideal source theorem.",
+      "blocked_by": "Ideal tail/gap hypotheses are not audited here."
+    }
+  ]
+}