Sharpen degree-controlled cyclic inverse constants to pi (no new κ)

research/hardy-inverse-constant/PROOF.md

@@ -0,0 +1,149 @@
+# A sharper constant in the degree-controlled inverse envelope
+
+The claim is a scoped analytic proof. Let P be a nonzero complex polynomial
+of degree n and suppose |P(z)| >= delta > 0 on the unit circle. Let m be
+the number of roots strictly inside the circle, including multiplicity.
+With normalized circle measure and the two-sided Fourier coefficient norm W,
+
+\[
+ \|1/P\|_W\le\frac{(1+\pi m)(1+\pi n)}{\delta}
+ \le\frac{(1+22m/7)(1+22n/7)}{\delta}.                 \tag{1}
+\]
+
+The second inequality is strict when n>0. For n=0 both expressions equal
+1/delta. If U is an invertible bounded operator on a complex Banach space
+with ||U^k|| <= 1 for every integer k, the same right side bounds
+||P(U)^(-1)||. Thus the statement covers unit-phase cyclic shifts at
+every length and integer stride, including zero and noncoprime strides.
+
+Rafael Guevara's PR803 proves the same assertions with 4 in place of pi.
+Its proof at `a0f15ce84f0951f69b39795f229cb854307ca52b`, retained unchanged
+on the package base, supplies the Hardy factorization, normalized rational
+arc-length inequality, root reflection and operator substitution used below.
+Those are cited premises. This contribution sharpens the coefficient
+estimate in that chain; it does not audit the predecessor or claim a new
+Hardy inequality.
+
+## 1. Evaluate the Schur integral instead of splitting it
+
+For j,k >= 0 put K_jk=1/(j+k+1), w_j=(j+1/2)^(-1/2), and a=j+1/2.
+The positive function f_a(x)=1/((a+x)sqrt(x)) is convex on x>0, since
+
+\[
+ f_a''(x)=\frac{3}{4x^{5/2}(a+x)}
+       +\frac{1}{x^{3/2}(a+x)^2}
+       +\frac{2}{x^{1/2}(a+x)^3}>0.
+\]
+
+The midpoint bound, including the integrable interval starting at zero,
+gives the same Schur row estimate as PR803 Section 1. Evaluate its integral
+using x=a t^2:
+
+\[
+ \sum_{k\ge0}K_{jk}w_k
+ \le\int_0^\infty\frac{dx}{(a+x)\sqrt{x}}
+ =\frac{2}{\sqrt a}\int_0^\infty\frac{dt}{1+t^2}
+ =\pi w_j.                                           \tag{2}
+\]
+
+PR803 instead bounds the two parts at x=a separately, obtaining 4w_j.
+The weighted Cauchy-Schwarz argument applied to finite nonnegative
+sequences s,t therefore gives
+
+\[
+ \sum_{j,k}K_{jk}s_jt_k\le\pi\|s\|_2\|t\|_2.         \tag{3}
+\]
+
+For h analytic in a neighborhood of the closed disk, use the classical
+Hardy factorization h=ab with ||a||_2 ||b||_2=||h||_1, as in PR803
+Section 1. Coefficient convolution, (3), and increasing finite truncations
+give
+
+\[
+ \sum_{l\ge0}\frac{|h_l|}{l+1}\le\pi\|h\|_1.        \tag{4}
+\]
+
+The predecessor's radial limit handles boundary zeros of h. The constant
+change does not alter that limit or any analyticity hypothesis.
+
+## 2. Carry the constant through the inherited analytic chain
+
+For a rational R of degree at most d analytic near the closed disk, apply
+(4) to h=R'. The normalized Dolzhenko-Spijker inequality, used in PR803
+Sections 2 and 3, is ||R'||_1 <= d||R||_infinity. Consequently
+
+\[
+ \|R\|_W
+ \le |R(0)|+\pi\|R'\|_1
+ \le(1+\pi d)\|R\|_\infty.                          \tag{5}
+\]
+
+Use the exact factorization P=JQ from PR803 Section 4. Here J is the
+finite Blaschke product of the m interior roots, has rational degree m
+and unit circle magnitude one. The polynomial Q has degree at most n
+and no roots in the closed disk, with |Q|=|P| on the circle. Hence J
+and 1/Q are analytic near the closed disk. Applying (5) gives
+
+\[
+ \|J\|_W\le1+\pi m,\qquad
+ \|1/Q\|_W\le(1+\pi n)/\delta.
+\]
+
+On the circle, 1/P=conjugate(J)/Q. Absolute coefficient convolution gives
+the first bound in (1). PR803 Section 5's absolutely convergent
+two-sided operator substitution then gives the asserted operator bound.
+This uses the full integer-power hypothesis; spectral location alone is
+not a replacement. No roots need to be computed to apply the bound with m=n.
+
+## 3. A rational upper certificate and strict improvement
+
+The elementary polynomial identity
+
+\[
+ x^4(1-x)^4=(1+x^2)(x^6-4x^5+5x^4-4x^2+4)-4
+\]
+
+integrates on [0,1] to
+
+\[
+ 0<\int_0^1\frac{x^4(1-x)^4}{1+x^2}\,dx
+   =\frac{22}{7}-\pi.                               \tag{6}
+\]
+
+The numerator is positive on (0,1), and the quotient polynomial has
+integral 22/7. This proves the rational version of (1) without a decimal
+approximation to pi. The integral certificate is classical; no historical
+priority is asserted for it or for the Hardy constant pi.
+
+The exact difference between the old and new rational multipliers is
+
+\[
+ (1+4m)(1+4n)-(1+22m/7)(1+22n/7)
+  =\frac67(m+n)+\frac{300}{49}mn.                   \tag{7}
+\]
+
+It is positive for every n>0 and 0<=m<=n. At m=n the leading quadratic
+coefficient decreases from 16 to 484/49, a ratio of 121/196. This is a
+comparison of sufficient upper bounds. It is not a ratio of actual norms
+or a lower bound on the improvement to a working implementation.
+
+## 4. Scope of the exact checks
+
+The verifier checks (6)'s polynomial identity and rational integral, (7)
+on its declared finite calibration domain, exact binary ceiling brackets,
+and new sufficient norm budgets for fourteen named prime-power radices.
+The budget input from PR803 Section 5 is the cited circle certificate
+delta^(-1)=2rn(2^r-1)^(n phi(r)-1), with n=r-1. We substitute the new
+multiplier, not replay the source's circle theorem or numerical results.
+Later #1025 improves that gap certificate in another regime; the theorem
+here accepts any independently supplied positive delta, including that one.
+
+Finite checks do not prove the infinite Schur bound, classical arc-length
+premise, or analytic limits. Those are the written argument and explicit
+dependencies above. No optimal degree dependence, paid inverse routine,
+rounded precision recurrence, complete supplier or multiplication theorem
+is established. Independent human and formal proof-kernel review are unclaimed.
+
+This refinement was produced by Nick Petalas. Credit Rafael Guevara/PR803,
+Ali Romman/PR621, and the classical Hardy, Hilbert, Blaschke,
+Dolzhenko-Spijker and Baranov-Zarouf lineage retained in PR803. Apache-2.0.

research/hardy-inverse-constant/README.md

@@ -0,0 +1,98 @@
+# A sharper degree-controlled cyclic inverse constant
+
+For a degree-n polynomial P with |P| >= delta > 0 on the unit circle,
+and m interior roots counted with multiplicity, this scoped analytic proof gives
+
+\[
+ \|1/P\|_W\le(1+\pi m)(1+\pi n)/\delta
+ \le(1+22m/7)(1+22n/7)/\delta.
+\]
+
+The same envelope bounds ||P(U)^(-1)|| whenever U is an invertible bounded
+operator with ||U^k|| <= 1 for every integer k. In particular it applies
+to unit-phase cyclic shifts at every length and stride.
+
+Rafael Guevara's [PR803](https://github.com/CrocSwap/integer-mult-bounds/pull/803)
+uses 4 instead of pi. The new step evaluates its positive Schur kernel
+integral exactly, then carries the smaller constant through its cited
+Hardy, rational arc-length and root-reflection chain. The rational envelope
+is strictly smaller at every positive degree. The leading quadratic
+coefficient at m=n changes from 16 to 484/49.
+
+The sufficient binary norm-bound ceilings decrease from 19 to 18 at radix 3,
+441 to 440 at radix 9, 11,999 to 11,998 at radix 25, and 347,859 to 347,858
+at radix 71, using the same explicit PR621 circle certificate. These are
+ceilings of upper bounds, not measured norms or working-precision savings.
+Later PR1025's improved circle gap is a separate input and is compatible
+with the general delta-parametric statement.
+
+[PROOF.md](PROOF.md) contains the written all-degree argument and identifies
+the inherited analytic premises. The classical constant pi and the positive
+integral proving pi<22/7 are not new mathematics. This contribution is the
+strict refinement of the repository's explicit inverse envelope. No optimal
+degree dependence, paid inverse algorithm, rounded implementation, complete
+supplier or new kappa is claimed.
+
+## Reproduce
+
+Use CPython 3.12 and the standard library, from the worktree root:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/hardy-inverse-constant
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/hardy-inverse-constant/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/hardy-inverse-constant --check-source-history
+```
+
+Other machines can substitute their CPython 3.12 executable. The registered
+commands run both normal and optimized Python. They print
+`PASS_HARDY_INVERSE_CONSTANT` in a generated JSON receipt containing exact
+results and SHA256 bindings to every package file and the consumed proof.
+An optional `--emit /absolute/external/new-receipt.json` creates that receipt
+outside the checkout and refuses overwrites. No receipt is hand-written.
+
+The checks cover the polynomial division and rational integral for pi<22/7,
+8,385 degree pairs with 0<=m<=n<=128, 4,096 exact logarithm brackets,
+fourteen named prime-power norm budgets, and seven rejection controls.
+Finite checks corroborate the new rational arithmetic; they do not prove
+the analytic limits or independently validate PR803. No predecessor verifier
+is run. Source bindings are in [SOURCES.json](SOURCES.json); the catalogue
+and selected record are historical provenance. The originating scope change
+and next questions are explicit in [TASK.json](TASK.json).
+
+## Verification limits
+
+The analytic proof is conditional on the explicitly cited classical and
+PR803 implications. Independent human and formal proof-kernel review are
+unclaimed. Rounded scan errors, preparation, routing, restoration and full
+supplier admission are unrun obligations. No selected frontier changes.
+
+The verifier has no recursion, subprocesses or network access. Its numerical
+loops have fixed finite domains; the largest budget uses fewer than 350,000
+bits. Functions are shorter than 60 lines, and required invariants use
+explicit exceptions under optimized Python. Python's managed allocation is
+a documented deviation from fixed allocation: only fourteen bounded budget
+rows are retained, each source file is capped at two MiB, and no steady
+service loop or mutable shared state exists. The written theorem has no
+finite-degree or radix ceiling; those limits apply only to calibration.
+
+## Open next questions
+
+- Integrate the smaller envelope into one actual PR628 or PR764 rounded
+  precision recurrence. Start with its explicitly consumed inverse norm,
+  retaining preparation, every error source and dirty restoration. No such
+  implementation or resource improvement is supplied here.
+- Improve the quadratic degree dependence. Start with a direct two-sided
+  Wiener estimate that avoids separately multiplying the reflected factors.
+  Neither this proof nor PR803 establishes an optimal degree multiplier.
+
+## Credit
+
+This refinement was produced by Nick Petalas. Credit Rafael Guevara/PR803
+for the degree-controlled inverse argument; Ali Romman/PR621 for the
+prime-power setting and circle certificate; Hardy, Hilbert, Blaschke,
+Dolzhenko and Spijker for the classical analytic ingredients; and
+Baranov-Zarouf for the normalized arc-length source retained by PR803.
+Thiago Costa/PR832 supplies a distinct Sobolev estimate, William Lawyer/PR852
+treats weighted power caps, and Philipp/PR1025 improves the circle gap.
+Their results are cited, not rechecked or incorporated as new work here.
+Apache-2.0.

research/hardy-inverse-constant/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4",
+  "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/PROOF.md",
+      "usage": "input",
+      "git_blob": "15d344789d1ae475790f5d6a45cd37ae27f05d1c",
+      "sha256": "6c28d93d9d1d37da0bbc3876070ef8c6f0f5dad8e186b31b31330028e5420c0e"
+    }
+  ]
+}

research/hardy-inverse-constant/TASK.json

@@ -0,0 +1,92 @@
+{
+  "schema_version": 1,
+  "task_id": "uniform-transfer-audit",
+  "priority_revision": 7,
+  "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4",
+  "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": "Sharpen PR803's degree-controlled Wiener and cyclic inverse upper envelope by replacing its Hardy coefficient constant 4 with pi, with a fully rational 22/7 upper certificate.",
+  "scope_change_reason": "The original card asks to audit one all-size construction implication. This is an original analytic constant improvement to a separately scoped inverse estimate; no predecessor audit or full caller admission is attempted.",
+  "bottleneck_link": "A smaller analytic inverse envelope can reduce a sufficient normalization or precision budget for cyclic components. Incorporation into a rounded paid caller remains an open obligation; this is an analytic side result.",
+  "budget_minutes": 60,
+  "stop_rule": "Package the first proved strict constant improvement; do not optimize the degree factor or begin a rounded implementation.",
+  "outcome": "completed",
+  "evidence": "PROOF.md derives the pi Schur constant and its operator corollary. verify.py checks the polynomial integral certificate, 8385 degree pairs, 4096 exact binary ceiling brackets, fourteen radix budgets and seven rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does this smaller inverse envelope lower a concrete rounded cyclic caller's sufficient precision?",
+      "why_it_matters": "An analytic norm improvement changes execution resources only after every error source, preparation and restoration charge is included.",
+      "first_step": "Select one PR628 or PR764 rounded scan with an explicit consumed inverse norm, and substitute this envelope into that one recurrence.",
+      "blocked_by": "No rounded scan, factor preparation or dirty restoration implementation is supplied here."
+    },
+    {
+      "question": "Can the quadratic degree multiplier be replaced by a smaller asymptotic degree dependence?",
+      "why_it_matters": "The present improvement only changes constants; the separate Blaschke and reflected reciprocal factors are still multiplied.",
+      "first_step": "Study a direct two-sided Wiener estimate for one rational function, retaining a uniform circle-gap premise.",
+      "blocked_by": "The inherited argument separately bounds the two analytic factors and gives no optimality theorem."
+    }
+  ],
+  "claim_type": "scoped proof",
+  "predecessors": [
+    {
+      "pr": 803,
+      "author": "Rafael Guevara",
+      "proof_commit": "a0f15ce84f0951f69b39795f229cb854307ca52b"
+    },
+    {
+      "pr": 621,
+      "author": "Ali Romman"
+    }
+  ]
+}