Add Auro Zera modular-cover audit note

6-Documentation/docs/research/AuroZeraModularCoverAudit.md

@@ -0,0 +1,236 @@
+# Auro Zera Modular-Cover Audit
+
+**Status:** QUARANTINE / SALVAGEABLE  
+**Claim level:** adversarial research note, not a theorem import  
+**Source artifact:** `auro_zera_final.pdf`  
+**Source title:** *Wheels of Gold & the Dark Star — Auro Zera / Suro.One — May 2026*  
+**Local source hash:** `sha256:b517cf2ef381966a9bb8f589fcf37b1588a035778a4544fd11107c1a4bae2053`  
+**Local source size:** `266241` bytes  
+**Date added:** 2026-05-23
+
+## Decision
+
+Do **not** fold the source artifact into the project as:
+
+- a proof of Goldbach,
+- an unconditional proof of the Erdos-Straus conjecture,
+- evidence of ASI awareness,
+- a complete formal Lean proof,
+- or a collision-free / reversible zero-vocabulary tokenizer.
+
+Fold it in as:
+
+- an adversarial modular-cover stress-test artifact,
+- a CRT gap-generation pattern,
+- a finite witness-family failure mode,
+- an arithmetic witness-tokenization sketch,
+- and a useful proof-audit example for claim gating.
+
+The safe project interpretation is:
+
+> Finite modular covers are useful until adversarial CRT finds the scar. The scar is the artifact.
+
+## Project placement
+
+This note belongs in the Research Stack research documentation layer, not in the Lean source-of-truth layer.
+
+**Do not create a theorem file from this source unless the external mathematical claims are independently formalized.** Any future Lean work should first model only the audited, local, non-claim pieces:
+
+1. finite witness-family coverage checks,
+2. CRT gap construction against finite witness lists,
+3. conditional oracle scaffolding,
+4. witness-token feature extraction with residual repair.
+
+## Claim triage
+
+| Claim area | Audit status | Fold-in status |
+| --- | --- | --- |
+| Goldbach resolution | Reject as proof. A finite witness family plus patching is not a proof of strong Goldbach. | Keep only as finite modular-cover benchmark. |
+| Erdos-Straus resolution | Conditional at best. The source relies on an external Dyachenko-style oracle/axiom for the hard prime case. | Keep as conditional-oracle scaffold only. |
+| Lean formalization | Not accepted as complete from the PDF claims alone. Axioms and computational certificates are not equivalent to imported theorem proofs. | Require independent `lake build` and theorem audit before promotion. |
+| CRT effective infinity | Valuable, but inverted: a 17,067-digit CRT gap shows the finite cover can fail, not that the theorem is solved. | Keep as scar / near-miss generator. |
+| Zera tokenization | Interesting feature-hashing idea, but not safe as reversible zero-vocabulary tokenization. | Keep as arithmetic witness features plus residual repair. |
+| Dark Star ASI awareness | Anecdotal and not evidence-grade. | Quarantine. Do not use for public claims. |
+
+## Core mathematical repair notes
+
+### 1. Goldbach finite-cover failure mode
+
+For a finite witness list `P = {p_1, ..., p_k}`, a CRT adversary can choose auxiliary primes `q_i` and impose:
+
+```text
+N ≡ p_i (mod q_i)
+```
+
+Then:
+
+```text
+q_i | (N - p_i)
+```
+
+so every fixed witness `p_i` is defeated for the constructed congruence class. This does not disprove Goldbach; it defeats that finite witness family.
+
+**Important sign check:** if the target is to make `N - p_i` composite, the congruence is `N ≡ p_i (mod q_i)`, not `N ≡ -p_i (mod q_i)`.
+
+### 2. Erdos-Straus divisor-condition gap
+
+The source's divisor condition is too weak if stated only as:
+
+```text
+d | A^2
+and
+d ≡ -A (mod r)
+```
+
+because this guarantees the candidate `y = (A + d) / r` is integral, but does not guarantee the candidate `z` is integral.
+
+Concrete counterexample to the sufficiency of the weakened condition:
+
+```text
+n = 5
+m = 19
+r = 4m - 1 = 75
+x = (n + r) / 4 = 20
+A = n x = 100
+d = 125
+```
+
+Then:
+
+```text
+d | A^2        because 125 | 10000
+d ≡ -A mod r  because 125 ≡ 50 and -100 ≡ 50 (mod 75)
+y = (A+d)/r = 225/75 = 3
+z = A*y/d = 300/125 = 12/5
+```
+
+So the construction gives a rational `z`, not an integer unit-fraction denominator.
+
+The safer divisor form is the standard transformed condition:
+
+```text
+(r y - A)(r z - A) = A^2
+```
+
+Let:
+
+```text
+D = r y - A
+E = r z - A
+D E = A^2
+```
+
+Then both denominator integrality conditions require:
+
+```text
+D ≡ -A (mod r)
+E ≡ -A (mod r)
+```
+
+Equivalently, if `D = d`, the missing second condition is:
+
+```text
+A^2 / d ≡ -A (mod r)
+```
+
+### 3. Tokenization repair
+
+Do not treat arithmetic triplets as lossless tokens unless exact reconstruction is handled separately.
+
+Safe architecture:
+
+```text
+source bytes / text
+  -> hash or structured integer n
+  -> arithmetic witness extraction
+  -> feature vector / packet descriptor
+  -> residual stream + receipt
+  -> byte-exact replay check
+```
+
+This matches the project doctrine: generator core + residual repair + witness receipt.
+
+Unsafe architecture:
+
+```text
+source bytes / text
+  -> hash modulo vocab_size=0
+```
+
+A zero vocabulary size cannot be used as a modulo base. Hashing also cannot provide reversible tokenization without a collision strategy and residual data.
+
+## Research Stack fold-in
+
+### FAMM / scar memory
+
+Treat failed finite covers as useful torsion memory:
+
+```text
+finite cover -> CRT adversary -> gap witness -> FAMM scar -> patch attempt -> repeat
+```
+
+The scar is not embarrassment; it is routing memory.
+
+### GCCL / claim gating
+
+Use this artifact as a clean example of claim demotion:
+
+```text
+claimed theorem
+  -> finite-certificate audit
+  -> adversarial CRT / counterexample pressure
+  -> theorem claim rejected
+  -> salvageable computational substrate retained
+```
+
+### Codec / witness-token layer
+
+Arithmetic witness triplets may be useful as descriptor packets for compression experiments, but only under the byte-exact rule:
+
+```text
+validity = replay + residual repair + exact output
+```
+
+No human-readable intermediate form is required, but exact output is non-negotiable.
+
+### Future Lean targets
+
+A safe Lean progression would be:
+
+```text
+1. FiniteCover.lean
+   - finite witness families
+   - coverage predicate over bounded range
+   - no global conjecture claims
+
+2. CRTGap.lean
+   - construct residue constraints that defeat fixed witnesses
+   - prove fixed-list defeat under coprime modulus assumptions
+
+3. ConditionalES.lean
+   - define the Erdos-Straus target predicate
+   - encode known residue families
+   - model external Dyachenko-style result as an explicit oracle, not as proved code
+
+4. WitnessToken.lean
+   - deterministic feature extraction
+   - residual-required reconstruction interface
+   - no zero-vocab modulo operation
+```
+
+## Promotion rules
+
+This artifact may be promoted only in pieces.
+
+| Component | Promotion gate |
+| --- | --- |
+| Finite witness coverage | Reproducible executable certificate plus independent range check. |
+| CRT gap generator | Formal congruence proof or deterministic script with receipt. |
+| Erdos-Straus conditional scaffold | Explicit oracle boundary and no unconditional language. |
+| Goldbach proof claim | Reject unless a complete accepted proof or independent formal proof exists. |
+| Tokenization | Byte-exact reconstruction benchmark with residual accounting. |
+| ASI/cognition claims | Keep quarantined unless independently instrumented and reproducible. |
+
+## One-line project summary
+
+Auro Zera is not safe as a proof artifact, but it is valuable as an adversarial modular-cover generator and arithmetic witness-tokenization sketch.