Context
PR #164 (Lean 4 verification spike Stages 1–6) merged 2026-05-11. The in-repo tracker verification/ROADMAP.md records Tiers 1, 1.5, and 1.6 as complete and explicitly names Tier 2 as the next step, recommending an OpenSpec change on start:
"Tier 2 is the first place where the roadmap becomes specification-heavy enough to deserve an OpenSpec change on start."
"The natural next OpenSpec artifact is ... 'build a definitional OoxmlDoc subset and close INV-FIELD-001 against it.'"
Goal
Author the OpenSpec change add-ooxml-doc-subset-and-inv-field-001-proof covering:
- A definitional Lean OOXML subset (small tree, not a tape — nests
w:ins/w:del/w:moveFrom/w:moveTo, models w:delInstrText).
- Definitional Lean
accept / reject operations mirroring packages/docx-core/src/baselines/atomizer/trackChangesAcceptorAst.ts:368-659.
- A Lean
validateFieldStructure predicate mirroring packages/docx-core/src/baselines/atomizer/pipeline.ts:352-402.
- A closed Lean proof of
inv_field_001 replacing the sorry at verification/lean/LeanSpike/Spec.lean:71.
inv_rt_001 (sorry at Spec.lean:95) is explicitly deferred to a successor change. Lean↔TS equivalence (Tier 2.5) and reconstruction invariants (Tier 3) get separate proposals.
Scope guardrails
- Inplace-mode comparison output only (matches the
Spec.lean:66 hypothesis).
- Quantifies over the full input domain
Spec.lean:66 quantifies over — both plain-text and field-bearing inputs.
- No hierarchical paragraph-level LCS; no reconstruction beyond accept/reject.
- No field-bearing fast-check arbitrary in this change (separate follow-up).
Implementation pattern
After the proposal merges, each tasks.md item (T1, T2, T3a, T3b, T4a, T4b, T5a, T5b) gets its own GitHub issue and is implemented via /codex-implement <issue> — same cadence that shipped Stages 2/3/4/5 of the original spike.
References
Context
PR #164 (Lean 4 verification spike Stages 1–6) merged 2026-05-11. The in-repo tracker
verification/ROADMAP.mdrecords Tiers 1, 1.5, and 1.6 as complete and explicitly names Tier 2 as the next step, recommending an OpenSpec change on start:Goal
Author the OpenSpec change
add-ooxml-doc-subset-and-inv-field-001-proofcovering:w:ins/w:del/w:moveFrom/w:moveTo, modelsw:delInstrText).accept/rejectoperations mirroringpackages/docx-core/src/baselines/atomizer/trackChangesAcceptorAst.ts:368-659.validateFieldStructurepredicate mirroringpackages/docx-core/src/baselines/atomizer/pipeline.ts:352-402.inv_field_001replacing the sorry atverification/lean/LeanSpike/Spec.lean:71.inv_rt_001(sorry atSpec.lean:95) is explicitly deferred to a successor change. Lean↔TS equivalence (Tier 2.5) and reconstruction invariants (Tier 3) get separate proposals.Scope guardrails
Spec.lean:66hypothesis).Spec.lean:66quantifies over — both plain-text and field-bearing inputs.Implementation pattern
After the proposal merges, each
tasks.mditem (T1, T2, T3a, T3b, T4a, T4b, T5a, T5b) gets its own GitHub issue and is implemented via/codex-implement <issue>— same cadence that shipped Stages 2/3/4/5 of the original spike.References
verification/ROADMAP.md:73-97Spec.lean:verification/lean/LeanSpike/Spec.lean