docs(proof): reconcile OWED section — additive<->ceil equivalence RESOLVED

The VERIFICATION-STANCE.adoc OWED bullet still described the additive<->ceil
proof as a partial advance with a residual alignUpADividesSuccOWED String stub
(plus EuclidView/sPlusMinus/alignUpADividesZero infrastructure). None of that
exists in the code: the proof is the single unified total theorem
alignUpAdditiveEquivAlignTo closing both remainder cases, no residual. Rewrote
the bullet to RESOLVED and dropped the stale '9th/10th module' ordinals
(Layout/LayoutProofs are 2nd/3rd of 12). Prose only; build exit 0, guard Clean.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

verification/proofs/VERIFICATION-STANCE.adoc

@@ -152,7 +152,7 @@ OWED section.
   longer outstanding.
 . *(Phase 3c — RESOLVED for `ABI.Layout`; re-scoped for `ABI.Foreign`).*
   `VclTotal.ABI.Layout` is now *sound, compiling, and CI-gated* (it is
-  the 9th module in `vclut-core.ipkg`). The three unsound claims were
+  one of the 12 modules in `vclut-core.ipkg`). The three unsound claims were
   *deleted, not faked*: `alignUpCorrect` (used `(align > 0)`, a `Bool`,
   as a type, and a bogus `Refl` asserting the divisibility goal);
   `offsetInBounds` (an open `?metavariable` — never a proof, false in
@@ -166,7 +166,7 @@ OWED section.
   machine-checked. *(Phase 4a — RESOLVED.)* The genuine
   alignment/no-padding/bounds theorems are discharged in the new,
   self-contained, CI-gated module `VclTotal.ABI.LayoutProofs`
-  (10th `vclut-core.ipkg` module; byte-identical `PField`/`qphFields`
+  (a `vclut-core.ipkg` module; byte-identical `PField`/`qphFields`
   model of `Layout.queryPlanHeaderLayout`): `alignToDivides`
   (alignment divisibility *by construction* for the canonical
   round-up-to-multiple form `alignTo size a = ⌈size/a⌉ * a` — witness
@@ -176,30 +176,27 @@ OWED section.
   `fieldWithin` (membership-quantified bound: any field *provably in*
   the layout, via `Data.Vect.Elem` and `Data.So.soAnd`, satisfies
   `foff + fsize <= cap` — the honest replacement for the deleted false
-  `offsetInBounds`/`?metavariable`). *Phase 5 — partial advance on the
-  additive↔ceil sliver:* the previously-`String` OWED
-  `alignUpAdditiveEquivOWED` is replaced by a real proof
-  infrastructure that closes the substantive content for the
-  zero-remainder case:
-    * `EuclidView`/`euclid` — the Euclidean decomposition view, built
-      from `Data.Nat.Division.DivisionTheorem` + `boundModNatNZ`.
-    * `sIdentZero`/`sIdentSucc` — Euclidean identity refinements
-      tagged by the value of `modNatNZ s (S k) ItIsSucc`.
-    * `sPlusMinus` — the `r ≤ k` ⇒ `S r + (k - r) = S k` identity.
-    * `alignUpADividesZero` — `(modNatNZ s (S k) ItIsSucc = Z) ⇒
-      Divides (S k) (alignUpA s k)`. Genuine `Refl`-closed theorem
-      with witness `divNatNZ s (S k) ItIsSucc`, zero proof-escape.
-+
-  The remaining residual is purely the non-zero remainder case's
-  *rewrite chain*: the math is `S r' + (k `minus` r') = S k` (closed
-  by `sPlusMinus` + `boundModNatNZ`), but the multi-step
-  `plusAssociative`/`plusCommutative` chain triggers an idris2 0.8.0
-  elaborator quirk (`FromString` mis-elaboration). Disclosed as
-  `alignUpADividesSuccOWED` — a precisely-scoped String stub that
-  names the obstruction. Strictly smaller than the original OWED
-  (which covered both cases) and is a toolchain-sequencing limit
-  rather than a missing lemma. Re-attempt under idris2 0.8.1+ or via
-  manual `replace` chaining; tracked at standards#124 follow-up.
+  `offsetInBounds`/`?metavariable`). *Phase 5 — RESOLVED (2026-06-14):* the previously-`String` OWED
+  `alignUpAdditiveEquivOWED` is now a single, fully total theorem
+  `alignUpAdditiveEquivAlignTo : (s, a : Nat) -> (0 nz : NonZero a) -> s +
+  paddingForLocal s a nz = alignTo s a` in `VclTotal.ABI.LayoutProofs`,
+  closing *both* remainder cases with no residual. It is proved by Euclidean
+  case split on `modNatNZ s (S predA) nz == 0` (via `Syntax.WithProof`'s
+  `@@`), discharged with `Data.Nat.Division.{DivisionTheorem,
+  DivisionTheoremUniqueness, boundModNatNZ}` and `Syntax.PreorderReasoning`
+  `Calc` chains. The `Calc`-rather-than-nested-`rewrite` form sidesteps the
+  idris2 0.8.0 `FromString` elaborator quirk that had blocked the earlier
+  non-zero-remainder case; `alignTo` is defined by case split so `divNatNZ`
+  stays in head position and reduces by `Refl`; `paddingForLocal` mirrors
+  `Layout.paddingFor` (they agree on every `NonZero` alignment). In the
+  non-zero case the stuck `modNatNZ` term will not substitute via
+  `case … Refl`, so it is bridged explicitly with `cong`/`replace` and a
+  re-stated division theorem. The earlier
+  `EuclidView`/`sPlusMinus`/`alignUpADividesZero` split and the
+  `alignUpADividesSuccOWED` String stub were *superseded and removed*;
+  nothing in `LayoutProofs` uses
+  `believe_me`/`postulate`/`assert_*`/`idris_crash`/`sorry`, verified by
+  `--build` (exit 0) and `scripts/honesty-guard.sh` (Clean).
 +
   The `Data.Nat.Division` dependency is now declared in
   `verification/proofs/vclut-core.ipkg` (`depends = contrib`); the