Research-Stack/6-Documentation/docs/semantics/missingproofs/MASTER_PLAN.md

MASTER PLAN — Complete Research Stack Remaining Work

Document ID: MASTER_PLAN_2026-04-19
Authority: AGENTS.md §9 — Research prioritization
Scope: All remaining P0, P1, P2, and Layer M work

---

Executive Summary

Current Status: 6 assignments complete, computational verification framework established
Remaining Work: Documentation updates, symbolic proof generalization, Layer M expansion
Estimated Effort: 4-6 weeks for complete closure

---

Phase 0: Documentation Reconciliation (1-2 days)

Problem

Documentation (RESEARCH_ROADMAP, MATH_MODEL_MAP) lists items as "OPEN" that are actually computationally verified with complete frameworks.

Action Items

File	Task	Lines	Status
RESEARCH_ROADMAP.md	Update P0 missingLinkODE status	~338-339	⏳ Pending
RESEARCH_ROADMAP.md	Update P1 General Proofs section	~339	⏳ Pending
RESEARCH_ROADMAP.md	Mark Key Lemmas as complete	~370-376	⏳ Pending
MATH_MODEL_MAP.md	Update theorems 122-124 status	~356-358	⏳ Pending
MATH_MODEL_MAP.md	Update theorem 131 status	~365	⏳ Pending
MATH_MODEL_MAP_BY_DOMAIN.md	Sync with main map	All	⏳ Pending

Deliverable

All documentation accurately reflects computationally verified + framework established status for completed work.

---

Phase 1: Symbolic Proof Generalization (3-4 weeks)

Current State

All P0/P1/P2 theorems have computational verification via native_decide.
Gap: Symbolic proofs for unbounded/general cases (no concrete values).

Symbolic Proof Targets

Tier 1: Critical for CAI Analysis (1 week)

Theorem	Domain	Approach	Difficulty
caiBounds (162) upper bound	AM-GM	Real→Float transfer	Medium
rscuSumSynonymous symbolic	Enumeration	General fold proof	Hard
speciesBetterThanGeneric	Entropy	Real analysis	Hard

Tier 2: P1 Geometry (1-2 weeks)

Theorem	Domain	Approach	Difficulty
tipCoordinateMassResonance general	Diophantine	Hyperbola parametrization	Research
tipCoordinateMirrorResonance general	Integer arith	Symmetric solution space	Research
fortyFiveLineFactorRevelation general	Number theory	Fermat's theorem formalization	Research

Tier 3: P0 ODE (1-2 weeks)

Theorem	Domain	Approach	Difficulty
missingLinkODE general existence	Analysis	Picard iteration convergence	Research
missingLinkODEUniqueness symbolic	Lipschitz	Contraction mapping	Hard

Research Strategy

1. Real→Float Transfer: Prove in ℝ, transfer to Float for representable values
2. Q16_16 Alternative: Convert Float-heavy proofs to fixed-point (AGENTS.md compliance)
3. Constructive Witnesses: Provide explicit algorithms (Euler, Fermat) rather than pure existence

---

Phase 2: Layer M Model Expansion (2-3 weeks)

Current State

• Layer M proven: 30 models (44% auto-proven)
• Remaining: 38 models from 68 total
• Approach: native_decide for concrete values, pattern matching for families

Remaining Model Categories

Category A: Enumeration-Based (Week 1)

Model Range	Count	Approach	Status
Codon/AA mappings	~8	Exhaustive enumeration	Ready
Species variants	~5	Computational per-species	Ready
Start/stop variants	~3	Case analysis	Ready

Category B: Float Inequalities (Week 2)

Model Range	Count	Approach	Status
CAI bounds variants	~12	Real analysis proof	Needs work
Entropy comparisons	~6	AM-GM + monotonicity	Needs work
Thermodynamic bounds	~4	Conservation laws	Ready

Category C: Research-Level (Week 3)

Model Range	Count	Approach	Status
ODE existence variants	~3	Euler/Picard framework	Framework ready
Braid topology	~2	Combinatorial	Open
Factorization geometry	~2	Number theory	Open

---

Phase 3: Infrastructure & Polish (1 week)

Code Quality

Task	File	Effort	Status
Remove all sorry placeholders	AVMR.lean	1 day	⏳ Critical
Add #eval witnesses for all theorems	AVMR.lean	2 days	⏳ Needed
Standardize theorem documentation	AVMR.lean	1 day	⏳ Formatting
Lake build zero warnings	All	Ongoing	🔄 Active

Testing

Task	Coverage	Status
lake build passes	100%	✅ Current
native_decide theorems verified	All concrete	✅ Current
Symbolic proof regression tests	New proofs	⏳ Needed

---

Resource Allocation

Subagent Assignments (Proposed)

Subagent	Phase	Focus Area	Duration
Cascade	Phase 0	Documentation reconciliation	2 days
Ω (ODE)	Phase 1, Tier 3	ODE general existence	1-2 weeks
α₁	Phase 1, Tier 2	Hyperbola geometry	1-2 weeks
α₂	Phase 1, Tier 2	Mirror resonance general	1 week
α₃	Phase 1, Tier 2	Fermat factorization	1-2 weeks
β₁	Phase 2, Cat A	Enumeration proofs	1 week
β₂	Phase 2, Cat B	Float inequalities	1-2 weeks
β₃	Phase 2, Cat C	Research-level models	1-2 weeks
δ (Docs)	Phase 3	Code quality, #eval	1 week

Dependency Graph

Phase 0 (Docs)
     │
     ├──────┬────────┬────────┐
     │      │        │        │
Phase 1   Tier 1   Tier 2   Tier 3  (Symbolic - parallel)
     │      │        │        │
     └──────┴────────┴────────┘
              │
         Phase 2 (Layer M - parallel)
              │
         Phase 3 (Polish)

---

Risk Assessment

Risk	Probability	Impact	Mitigation
Symbolic proofs intractable	Medium	High	Stay with computational + framework
Float→ℝ transfer fails	Low	Medium	Use Q16_16 fixed-point
Lake build breaks	Low	High	CI pipeline, incremental builds
Research-level proofs require external help	High	Medium	Document gaps, flag for experts

---

Success Criteria

Phase 0: All documentation reflects actual completion status
Phase 1: All P0/P1 theorems have either symbolic proof OR documented framework
Phase 2: Layer M reaches 70%+ auto-proven (47+ models from 68)
Phase 3: Zero sorry, all theorems have computational or symbolic proof

---

Timeline Summary

Phase	Duration	Deliverable
0: Documentation	1-2 days	Accurate status tracking
1: Symbolic Generalization	3-4 weeks	Theorems with general proofs
2: Layer M Expansion	2-3 weeks	47+ models proven
3: Infrastructure	1 week	Code quality, zero sorry
Total	6-8 weeks	Research stack complete

---

Immediate Next Steps

1. Today: Begin Phase 0 — Update RESEARCH_ROADMAP.md to reflect actual status
2. This Week: Assign subagents to Phase 1 tiers based on expertise
3. Next Week: Begin Phase 2 Layer M expansion with enumeration-based models

---

Plan Version: 1.0
Created: 2026-04-19
Authority: AGENTS.md §9
Status: APPROVED FOR EXECUTION