Prove the sharp mixed-quadratic inverse factor two (no new κ)

research/mixed-quadratic-circle-bound/PROOF.md

@@ -0,0 +1,119 @@
+# Sharp inverse bounds for a mixed quadratic
+
+This scoped proof is produced by Nick Petalas. The cyclic operator setting and
+the general degree multiplier are credited to Ali Romman #621 and Rafael
+Guevara #803. Geometric series, partial fractions and the triangle inequality
+are classical. No literature-priority claim is made for those methods.
+
+Let
+
+    P(z) = c (z-a)(1-bz),   c != 0,   |a|=A<1,   0<|b|=B<1.
+
+Thus P has exactly one root in the open unit disk and one outside its closure.
+Put m=min(A,B) and delta=min_{|z|=1}|P(z)|>0. For an absolutely convergent
+Laurent series, its Wiener norm is the sum of the absolute values of its
+coefficients. Then
+
+    delta ||1/P||_W <= (1+m)^2/(1+m^2) < 2.                 (1)
+
+For every fixed 0<=m<1 the displayed factor is best possible among this
+class with min(A,B)=m. Consequently the best factor independent of the roots
+is two. In particular, the general degree-two multiplier 81 obtained by
+substituting n=2 in #803 can be replaced by two on this subclass. This is a
+strengthening of a bound, not a defect in that predecessor.
+
+## Exact Laurent norm
+
+It suffices to take c=1, since delta scales by |c| and the inverse norm by
+its reciprocal. On the unit circle the two absolutely convergent geometric
+series give
+
+    1/((z-a)(1-bz))
+      = 1/(1-ab) [ sum_{j>=0} b^(j+1) z^j
+                    + sum_{h>=1} a^(h-1) z^(-h) ].        (2)
+
+One can obtain (2) by multiplying the geometric series for each factor,
+or by partial fractions. The positive and negative exponent sets are disjoint.
+Since A,B<1, their absolute sums are geometric, so
+
+    ||1/P||_W = (1-AB)/((1-A)(1-B)|1-ab|).                (3)
+
+No cancellation or asymptotic estimate enters (3).
+
+## The sharp upper bound
+
+For 0<=x<=y<1 and every real theta,
+
+    |1-y exp(i theta)| / |1-x exp(i theta)|
+       <= (1+y)/(1+x).                                  (4)
+
+To prove this, square the ratio and put t=cos(theta). Its derivative in t
+has the sign of (x-y)(1-xy), which is nonpositive. The maximum is at t=-1.
+This also proves (4) at x=0 and at x=y without division by a vanishing quantity.
+
+Suppose first A>=B. Here A>0. Evaluate P at z=a/A and apply (4) with
+x=AB, y=B and exp(i theta)=ab/(AB). Equations (3) and (4) give
+
+    delta ||1/P||_W
+       <= (1-AB)(1+B)/((1-B)(1+AB))
+       <= (1-B^2)(1+B)/((1-B)(1+B^2))
+        = (1+B)^2/(1+B^2).                               (5)
+
+The second inequality follows because (1-x)/(1+x) decreases for x>=0
+and AB>=B^2. If B>A, evaluate instead at z=conjugate(b)/B. The identical
+argument with A,B interchanged gives (1). This also covers A=0 directly:
+(3) and delta=1-B give product one. Finally
+(1+m)^2<2(1+m^2) is equivalent to (1-m)^2>0.
+
+## Attainment and the uniform factor
+
+For any 0<r<1 take a=r and b=-r. For |z|=1,
+
+    |(z-r)(1+rz)|^2
+       = (1+r^2)^2 - 4r^2 (Re z)^2
+       >= (1-r^2)^2.
+
+Equality holds at z=1 and z=-1, so delta=1-r^2. Equation (3) yields
+
+    delta ||1/P||_W = (1+r)^2/(1+r^2).                   (6)
+
+This proves sharpness for every fixed m=r>0 and tends to two as r tends
+to one from below. At m=0, use a=0 and any 0<B<1 to attain one. Thus two
+is the least uniform constant, although no member of the class attains two.
+
+## Cyclic operators and sharpness there
+
+Let Z_L be a cyclic permutation matrix of any positive length L, let w be
+any integer and let |tau|=1. Put U=tau Z_L^w. Every integer power of U has
+induced infinity norm one. Substituting U in the absolutely convergent
+series (2) therefore gives an inverse of P(U), with
+
+    ||P(U)^(-1)||_infinity <= ||1/P||_W
+       <= (1+m)^2/((1+m^2) delta) < 2/delta.             (7)
+
+Multiplication by the finite polynomial P preserves absolute convergence,
+and the Laurent coefficient identity proves both inverse identities. There
+is no assumption that w is positive or coprime to L.
+
+The factor in (7) is also sharp uniformly in cyclic length. Fix the Laurent
+coefficient sequence (d_k) of 1/P, and take U=Z_L. The inverse has coefficients
+q_j=sum_{k congruent j mod L} d_k. Its infinity norm is sum_j |q_j|, since
+the first row has one entry at each residue and other rows are permutations.
+For K>=0 and L>2K, the coefficients with |k|<=K have distinct residues.
+Writing T_K=sum_{|k|>K}|d_k|, the triangle inequality in both directions gives
+
+    ||1/P||_W - 2T_K <= sum_j |q_j| <= ||1/P||_W.
+
+Since T_K tends to zero, these finite cyclic norms tend to the Wiener norm.
+Apply this to the rational family in (6), first taking L large at fixed r,
+then taking r towards one. No smaller uniform cyclic constant can work.
+
+## Boundaries
+
+The proof uses the exactly quadratic mixed-root factorization. It does not
+improve #803's general arbitrary-degree theorem. It supplies no coefficient
+preparation, rounded algorithm, source restoration, paid tape schedule,
+physical supplier, new kappa or complete multiplication theorem. The finite
+checks corroborate formulas and finite cyclic inverses; the universal result
+rests on this written proof. Independent human and formal proof-kernel review
+are unclaimed.

research/mixed-quadratic-circle-bound/README.md

@@ -0,0 +1,104 @@
+# Sharp factor two for mixed quadratic cyclic inverses
+
+This scoped proof is produced by Nick Petalas. For
+
+    P(z)=c(z-a)(1-bz),  c!=0,  |a|<1,  0<|b|<1,
+    delta=min_{|z|=1}|P(z)|,  m=min(|a|,|b|),
+
+the [written proof](PROOF.md) establishes
+
+    delta ||1/P||_W <= (1+m)^2/(1+m^2) < 2.
+
+The Wiener norm sums the absolute values of the Laurent coefficients. The
+radius-sensitive factor is optimal at each fixed m, and two is the least
+uniform factor. Both statements also hold for the induced infinity norm of
+`P(tau Z_L^w)^(-1)`, uniformly over positive cyclic lengths, integer strides
+and unit phases. Sharpness there is a limit over cyclic lengths.
+
+Rafael Guevara's [#803](https://github.com/CrocSwap/integer-mult-bounds/pull/803)
+proves the general degree bound `(1+4n)^2/delta` and leaves its degree factor
+nonoptimal. On this mixed-root degree-two subclass, the sufficient multiplier
+therefore falls from 81 to two. The new step is the exact two-sided Laurent
+norm and a sharp endpoint bound. The antipodal family `a=r,b=-r` attains
+`(1+r)^2/(1+r^2)` and approaches two. No predecessor result is replayed or audited.
+
+## Evidence and reproduction
+
+Standard-library CPython 3.12 is sufficient. From the repository root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/mixed-quadratic-circle-bound
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/mixed-quadratic-circle-bound/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/mixed-quadratic-circle-bound/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/mixed-quadratic-circle-bound --check-source-history
+```
+
+A reviewer can substitute their CPython 3.12 executable. Direct verification
+also works from a Git-free export. Ordinary verification writes no files.
+`--emit-to NEW_EXTERNAL_FILE` exclusively creates a generated receipt with all
+six package source hashes; `--check-receipt FILE` recomputes every result and
+compares it with the receipt, including integer/Boolean types. No receipt is
+hand-written or required as an external replay input.
+
+The executed finite coverage is:
+
+- 192 exact endpoint inequalities across four interior radii, three reciprocal
+  exterior radii and every pair of phases in `{1,-1,i,-i}`.
+- 768 cyclic inverse comparisons between dense elimination and a finite
+  geometric resolvent construction, with 2,688 inverse entries. Eight root
+  pairs, lengths 1 through 6, strides `-1,0,1,2` and all four unit phases are
+  crossed. Both inverse identities and rational upper enclosures of the norms
+  are checked. The 192 antipodal cases also use their exact circle gap.
+- 63 rational sharpness identities at `r=(d-1)/d`, `d=2,...,64`. The final
+  normalized Wiener norm is `16129/8065`, with exact deficit `1/8065` from two.
+- Eight controls cover three invalid root domains, wrong factor sign, wrong
+  inverse direction, wrong gauge, omitted negative Fourier frequencies, and a
+  finite cyclic counterexample to replacing the factor by one.
+
+The enumerations corroborate the universal proof. They do not exhaust complex
+roots or establish the universal theorem by sampling. Receipt mutation,
+exclusive-create and source-hash controls are separate publication checks.
+
+## Scope and implementation limits
+
+This is a scoped proof with finite corroboration, not a finite supplier
+certificate or complete multiplication theorem. No new kappa is claimed.
+The theorem concerns exact operators with one interior and one exterior root.
+It gives no coefficient preparation, rounded execution, dirty restoration,
+fixed-tape schedule, complete caller invoice or supplier admission. The selected
+frontier remains unchanged. Independent human and formal proof-kernel review
+are unclaimed. No Lean, Docker or selected cold replay is required or run.
+
+The verifier has no recursive calls. Its finite mathematical loops are bounded
+by the displayed corpus, matrix size six and exponent 64; functions remain
+below 60 lines. Explicit exceptions retain the checks under optimization.
+Python's managed allocation is a deviation from fixed storage: all matrix
+storage is bounded by six rows of seven Gaussian rationals, and external
+receipt size is bounded by one MiB. Library arithmetic and JSON parsing use
+runtime allocation. A lower-level implementation would require its own storage
+proof. Warning-strict normal and optimized execution provide available
+diagnostics; no separate linter or type checker is installed in this environment.
+
+Source pins in [SOURCES.json](SOURCES.json) are historical provenance at canonical
+main `624de9dc66858af0945e5f8a0942488d62280d43`. There are no imported predecessor
+executables or live mathematical dependencies. [TASK.json](TASK.json) records
+the changed card scope and structured next questions.
+
+## Open next questions
+
+1. Determine the best multiplier when both quadratic roots are outside the
+   unit circle. Start with separated two-pole phases and exact coefficient
+   sums. Coefficient cancellation blocks the disjoint-series argument here.
+2. Apply the bound to one actual source-bound mixed quadratic caller's complete
+   rounding recurrence. First identify the factor, then charge preparation,
+   every prefix and restoration. A complete physical invoice remains missing.
+
+## Credit
+
+Credit Rafael Guevara #803 for the general degree-controlled bound and its
+nonoptimality question, Ali Romman #621 for the cyclic kernel setting, and
+Thiago Costa #802 for the related Fourier-transfer work. Geometric-series
+resolvents and Fourier substitution are classical; Ryan Pinto #692 retains
+credit for the retained finite-geometric cyclic implementation lineage. No
+literature-priority claim is made for those methods. This result is produced
+by Nick Petalas. New files are under Apache-2.0.

research/mixed-quadratic-circle-bound/SOURCES.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/rational-circle-bound/README.md",
+      "usage": "provenance",
+      "git_blob": "1a1d3068a85a41ceabdf512e30aa15c448ccd321",
+      "sha256": "77dcfe10cf69b66e092c4bf9501353cd82e61d899fca0b983f60dec25e012c4f"
+    },
+    {
+      "path": "research/rational-circle-bound/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "15d344789d1ae475790f5d6a45cd37ae27f05d1c",
+      "sha256": "6c28d93d9d1d37da0bbc3876070ef8c6f0f5dad8e186b31b31330028e5420c0e"
+    },
+    {
+      "path": "research/prime-power-cyclic-inverse/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "0c757c37c70fdeb261d73f111ceedd3b233287bf",
+      "sha256": "2b8056c88e66f692f407450fff0414d41bcd09db8597be22e274a6c3dc20eb9e"
+    }
+  ],
+  "note": "Historical mathematical context only. No predecessor executable is imported or replayed."
+}

research/mixed-quadratic-circle-bound/TASK.json

@@ -0,0 +1,85 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "uniform-transfer-audit",
+    "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Prove one missing implication with explicit quantified hypotheses.",
+      "Find an exact counterexample at the claimed interface boundary."
+    ],
+    "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_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.",
+    "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.",
+    "allowed_variations": [
+      "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller."
+    ],
+    "scope_change_triggers": [
+      "Replacing a quantified obligation with another finite smoke test.",
+      "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses."
+    ],
+    "overlap_terms": [
+      "uniform transfer",
+      "all-size",
+      "precision",
+      "4100",
+      "unconditional-batched-crt"
+    ],
+    "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_status": "changed",
+  "actual_scope": "Sharp Wiener and cyclic inverse-circle-gap factor two for quadratics with one interior and one exterior root, and sharp radius-sensitive factor (1+m)^2/(1+m^2).",
+  "scope_change_reason": "The assignment requires original work rather than rechecking predecessors. This card is redirected to the nonoptimal conditioning multiplier in #803, a scoped cyclic-interface side result.",
+  "bottleneck_link": "Scoped conditioning side result for the cyclic inverse interface. It reduces a sufficient norm multiplier for mixed quadratic factors, without a paid implementation or new kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after the first proved sharp mixed-quadratic strengthening and exact bounded corroboration; do not extend to other degrees.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and warning-strict normal/optimized verify.py. Finite cases corroborate the proof, rather than prove universal quantifiers.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the optimal inverse-circle-gap multiplier for quadratics whose two roots are both outside the unit circle?",
+      "why_it_matters": "This would address another subclass of the nonoptimal general degree bound.",
+      "first_step": "Derive the exact coefficient absolute sum for a two-pole rational family with separated phases.",
+      "blocked_by": "Coefficient cancellation prevents the disjoint two-sided geometric-series argument used here."
+    },
+    {
+      "question": "Can one actual cyclic-factor caller use the sharper bound in its complete rounding recurrence?",
+      "why_it_matters": "A norm improvement only reduces physical precision if it reaches a paid implementation.",
+      "first_step": "Identify a source-bound mixed quadratic and reprice coefficient preparation, every rounded prefix and restoration.",
+      "blocked_by": "No such caller or complete resource invoice is supplied here."
+    }
+  ],
+  "environment": {
+    "python": "3.12.15",
+    "implementation": "CPython",
+    "dependencies": "standard library only"
+  }
+}

research/mixed-quadratic-circle-bound/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": "192 exact endpoint inequalities, 768 dense/geometric cyclic inverse comparisons, 63 sharpness identities and eight semantic controls; source-bound receipt emission is optional and external."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "192 exact endpoint inequalities, 768 dense/geometric cyclic inverse comparisons, 63 sharpness identities and eight semantic controls; source-bound receipt emission is optional and external."
+    }
+  ]
+}