Coherence pass 4 (the closing pass): 4-tier apex documentation + hygiene

- README: pyramid-diagram apex row upgraded to the proven full lift
  (accepted <=> decompress(R) = [k](-A)+[s]B), status table names all
  four button-enforced tiers, apex section gains the phase-2 tier table
  (half-lift / point equation / full lift) + the decompress-chain
  summary; source pin updated to the pushed patch commit.
- TRUSTED-BASE item 5: rewritten from the single byte-apex certificate
  to the FOUR enforced tiers (decompress_of_canonical noted as
  standard-three-only).
- gen/CurveField/FunsExternal.lean: stale root-namespace
  edwards.decompress.step_1/step_2 axioms removed (dead weight left
  behind by un-opaquing; outside every cone, but they forced
  fully-qualified unfolds - see control FAILURES.md).
- check.sh Phase 3b success echo aligned to "apex + full-lift" (echo
  only; the enforcing greps covered all four tiers already).

Validated by the pass-4 sweep: 9/9 buttons green (this repo's check.sh
+ check-scalar.sh among them), logs retained in the pass workspace.
Full record: formal-verification-control/COHERENCE-PASS-4.md.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

README.md

@@ -5,7 +5,7 @@ coherent proof pyramid in Lean 4 via the Charon/Aeneas transpilation pipeline:
 
 ```
         ┌──────────────────────────────┐
-        │  Signature (EdDSA verify)    │   accepted ⇔ compress([s]B−[k]A) = R
+        │  Signature (EdDSA verify)    │   accepted ⇔ decompress(R) = [k](−A)+[s]B
         ├──────────────────────────────┤
         │  Scalar arithmetic mod ℓ     │   Scalar52 ops correct mod ℓ
         ├──────────────────────────────┤
@@ -28,12 +28,12 @@ in this repository.
 | Field 𝔽_p          | `fieldImplementation`    | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
 | Group law (Edwards) | `edwardsImplementation`  | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
 | Scalar mod ℓ        | `scalarImplementation` (add ✅ sub ✅ mul ✅) | ✅ proven | `[propext, Classical.choice, Quot.sound]` |
-| Signature (EdDSA)   | `verify_accepts_iff` | ✅ proven (phase 1) | standard three + the button-enforced SHA-512/wire-format boundary — see [The signature apex](#the-signature-apex-phase-1) |
+| Signature (EdDSA)   | `verify_accepts_iff` … `verify_accepts_iff_decompress` (4 tiers) | ✅ proven (phases 1+2) | standard three + the button-enforced SHA-512/wire-format boundary — see [The signature apex](#the-signature-apex-phases-1-and-2) |
 
 Status legend: ✅ proven & axiom-audited · ⏳ in progress · ❌ not started.
 This table is updated only when `verification/check.sh` passes for the layer.
 
-## The signature apex (phase 1)
+## The signature apex (phases 1 and 2)
 
 The apex certificate `CurveFieldProofs.verify_accepts_iff` is the literal EdDSA
 acceptance criterion, proven about the extracted verifier:
@@ -51,7 +51,7 @@ makes the incremental-hasher types untranslatable) and the wire-format types
 stay opaque.
 
 `check.sh` has a dedicated audit phase (Phase 3b) that fails the build unless
-the apex certificate's axiom cone is **exactly**
+each apex-tier certificate's axiom cone is **exactly**
 
 `[propext, Classical.choice, Quot.sound]` + `{ed25519.Signature, verifying.sha512_hash3, ed25519.Signature.to_bytes, signature.error.Error, signature.error.Error.new}`
 
@@ -60,16 +60,30 @@ boundary. Zero curve, scalar, or backend axioms. The companion certificate
 `verify_loop_full` (the 32-byte comparison loop computes array equality)
 carries the standard three axioms only.
 
-**Phase 2 (deferred, documented):** lifting the byte-level equation to the
+**Phase 2 (complete): the point-level lift.** Phase 3b enforces the SAME
-point level (`[s]B − [k]A = decompress R`) additionally needs `compress`
+axiom boundary on three further tiers that lift the byte equation to points:
-canonicity and a verified `decompress`; it is deliberately out of scope for
+
-this milestone, mirroring the layer-by-layer phase split used below the apex.
+| Tier | Certificate | Statement |
+|------|-------------|-----------|
+| half-lift | `verify_accepts_iff_point` | accepted ⇔ R = the **canonical encoding** of `[k]·(−A) + [s]·B` (compress semantics + `as_bytes` canonicity + hash-to-scalar, recompute chain inverted) |
+| point equation | `verify_accepts_iff_point_eq` | for any valid on-curve `Q` canonically encoded by R: accepted ⇔ `Q = [k]·(−A) + [s]·B` **as points** (encoding-injectivity: d non-square + parity root-selection) |
+| full lift | `verify_accepts_iff_decompress` | R **decompresses** to a valid on-curve `Pt`, and accepted ⇔ `Pt = [k]·(−A) + [s]·B` — the constructive capstone |
+
+The full lift runs through the extracted `CompressedEdwardsY::decompress`
+itself, proven end-to-end: `from_bytes` parses the y-residue exactly below
+bit 255 (`from_bytes_spec`), `sqrt_ratio_i` returns the even square root of
+`(y²−1)/(dy²+1)` (`sqrt_ratio_i_sq_spec`, Fermat-exponent square root), and
+the sign bit selects the x-parity (`decompress_of_canonical`, standard three
+axioms). Byte comparison ↔ encoding equality ↔ point equality ↔
+decompressed-point equality: every link is machine-checked over the
+extracted code, and `check.sh` fails the build if any of the four tiers'
+cones deviates from the boundary above.
 
 
 ## Source
 
 - **Upstream**: [betrusted-io/curve25519-dalek](https://github.com/betrusted-io/curve25519-dalek), commit `16e087a`
-- **Pinned/patched source**: [saymrwulf/betrusted-curve25519-dalek-source](https://github.com/saymrwulf/betrusted-curve25519-dalek-source), commit `64ee8f0`
+- **Pinned/patched source**: [saymrwulf/betrusted-curve25519-dalek-source](https://github.com/saymrwulf/betrusted-curve25519-dalek-source), commit `cee0e17` (adds the decompress step_2 negate-then-assign patch)
 - **Patches**: minimal Aeneas-compatibility only (documented in the source repo)
 - **Scope caveat**: this verifies the fork's pure-Rust `serial/u64` path. The Engine25519 hardware-accelerator path on Precursor is different code and is NOT covered by these proofs.
 

TRUSTED-BASE.md

@@ -15,18 +15,25 @@ running Rust code. Everything else is machine-checked.
    plumbing, formatting) are axiomatized as opaque symbols. The axiom audit
    proves none of these axioms enters the dependency cone of any certificate,
    except where a model is explicitly listed below.
-5. **The signature-apex boundary (signature layer only)**: the apex
+5. **The signature-apex boundary (signature layer only)**: FOUR apex-tier
-   certificate `CurveFieldProofs.verify_accepts_iff` ("the verifier accepts
+   certificates — `CurveFieldProofs.verify_accepts_iff` (byte apex:
-   iff compress([s]·B − [k]·A) = R byte-for-byte") is `#print axioms`-audited
+   accepted iff compress([s]·B − [k]·A) = R byte-for-byte),
-   by check.sh Phase 3b against EXACTLY the standard three plus this
+   `verify_accepts_iff_point` (half-lift: R is the canonical encoding of
-   documented set, and the build fails on any deviation:
+   the recomputed point), `verify_accepts_iff_point_eq` (point equation:
+   canonically-encoded Q accepted iff Q equals the recomputed point), and
+   `verify_accepts_iff_decompress` (full lift: R decompresses to a valid
+   on-curve point that equals the recomputed point) — are each
+   `#print axioms`-audited by check.sh Phase 3b against EXACTLY the
+   standard three plus this documented set, and the build fails on any
+   deviation:
    `ed25519.Signature` (wire-format type), the single SHA-512 oracle
    `verifying.sha512_hash3` (semantically `Sha512(R ‖ A ‖ msg)`),
    `ed25519.Signature.to_bytes`, and `signature.error.Error`/`Error.new`
    (opaque error type). The hash is an oracle with no algebraic properties
-   assumed — the theorem holds for whatever bytes it produces; the SHA-512
+   assumed — the theorems hold for whatever bytes it produces; the SHA-512
    implementation itself is NOT verified. Zero curve, scalar, or backend
-   axioms are in the cone.
+   axioms are in any of the four cones. The constructive decompress theorem underneath the full lift
+   (`decompress_of_canonical`) carries the standard three axioms ONLY.
 6. **Compilation of Rust to machine code** (rustc backend) is out of scope,
    as is side-channel behaviour (timing, speculation). The proofs are about
    functional correctness at the MIR/LLBC level.

verification/gen/CurveField/FunsExternal.lean

@@ -357,23 +357,6 @@ axiom
     (backend.serial.curve_models.AffineNielsPoint ×
     backend.serial.curve_models.AffineNielsPoint)
 
-/-- [curve25519_dalek::edwards::decompress::step_2]:
-    Source: 'curve25519-dalek/src/edwards.rs', lines 223:4-240:5 -/
-axiom edwards.decompress.step_2
-  :
-  edwards.CompressedEdwardsY → backend.serial.u64.field.FieldElement51 →
-    backend.serial.u64.field.FieldElement51 →
-    backend.serial.u64.field.FieldElement51 → Result edwards.EdwardsPoint
-
-/-- [curve25519_dalek::edwards::decompress::step_1]:
-    Source: 'curve25519-dalek/src/edwards.rs', lines 209:4-220:5 -/
-axiom edwards.decompress.step_1
-  :
-  edwards.CompressedEdwardsY → Result (subtle.Choice ×
-    backend.serial.u64.field.FieldElement51 ×
-    backend.serial.u64.field.FieldElement51 ×
-    backend.serial.u64.field.FieldElement51)
-
 /-- [curve25519_dalek::edwards::{curve25519_dalek::edwards::CompressedEdwardsY}::from_slice]:
     Source: 'curve25519-dalek/src/edwards.rs', lines 404:4-406:5
     Visibility: public -/