C6 method boundary: sharp abstract count-cap loss and the missing size-biased moment

.github/workflows/c6-count-cap-boundary.yml

@@ -0,0 +1,33 @@
+name: C6 count-cap method-boundary controls
+
+'on':
+  pull_request:
+    paths:
+      - 'frontiers/c6_count_cap_boundary_20260929/**'
+      - '.github/workflows/c6-count-cap-boundary.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'frontiers/c6_count_cap_boundary_20260929/**'
+      - '.github/workflows/c6-count-cap-boundary.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  exact-boundary:
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262
+        with:
+          persist-credentials: false
+      - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065
+        with:
+          python-version: '3.11.16'
+      - name: Exact sources and both-mode semantic controls
+        run: |
+          set -euo pipefail
+          python -B -S frontiers/c6_count_cap_boundary_20260929/verify.py --output "${RUNNER_TEMP}/count-cap-boundary-${GITHUB_RUN_ID}-${GITHUB_RUN_ATTEMPT}"
+          git diff --exit-code

frontiers/c6_count_cap_boundary_20260929/PROOF.md

@@ -0,0 +1,223 @@
+# What a rare first moment and a global count cap can—and cannot—prove
+
+Object: OA-C6-COUNT-CAP-BOUNDARY-20260929-v1.
+Author: OpenAI / ChatGPT, 29 September 2026.
+Disposition: AUTHOR-SIDE MATHEMATICAL CANDIDATE; nonauthor review required.
+Scientific effect NONE. No existing source, review, status, graph, lemma flag or
+prize is modified. No novelty or Gaussian optimality claim is made.
+
+## 1. Purpose and independence from the Gaussian candidates
+
+The new C6 route bounds a rare window count N by a total critical-point cap Psi.
+Claude's Math-#142 separately develops a Gaussian cap tail using a growing
+complex Cauchy radius. This note does NOT duplicate that theorem. It proves an
+abstract inference bound, an explicit example saturating it, and an exact
+size-bias identity isolating the extra information needed for a log-free result.
+
+No Gaussian covariance, Rouché theorem, invariant manifold or unreviewed
+higher-dimensional first-moment statement is an input to the proofs below.
+The existing project arguments motivate the hypotheses but are not proved or
+accepted by this note. In particular, the example is NOT a Gaussian random
+field and says nothing about the actual optimal order of C6.
+
+Fix an integer d>=2. For each sufficiently small r>0, let Q_r be a probability
+law, P_r a law with density R_r=dP_r/dQ_r, N_r a nonnegative integer-valued
+random variable, and Psi_r a nonnegative measurable cap with N_r<=Psi_r.
+Assume constants independent of r satisfy
+
+    E_{P_r} N_r <= C_0 r^3,             ||R_r||_{L2(Q_r)} <= K,
+    Q_r(Psi_r>x) <= C_1 exp(-c phi_d(x)),
+    phi_d(x)=x^(1/d) log(2+x),            x>=0.                 (B1)
+
+The laws and variables may otherwise depend on r. Constants may depend on d.
+No independence between the cap, count and density is assumed. The cap-tail
+hypothesis implies Psi_r<infinity almost surely under both laws. For integer
+q>=1, (N)_q=N(N-1)...(N-q+1), with value zero when N<q.
+
+**Theorem A (inference bound).** For every fixed integer q>=2, writing
+L=log(1/r), (B1) implies
+
+    E_{P_r}(N_r)_q <= C_q r^3 [L/log L]^{d(q-1)}               (B2)
+
+for all sufficiently small r. It also implies a uniformly bounded small positive
+exponential moment of phi_d(Psi_r), under Q_r and P_r.
+
+**Theorem B (limit of these hypotheses).** There is an explicit family satisfying
+(B1), even with P_r=Q_r and E N_r=r^3 on a sequence r_n decreasing to zero, such
+that for every fixed q>=2
+
+    E (N_{r_n})_q ~ r_n^3 [L_n/log L_n]^{d(q-1)}.              (B3)
+
+Thus (B1) alone cannot imply an o of the right-hand side in (B2), or an O(r^3)
+second factorial moment. This is an optimality statement for this ABSTRACT
+class of inference, not for Gaussian critical points.
+
+**Proposition C (the missing correlation).** Let m_r=E_{P_r}N_r>0 and define the
+count-size-biased configuration law
+
+    dP_r^sb = (N_r/m_r) dP_r.
+
+Then the exact identity
+
+    E_{P_r}(N_r)_q
+      = m_r E_{P_r^sb}[(N_r-1)_{q-1}]
+      <= m_r E_{P_r^sb}[Psi_r^{q-1}]                          (B4)
+
+holds as an identity/inequality of nonnegative extended expectations. Therefore
+uniform size-biased cap moments, not merely unconditional cap moments, suffice
+for a log-free O(r^3) result. Count-size bias is NOT conditioning on N_r>=1.
+
+## 2. Proof of the upper inference bound
+
+The tail in (B1) gives every fixed polynomial cap moment uniformly:
+
+    E_{Q_r}Psi_r^p
+       = p integral_0^infinity t^(p-1) Q_r(Psi_r>t)dt <= C_p.
+
+This formula follows first for truncations and then by monotone convergence.
+Since phi_d grows faster than log t, the integral is finite. In particular all
+moments used below exist, independently of r.
+
+For any cutoff lambda>0 and integer q>=2, pathwise
+
+    (N)_q <= N Psi^{q-1}
+           <= lambda^{q-1}N + Psi^q 1{Psi>lambda}.             (B5)
+
+Take expectations under P_r. Cauchy–Schwarz with the actual density R_r, followed
+by another Cauchy–Schwarz under Q_r, gives
+
+    E_{P_r}[Psi^q 1_A]
+      <= ||R_r||_2 (E_{Q_r}[Psi^{2q}1_A])^(1/2)
+      <= K (E_{Q_r}Psi^{4q})^(1/4) Q_r(A)^(1/4)
+      <= C_q exp(-c phi_d(lambda)/4),       A={Psi>lambda}.   (B6)
+
+Both square roots matter. Neither (B5) nor (B6) factors an expectation of N and
+Psi or assumes independence of R_r from the cap. In the application R_r=W_r/Z_r;
+a uniform W_r/r^2 moment and a positive Z_r/r^2 floor are what bound its norm.
+Those Gaussian facts are external premises, not consequences of this note.
+
+Take lambda=(A L/log L)^d, A>=1, with L sufficiently large. For example,
+log L>=2 implies 2loglog L<=log L; hence
+
+    log lambda = d(log A+log L-loglog L) >= log L,
+    phi_d(lambda) >= lambda^(1/d) log lambda >= A L.           (B7)
+
+Choose A so cA/4>=4. The tail term in (B6) is at most C_q r^4. The first term in
+(B5) is at most C_0 r^3 lambda^{q-1}. Since lambda>=1 for small r, the r^4 term is
+absorbed, proving (B2). Each q is fixed; no uniform-in-q constant is asserted.
+
+For the exponential-moment assertion, use that phi_d is continuous, strictly
+increasing on [0,infinity), and unbounded. From (B1),
+Q_r(phi_d(Psi_r)>t)<=C_1 e^{-ct}. Layer-cake integration gives
+
+    E_{Q_r} exp(a phi_d(Psi_r))
+      =1+ a integral_0^infinity e^{at}Q_r(phi_d(Psi_r)>t)dt
+      <=1+C_1 a/(c-a),                       0<a<c.
+
+Under P_r, Cauchy–Schwarz bounds the moment at a by K times the square root of
+the Q_r moment at 2a. Thus any 0<a<c/2 works uniformly for both laws. This extra
+unconditional integrability STILL does not eliminate the loss, as the example
+shows.
+
+## 3. Explicit family attaining the inference bound
+
+For integers n>=3 define
+
+    r_n=n^{-n},        K_n=n^d,        p_n=r_n^3/K_n.
+
+Under P_n=Q_n, set N_n=K_n with probability p_n and N_n=0 otherwise. Put
+Psi_n=N_n+2. This +2 models the harmless presence of two excluded prescribed
+objects in a total cap; no pinning or Gaussian law is asserted. The density
+R_n is identically one, so its L2 norm is one. Direct computation gives
+
+    E N_n = p_n K_n = r_n^3,
+    E(N_n)_2 = r_n^3(K_n-1),
+    E(N_n)_q = r_n^3 product_{j=1}^{q-1}(K_n-j).               (B8)
+
+For fixed q and n large, the last expression is asymptotic to
+r_n^3 n^{d(q-1)}. These identities use falling factorials, not ordinary powers.
+
+### A uniform cap-tail bound, not merely bounded moments
+
+For x<2, Q_n(Psi_n>x)=1. For 2<=x<K_n+2 it is p_n, and for x>=K_n+2 it is zero.
+For n>=3 and d>=2,
+
+    (n^d+2)^(1/d)<=2n,       n^d+4<=n^{d+1},
+    phi_d(K_n+2)<=2(d+1)n log n.
+
+Let c_d=1/[2(d+1)]. Monotonicity gives, whenever 2<=x<K_n+2,
+
+    p_n=exp(-(3n+d)log n)
+       <=exp(-n log n)
+       <=exp(-c_d phi_d(K_n+2))
+       <=exp(-c_d phi_d(x)).                                 (B9)
+
+For x<2, use C_d=exp(c_d phi_d(2)) to extend the same bound. For larger x the
+tail is zero. Therefore (B1) holds with constants independent of n. The example
+also satisfies the uniform exponential-cap-moment conclusion of Theorem A.
+A large rare cap cannot be excluded just by knowing all unconditional moments.
+
+Finally
+
+    L_n=log(1/r_n)=n log n,
+    L_n/log L_n=n log n/(log n+loglog n) ~ n.                  (B10)
+
+Combining (B8) and (B10) proves (B3). A family indexed by every small r can be
+obtained by assigning this law at r_n and setting N_r=0,Psi_r=2 elsewhere;
+(B1) still holds. No continuity in r is among the hypotheses. The subsequence
+already disproves any purported universally stronger conclusion from (B1).
+
+## 4. The exact extra input: size-biased configuration moments
+
+For m_r>0 the formula in Proposition C defines a probability law because
+E N_r/m_r=1. It assigns zero mass to N_r=0. At N_r>=1,
+
+    (N_r)_q=N_r (N_r-1)_{q-1}.
+
+Integrating proves the identity in (B4), including when the result is infinite.
+Since (N-1)_{q-1}<=Psi^{q-1}, its upper bound follows. Thus
+
+    sup_r E_{P_r^sb}Psi_r^{q-1}<infinity and m_r<=Cr^3
+          imply E_{P_r}(N_r)_q<=C_q r^3.                     (B11)
+
+For q=2 the exact ratio E[N(N-1)]/E N is E_{P^sb}(N-1). If E N is two-sided of
+order r^3, boundedness of this size-biased mean is also necessary for an O(r^3)
+second factorial moment. Boundedness of the possibly loose Psi under that law
+is a sufficient, not necessary, replacement.
+
+The distinction from conditioning on nonemptiness is elementary but essential.
+Take P(N=0)=1/3, P(N=1)=1/2, P(N=3)=1/6. Then E N=1. Under count-size bias,
+N=1 and N=3 each have probability 1/2. Under P(.|N>=1), their probabilities
+are 3/4 and 1/4. They yield different expectations, even in a finite space.
+
+In the family of Section 3, P_n^sb is concentrated entirely on the rare outcome
+N_n=K_n. Consequently E_{P_n^sb}Psi_n=K_n+2 diverges, even though the original
+cap has a uniform stretched-super-exponential tail. This isolates precisely the
+correlation not controlled by (B1).
+
+For an actual point process, disintegrating the N-weighted configuration law by
+a tagged point is the appropriate entry to a Palm/marked-intensity argument.
+The current Gaussian research route called M'/H aims to supply such conditional
+marked control. This note neither proves that route nor assumes it to close C6.
+It explains why a new marked estimate is genuinely additional information.
+
+## 5. Verification and boundaries
+
+The public finite checker uses exact rational probabilities and integer falling
+factorials. It tests (B8), finite size-bias identities, the probability-tail
+steps, algebra behind (B9), the pathwise cap split and the W/Z exponent ledger.
+Its negative variants deliberately replace count-size bias by conditioning on
+nonemptiness, use the wrong rare probability, replace falling factorials with
+ordinary powers, lose the dimension, remove the +2 pin offset, or drop Z.
+
+Those checks are NOT a proof of all real-parameter tail integrals or asymptotic
+limits. The analytic arguments are the displayed derivations above. No numerical
+Gaussian constant, actual Gaussian lower saturation, all-d D5 acceptance, or
+independent formal alignment follows from the tests. No scientific register or
+source proof is altered. Classical truncation, Hölder, size-bias and power-law
+calculations are credited as such; there is no worldwide novelty claim.
+
+Context only, not mathematical inputs: Math-#140, the separate Claude successor
+#142, and the marked M'/H lane discussed in #140. Their exact context references
+are recorded in SOURCE_MAP.json. This note does not depend on those drafts being
+accepted or merged, and must not be used as their Gaussian verification.

frontiers/c6_count_cap_boundary_20260929/README.md

@@ -0,0 +1,22 @@
+# Count-cap method boundary
+
+Author-side mathematical candidate; nonauthor review required. Scientific effect NONE.
+
+PROOF.md proves an abstract factorial-moment implication from a rare first moment,
+an L2 likelihood bound and a global count-cap tail. An explicit finite probability
+family attains its logarithmic factor, so those hypotheses alone cannot prove the
+Gaussian program's hoped-for log-free result. This is NOT a Gaussian counterexample.
+
+The distinct practical conclusion is the exact count-size-biased identity: uniform
+marked cap moments would supply the extra input needed to remove the loss. Count
+size bias is not conditioning on a nonempty configuration.
+
+Run from this directory:
+
+    python -B -S verify.py --output /path/to/new-output
+    python -B -O -S verify.py --output /path/to/another-new-output
+
+Each runner verifies the flat packet, executes fifteen finite tests and six semantic
+negatives in both Python modes, and requires matching output pairs. It writes only
+outside the source directory. Finite checks do not certify the continuum arguments.
+No upstream Gaussian proof is consumed or locally replayed by this packet.

frontiers/c6_count_cap_boundary_20260929/RESULTS.json

@@ -0,0 +1,7 @@
+{
+  "tests_per_mode": 15,
+  "semantic_mutants_per_mode": 6,
+  "identical_output_pairs": 7,
+  "scientific_effect": "NONE",
+  "gaussian_analysis_verified": false
+}

frontiers/c6_count_cap_boundary_20260929/SOURCE_FILES.json

@@ -0,0 +1,48 @@
+{
+  "schema": 1,
+  "scientific_effect": "NONE",
+  "files": [
+    {
+      "path": "PROOF.md",
+      "bytes": 10406,
+      "sha256": "264a5e762f598145e9230aa0947acb2e0354efdb2e3adf65d331e7ee0ba52011",
+      "git_blob": "3d4c28a4ca8784b6c71c13ca804a817a6cb52e6f"
+    },
+    {
+      "path": "README.md",
+      "bytes": 1152,
+      "sha256": "5a9e0e57b29bb3956392e209683fb5c0310a25961b0cff993620bb9ad6c335ba",
+      "git_blob": "a783de28438824b4a91f01c97805396fe1ca755a"
+    },
+    {
+      "path": "RESULTS.json",
+      "bytes": 162,
+      "sha256": "3dd4a09160c4ebbae034e8ce3d7c2b878caab616eff1273473082fd3099dfc00",
+      "git_blob": "d9700273c9ce5d4998630d29b47560b4838d7b6a"
+    },
+    {
+      "path": "SOURCE_MAP.json",
+      "bytes": 971,
+      "sha256": "426417104bd9360c9e99536bbcf7a41adea622b3deed690144939ef6ca2927dd",
+      "git_blob": "49ce9a638320ea783f90d55fa085c3d8e23854e7"
+    },
+    {
+      "path": "barrier.py",
+      "bytes": 1767,
+      "sha256": "f4850d0dc5ed968fae6ddce7a8dfaff725795ca289e0625fd0af77668d61dfee",
+      "git_blob": "2dacdc83661e2b64d0dc5748fcc9d7d7258bf1c1"
+    },
+    {
+      "path": "test_barrier.py",
+      "bytes": 3953,
+      "sha256": "da754c80301d5d8ddfa60ef8092e13f0098286ecbf06b35619d0f4ba8ffc14fc",
+      "git_blob": "b2a3264b94c69d0b421bfafbac34c2e8ec87009b"
+    },
+    {
+      "path": "verify.py",
+      "bytes": 4721,
+      "sha256": "429e1d67961fff713ec6d11c63f564ac5b4f6b2161595f3776a772187ba5b3db",
+      "git_blob": "9428ba292a4c387d51a10c5a35ec9e40eb144b1d"
+    }
+  ]
+}

frontiers/c6_count_cap_boundary_20260929/SOURCE_MAP.json

@@ -0,0 +1,23 @@
+{
+  "scientific_effect": "NONE",
+  "mathematical_inputs": [],
+  "context_only": [
+    {
+      "repository": "d6g8k5htny-coder/Math-",
+      "pull_request": 140,
+      "commit": "09763caf5849c96ab291b4c51b2192c64529565f",
+      "path": "frontiers/c6_factorial_moment_20260929/PROOF.md",
+      "use": "Motivates rare-count/cap-tail inference; not an input to the abstract proof."
+    },
+    {
+      "repository": "d6g8k5htny-coder/Math-",
+      "pull_request": 142,
+      "commit": "aee04cd1eca597cfd45ca88df4b2fdc1728717f9",
+      "path": "frontiers/c6_sharpened_20260929/PROOF.md",
+      "use": "Separate growing-Cauchy-radius candidate. This packet neither duplicates nor accepts its Gaussian argument."
+    }
+  ],
+  "independence": "The author proposed the growing-radius route and reviewed inputs in the same account. This separate abstract result requires its own nonauthor review.",
+  "gaussian_optimality_claimed": false,
+  "global_factorial_order_closed": false
+}