Per-wrapper field-context neutrality runtime gate (engine-side mirror of Lean residual axiom)

[stevenobiajulu]

Context

PR #208 introduces a residual axiom compareDocumentXml_output_recursivelyWellformed asserting that every <w:ins> / <w:del> / <w:moveFrom> / <w:moveTo> wrapper subtree in inplace-comparison output is field-context-neutral. The Lean proof depends on this; today the only verification is a single bridge-test fixture (NUMPAGES insertion) which exercises zero adverse atom shapes.

This issue tracks lifting the per-wrapper neutrality check into the TS engine itself as a runtime safety gate, so the residual axiom becomes a checked invariant rather than a load-bearing assumption.

What needs to change

• Port the bridge test's isFieldContextNeutral (currently at packages/docx-core/src/integration/lean-spec-bridge.test.ts:704-738) into engine code, callable from evaluateSafetyChecks at packages/docx-core/src/baselines/atomizer/pipeline.ts:404-440.
• The check should walk every w:ins/w:del/w:moveFrom/w:moveTo wrapper subtree and verify it doesn't disturb the outer field context (pop on empty, flip separator on empty, or leave the stack changed when returning to outer scope).
• When the check fires in production, surface a ReconstructionSafetyCheckName failure so the pipeline falls back to rebuild mode rather than emitting non-conformant inplace XML.

Dependency — must wait for PR #208 follow-up

The current Lean predicate uses ∀ ctx, walkBlocks (.ok ctx) bs = .ok ctx — universal over all outer contexts. ECMA-376 deep research showed this is too strong for conformant field-fragmentation outputs (e.g., a <w:ins> containing only <w:instrText> is conformant but not context-neutral under empty ctx). PR #208 will be updated to weaken the predicate to a path-conditional form (neutral under the contexts the walk actually reaches it with, not ∀ ctx).

Do not start this issue until PR #208's path-conditional predicate lands. Otherwise the runtime check will reject conformant fragmented-field outputs.

Acceptance

• Engine-side assertRecursivelyWellformed analogue exists.
• Called from evaluateSafetyChecks on every inplace candidate.
• Failure triggers ReconstructionSafetyCheckName.recursiveFieldWellformedness (or similar) and rebuild fallback.
• At least one regression fixture in lean-spec-bridge.test.ts exercises the path where a fragmented field passes the runtime check.

Ref: #208, #209.

[stevenobiajulu]

Update (post-PR #219): the Lean-side predicate has now been weakened from per-subtree ∀ ctx neutrality to document-level Tier2.AcceptReject.preservationFriendly. This changes what a runtime gate would check:

• Original design (per-wrapper isFieldContextNeutral lifted into the engine) — no longer matches what the axiom asserts.
• New shape — verify the engine's combined output is preservationFriendly at runtime by:
  1. Computing the field-context walk over combinedXml.
  2. Running accept and reject; computing the field-context walk over each output.
  3. Confirming the walks end in identical contexts and that begin/end counts balance.
     This is approximately what the safety checks at pipeline.ts:439-440 already do via validateFieldStructure(acceptedXml) && validateFieldStructure(rejectedXml) — the new gate would just add the walk-equality assertion alongside.

Still depends on #217 landing first, because once the engine fragments fields, the bridge test's existing assertRecursivelyWellformed per-wrapper check will need to be removed first (it currently over-checks the old ∀ ctx property).

Sequencing: #217 → adjust this issue's design → implement.