proofs(Layer 1.0 follow-up): stripIsIdentityOnStrippedBody — slash-slash closure

[hyperpolymath]

Context

PR #111 landed the Layer 1.0 foundation for line-comment stripping:

• stripLineCommentBody + stripLineComments total Idris2 definitions mirroring src/assail/analyzer.rs:931.
• IsStrippedBody shape predicate + stripBodyProducesStrippedShape lemma (Qed).
• Base cases of stripLineCommentsIdempotent (empty + non-slash-headed input) (Qed).
• 3 concrete sanity tests (Refl).

What's open

The slash-slash inductive case of stripLineCommentsIdempotent requires:

stripIsIdentityOnStrippedBody :
    (xs : List Char) -> IsStrippedBody xs ->
    stripLineComments xs = xs

Three constructor cases:

• StripEmpty → Refl
• StripJustNl tail → requires a second induction on tail (arbitrary content)
• StripSpaceCons rest _ → unfold strip on sp + IH

Once that lemma is closed, the slash-slash case of the main theorem is cong (sp :: sp ::) (bodyOutputIdempotent rest).

Acceptance

• No believe_me / assert_total / holes.
• All existing PR proofs(Layer 1.0): Idris2 stripping foundation — base cases + shape lemma #111 tests still pass.
• PROOF-NEEDS.md 'What Still Needs Proving' Layer-1.0 row for this obligation gets moved to 'Completed Proofs'.

Refs

• PROOF-PROGRAMME.md row 1 (Layer 1.0)
• PR proofs(Layer 1.0): Idris2 stripping foundation — base cases + shape lemma #111 (the foundation)
• src/abi/Stripping.idr (the file to extend)

[hyperpolymath]

Closed by panic-attack#119 (merged 2026-06-02 19:22Z).

The slash-slash inductive case of stripLineCommentsIdempotent is now Qed-closed via the mutual-recursive bodyIsFixedPoint lemma. The previous PR #111 model has also been corrected — it had a semantic bug where only the FIRST line comment was stripped; the corrected model uses mutual recursion (stripLineComments ↔ stripLineCommentBody) so the body-stripper calls back into the main stripper at each preserved newline, processing the entire input in one pass.

No believe_me / assert_total / holes.

New sanity-check theorem sanityTwoComments exercises the case PR #111's broken model would have failed.

Remaining Layer-1.0 work (block + strings + composition + position-preservation) tracked in #114.