# Gao Math Lab — reproducible research brief
Generated UTC: 2026-10-31T21:54:09+00:00

## Epistemic status
No global open problem was solved. Single-number checks are observations,
modular lemmas establish only explicitly delimited infinite residue classes.
Independent verification of each JSON certificate is required.

## Computation state
- Collatz next untested starting integer: 4289372
- Collatz individual starts checked: 4289370
- Goldbach next even integer: 4289374
- Goldbach individual even numbers checked: 2144685
- Residue classes processed: 8190
- Classes with k-step local descent certificates: 6423
- Next modular class: k=13, residue=0
- Alert: None

## Certified *local* lemmas (not claimed new)
- k=12, n mod 4096=4, T^k(n)=(243n + 3124) / 4096, valid descent if n >= 4. Certificate: lemma_k12_r4.json
- k=12, n mod 4096=3, T^k(n)=(729n + 6005) / 4096, valid descent if n >= 3. Certificate: lemma_k12_r3.json
- k=12, n mod 4096=2, T^k(n)=(729n + 6734) / 4096, valid descent if n >= 4098. Certificate: lemma_k12_r2.json
- k=12, n mod 4096=1, T^k(n)=(729n + 3367) / 4096, valid descent if n >= 4097. Certificate: lemma_k12_r1.json
- k=12, n mod 4096=0, T^k(n)=(1n + 0) / 4096, valid descent if n >= 4096. Certificate: lemma_k12_r0.json

## Next research protocol for Codex
1. Compare all claims against published mathematics before calling anything novel.
2. Propose a specific generalized invariant or a shorter residue-covering proof.
3. State a falsifiable finite test; implement it in a separate branch.
4. Attempt an independently checked arithmetic certificate or Lean proof.
5. Attempt adversarial counterexamples before claiming a theorem.
6. Do not auto-deploy self-written code or authorize compute/API spending.
7. Report proof obligation, assumptions, counterexamples, resource usage.


## Bounded conjecture research queue
Run 4: completed
Model calls: 0; novelty remains unassessed.
- #1: ∀ n∈ℕ, n>1 → ∃ j∈[1,2], Tʲ(n)<n — falsified; Lean: not_checked; literature: leads_found
- #2: ∀ n∈ℕ, n≥1 ∧ n mod 4=1 → T^2(n)<n — falsified; Lean: not_checked; literature: leads_found
- #3: ∀ n∈ℕ, n≥5 ∧ n mod 4=1 → T^2(n)<n — formally_verified_local; Lean: checked; literature: leads_found