diff --git a/CLAUDE.md b/CLAUDE.md
index c6b6886c63..fdef13906b 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -8,7 +8,7 @@ This file provides guidance to Claude Code (claude.ai/code) when working with co
 
 Perry is a native TypeScript compiler written in Rust that compiles TypeScript source code directly to native executables. It uses SWC for TypeScript parsing and LLVM for code generation.
 
-**Current Version:** 0.5.1452
+**Current Version:** 0.5.1453
 
 
 ## TypeScript Parity Status
diff --git a/Cargo.lock b/Cargo.lock
index 7a6d59d8c7..c3b19cf5de 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -5547,7 +5547,7 @@ checksum = "9b4f627cb1b25917193a259e49bdad08f671f8d9708acfd5fe0a8c1455d87220"
 
 [[package]]
 name = "perry"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "base64",
@@ -5607,14 +5607,14 @@ dependencies = [
 
 [[package]]
 name = "perry-api-manifest"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "serde",
 ]
 
 [[package]]
 name = "perry-audio-miniaudio"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "cc",
  "libc",
@@ -5622,7 +5622,7 @@ dependencies = [
 
 [[package]]
 name = "perry-codegen"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "inkwell",
@@ -5639,7 +5639,7 @@ dependencies = [
 
 [[package]]
 name = "perry-codegen-arkts"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "perry-hir",
@@ -5647,7 +5647,7 @@ dependencies = [
 
 [[package]]
 name = "perry-codegen-glance"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "perry-hir",
@@ -5655,7 +5655,7 @@ dependencies = [
 
 [[package]]
 name = "perry-codegen-js"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "perry-dispatch",
@@ -5664,7 +5664,7 @@ dependencies = [
 
 [[package]]
 name = "perry-codegen-swiftui"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "perry-hir",
@@ -5672,7 +5672,7 @@ dependencies = [
 
 [[package]]
 name = "perry-codegen-wasm"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "base64",
@@ -5684,7 +5684,7 @@ dependencies = [
 
 [[package]]
 name = "perry-codegen-wear-tiles"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "perry-hir",
@@ -5692,7 +5692,7 @@ dependencies = [
 
 [[package]]
 name = "perry-container-compose"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "async-trait",
@@ -5721,14 +5721,14 @@ dependencies = [
 
 [[package]]
 name = "perry-container-e2e"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
 ]
 
 [[package]]
 name = "perry-diagnostics"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "serde",
  "serde_json",
@@ -5736,7 +5736,7 @@ dependencies = [
 
 [[package]]
 name = "perry-dispatch"
-version = "0.5.1452"
+version = "0.5.1453"
 
 [[package]]
 name = "perry-doc-fixture-my-bindings"
@@ -5747,7 +5747,7 @@ dependencies = [
 
 [[package]]
 name = "perry-doc-tests"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "clap",
@@ -5762,7 +5762,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-ads"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "block2",
  "objc2",
@@ -5772,7 +5772,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-argon2"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "argon2",
  "perry-ffi",
@@ -5780,7 +5780,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-axios"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "reqwest",
@@ -5789,7 +5789,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-bcrypt"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "bcrypt",
  "perry-ffi",
@@ -5797,7 +5797,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-better-sqlite3"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "rusqlite",
@@ -5805,7 +5805,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-cheerio"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "scraper",
@@ -5813,7 +5813,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-commander"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "perry-runtime",
@@ -5821,7 +5821,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-cron"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "chrono",
  "cron",
@@ -5831,7 +5831,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-dayjs"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "chrono",
  "perry-ffi",
@@ -5839,7 +5839,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-decimal"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "rust_decimal",
@@ -5847,7 +5847,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-dotenv"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "serde_json",
@@ -5855,7 +5855,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-ethers"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "rand 0.10.1",
@@ -5863,7 +5863,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-events"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "perry-runtime",
@@ -5871,14 +5871,14 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-exponential-backoff"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
 ]
 
 [[package]]
 name = "perry-ext-fastify"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "bytes",
  "http-body-util",
@@ -5896,7 +5896,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-fetch"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "bytes",
  "lazy_static",
@@ -5909,7 +5909,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-http"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "bytes",
  "h2",
@@ -5933,7 +5933,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-ioredis"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "lazy_static",
  "perry-ffi",
@@ -5943,7 +5943,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-jsonwebtoken"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "base64",
  "jsonwebtoken",
@@ -5954,7 +5954,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-lru-cache"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "lru",
  "perry-ffi",
@@ -5963,7 +5963,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-moment"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "chrono",
  "perry-ffi",
@@ -5971,7 +5971,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-mongodb"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "bson",
  "futures-util",
@@ -5983,7 +5983,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-mysql2"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "chrono",
  "perry-ffi",
@@ -5993,7 +5993,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-nanoid"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "nanoid",
  "perry-ffi",
@@ -6002,7 +6002,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-net"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "bytes",
  "perry-ffi",
@@ -6015,7 +6015,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-node-forge"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "const-oid 0.9.6",
  "der 0.7.10",
@@ -6034,7 +6034,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-nodemailer"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "lettre",
  "perry-ffi",
@@ -6044,7 +6044,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-pdf"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "printpdf",
@@ -6052,7 +6052,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-pg"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "sqlx",
@@ -6061,7 +6061,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-ratelimit"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "governor",
  "perry-ffi",
@@ -6069,7 +6069,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-sharp"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "fast_image_resize",
  "image",
@@ -6079,14 +6079,14 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-slugify"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
 ]
 
 [[package]]
 name = "perry-ext-streams"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "lazy_static",
  "perry-ffi",
@@ -6095,7 +6095,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-undici"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "perry-runtime",
@@ -6104,7 +6104,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-uuid"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "uuid",
@@ -6112,7 +6112,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-validator"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ffi",
  "regex",
@@ -6122,7 +6122,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-ws"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "futures-util",
  "lazy_static",
@@ -6135,7 +6135,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ext-zlib"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "brotli",
  "flate2",
@@ -6145,7 +6145,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ffi"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "dashmap",
  "once_cell",
@@ -6154,7 +6154,7 @@ dependencies = [
 
 [[package]]
 name = "perry-hir"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "perry-api-manifest",
@@ -6172,7 +6172,7 @@ dependencies = [
 
 [[package]]
 name = "perry-parser"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "perry-diagnostics",
@@ -6184,7 +6184,7 @@ dependencies = [
 
 [[package]]
 name = "perry-runtime"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "base64",
@@ -6226,14 +6226,14 @@ dependencies = [
 
 [[package]]
 name = "perry-runtime-static"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-runtime",
 ]
 
 [[package]]
 name = "perry-stdlib"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "aes 0.8.4",
  "aes 0.9.1",
@@ -6328,14 +6328,14 @@ dependencies = [
 
 [[package]]
 name = "perry-stdlib-static"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-stdlib",
 ]
 
 [[package]]
 name = "perry-transform"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "perry-hir",
@@ -6344,14 +6344,14 @@ dependencies = [
 
 [[package]]
 name = "perry-ui"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ui-model",
 ]
 
 [[package]]
 name = "perry-ui-android"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "base64",
  "itoa",
@@ -6368,7 +6368,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-geisterhand"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "rand 0.10.1",
  "serde",
@@ -6378,7 +6378,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-gtk4"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "base64",
  "cairo-rs 0.22.0",
@@ -6401,7 +6401,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-ios"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "base64",
  "block2",
@@ -6417,7 +6417,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-macos"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "base64",
  "block2",
@@ -6432,7 +6432,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-model"
-version = "0.5.1452"
+version = "0.5.1453"
 
 [[package]]
 name = "perry-ui-test"
@@ -6443,11 +6443,11 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-testkit"
-version = "0.5.1452"
+version = "0.5.1453"
 
 [[package]]
 name = "perry-ui-tvos"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "base64",
  "block2",
@@ -6463,7 +6463,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-visionos"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "base64",
  "block2",
@@ -6479,7 +6479,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-watchos"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "block2",
  "libc",
@@ -6492,7 +6492,7 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-windows"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "base64",
  "libc",
@@ -6509,14 +6509,14 @@ dependencies = [
 
 [[package]]
 name = "perry-ui-windows-winui"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "perry-ui-windows",
 ]
 
 [[package]]
 name = "perry-updater"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "anyhow",
  "base64",
@@ -6532,7 +6532,7 @@ dependencies = [
 
 [[package]]
 name = "perry-wasm-host"
-version = "0.5.1452"
+version = "0.5.1453"
 dependencies = [
  "wasmi",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index cb34520397..ad207d533d 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -315,7 +315,7 @@ codegen-units = 16
 codegen-units = 16
 
 [workspace.package]
-version = "0.5.1452"
+version = "0.5.1453"
 edition = "2021"
 license = "MIT"
 repository = "https://github.com/PerryTS/perry"
diff --git a/changelog.d/7774-element-group-numeric-proof.md b/changelog.d/7774-element-group-numeric-proof.md
new file mode 100644
index 0000000000..747f9bd942
--- /dev/null
+++ b/changelog.d/7774-element-group-numeric-proof.md
@@ -0,0 +1,32 @@
+**repsel: element-group members now claim numeric fields — proven reads drop `js_number_coerce` (#7770, PR #7774).**
+
+A `Ptr<Shape>`-proven `const r = a[i]` (or a producer pushed into an
+element-shape-proven array) stood down to zero numeric fields, so every
+declared-`number` field read paid the Phase-5a checked load with a cold
+`js_number_coerce` arm. The stand-down existed because one member's stores
+cannot witness a sibling's — but the E1–E5 containment that licenses the
+SHAPE proof also closes the group's store universe, so the exhaustive
+reachable-store proof is now discharged once per array root
+(`collectors/ptr_shape_numeric.rs::prove_group_numeric_fields`): constructor
+parameters resolve as the meet over every push's `new` argument list, member
+field stores are unioned, and method parameters resolve through group-merged
+call sites. Every member carries the group verdict; group integrity drops
+claim and fact together when any member fails rule 2.
+
+Constructor arguments like `new P(i, i + 1)` additionally needed the loop
+counter: `collect_numeric_by_construction_locals` proves locals whose every
+write is number-producing by construction (optimistic greatest fixpoint like
+`collect_not_bigint_locals`, with no declared-type leaf — annotations stay
+untrusted; a no-init `let` poisons). The expression proof consults it in
+function scope, and `i++` as a value resolves through the not-BigInt fact.
+
+On the issue's reproducer the read loop's `js_number_coerce` sites go 4 → 0
+while `--opt-report` still shows the `Ptr<Shape>` promotion; output verified
+byte-identical vs Node 26.5.1 across sibling/push-site/method poison
+channels, NaN / Infinity / −0 payloads, and `null`/`{}`/`1n`/`true` stores
+(`test-files/test_gap_repsel_element_group_numeric.ts`), and a
+`PERRY_GC_ZEAL=1 PERRY_GC_PROTECT_FROMSPACE=1` run relocated 4014 objects
+under the bare loads with a clean verdict. Pass 4 moved wholesale into the
+`ptr_shape_numeric.rs` child module for the 2000-line gate. A neighbouring
+PRE-EXISTING divergence found during validation (`o.x + 1` coercing where
+Node concatenates, plus an evaporating any-laundered add) is filed as #7773.
diff --git a/crates/perry-codegen/src/collectors/ptr_shape.rs b/crates/perry-codegen/src/collectors/ptr_shape.rs
index e2a93074d7..4cb01b5a60 100644
--- a/crates/perry-codegen/src/collectors/ptr_shape.rs
+++ b/crates/perry-codegen/src/collectors/ptr_shape.rs
@@ -414,6 +414,7 @@ pub(crate) fn collect_shape_proven_ptr_locals(
         field_stores: HashMap::new(),
         method_calls: HashMap::new(),
         new_args: HashMap::new(),
+        element_pushes: HashMap::new(),
         const_local_inits: HashMap::new(),
         disq_reasons: HashMap::new(),
         escape_ctx: report::ESC_BARE_REFERENCE,
@@ -429,10 +430,40 @@ pub(crate) fn collect_shape_proven_ptr_locals(
         field_stores,
         method_calls,
         new_args,
+        element_pushes,
         const_local_inits,
         disq_reasons,
         ..
     } = walk;
+    // #7770: locals whose every write is number-producing by construction —
+    // they let a provenance `new C(i, i + 1)` resolve its parameters.
+    let numeric_locals = collect_numeric_by_construction_locals(
+        stmts,
+        boxed_vars,
+        module_globals,
+        not_bigint_locals,
+        &const_local_inits,
+    );
+    // #7770: one numeric-field verdict per element group, computed from the
+    // union of every member's stores and the meet over every push's `new`
+    // arguments (see `ptr_shape_numeric.rs`). Consulted by the `'cand` loop
+    // in place of the per-member proof, which cannot see sibling stores. The
+    // claim is honest even though member verdicts are not in yet: group
+    // integrity below drops EVERY member's fact when any member fails, and a
+    // dropped fact takes its claim with it.
+    let group_numeric = prove_group_numeric_fields(
+        classes,
+        module_dispatch,
+        element_facts,
+        &roots,
+        &field_stores,
+        &method_calls,
+        &new_args,
+        &element_pushes,
+        not_bigint_locals,
+        &const_local_inits,
+        &numeric_locals,
+    );
     let mut out = HashMap::new();
     // `--opt-report`: one closure so every `continue` below has a matching
     // one-line recording. Behaviour is unchanged — `deny` is a no-op when
@@ -525,25 +556,31 @@ pub(crate) fn collect_shape_proven_ptr_locals(
         // shape proof by itself still retires the whole guard diamond; this
         // is the same stand-down `collectors/proven_this.rs` makes, for the
         // same reason.
-        let numeric_fields = if return_seeded.contains(id) || element_facts.is_group_member(*id) {
-            // #7034 §3: an element-group member's object is reachable through
-            // the array, so the numeric proof's exhaustive-reachable-store
-            // obligation cannot be discharged from this local's stores alone —
-            // a sibling member's `r.score = "s"` is a store this proof never
-            // sees. Same stand-down as the return-seeded case above.
+        let numeric_fields = if return_seeded.contains(id) {
             HashSet::new()
+        } else if let Some(group_root) = element_facts.member_group_root(*id) {
+            // #7034 §3 / #7770: an element-group member cannot discharge the
+            // exhaustive-reachable-store obligation from its own stores — a
+            // sibling's `r.score = "s"` is a store this proof never sees.
+            // The GROUP can: containment bounds every reference to the
+            // group's objects to its members and provenance `new`s, and
+            // `prove_group_numeric_fields` unions exactly those. Every
+            // member carries the group verdict or nothing.
+            group_numeric.get(&group_root).cloned().unwrap_or_default()
         } else {
+            let single_new_list: [&[Expr]; 1] = [new_args.get(id).copied().unwrap_or(&[])];
             prove_numeric_fields(
                 &chain,
                 &members,
                 &store_records,
                 field_stores.get(id).map(Vec::as_slice).unwrap_or(&[]),
-                new_args.get(id).copied().unwrap_or(&[]),
+                &single_new_list,
                 called,
                 &super_call_args,
                 &internally_invoked,
                 not_bigint_locals,
                 &const_local_inits,
+                &numeric_locals,
             )
         };
         let fact = PtrShapeLocal {
@@ -735,6 +772,7 @@ pub(super) fn chain_method_map<'a>(
 
 /// A recorded store into a candidate's field, with enough context to resolve
 /// parameter-mediated values later.
+#[derive(Clone, Copy)]
 enum StoreValue<'a> {
     /// Value expression in function scope (a direct `o.f = expr` store).
     Direct(&'a Expr),
@@ -744,6 +782,22 @@ enum StoreValue<'a> {
     Update,
 }
 
+/// #7770: one provenance record per push into an element-shape-proven array,
+/// feeding the group-wide numeric proof
+/// (`ptr_shape_numeric.rs::prove_group_numeric_fields`).
+enum ElementPush<'a> {
+    /// `A.push(new C(...))` — the inline argument list.
+    Inline(&'a [Expr]),
+    /// `A.push(v)` — a vetted producer local; its argument list is the one
+    /// `UseWalk::new_args` records at its `Let`.
+    Producer(u32),
+    /// A value shape E2 admits into no proven array. Unreachable while the
+    /// element walk and this walk see the same tree; recorded (rather than
+    /// skipped) so drift between them forfeits the group's numeric claim
+    /// instead of silently narrowing the provenance meet.
+    Opaque,
+}
+
 struct UseWalk<'a> {
     candidates: &'a HashMap<u32, String>,
     /// Tracked member id (candidate or const alias) -> root candidate id.
@@ -757,6 +811,8 @@ struct UseWalk<'a> {
     method_calls: HashMap<u32, HashMap<String, Vec<&'a [Expr]>>>,
     /// root candidate -> the provenance `new C(...)` argument list.
     new_args: HashMap<u32, &'a [Expr]>,
+    /// #7770: proven element-array root -> one [`ElementPush`] per push.
+    element_pushes: HashMap<u32, Vec<ElementPush<'a>>>,
     /// Non-tracked `const` locals' init expressions (single-Let only; a
     /// re-declared id is poisoned to `None`). Lets the numeric-field proof
     /// chase one level through `const v = i * 0.5`-style temps.
@@ -1189,6 +1245,22 @@ impl<'a> UseWalk<'a> {
             // Any other array, any other value shape, keeps today's escape.
             Expr::ArrayPush { array_id, value } => {
                 self.disq(*array_id, report::ESC_CONTAINER_MUTATOR);
+                // #7770: record the provenance argument list for the
+                // group-wide numeric proof. Only pushes into a PROVEN array
+                // are recorded — for any other array no group exists to
+                // consume them.
+                if let Some(root) = self.element_facts.proven_array_root(*array_id) {
+                    let push = match value.as_ref() {
+                        Expr::New { args, .. } => ElementPush::Inline(args.as_slice()),
+                        Expr::LocalGet(v)
+                            if self.element_facts.push_is_contained(*v, *array_id) =>
+                        {
+                            ElementPush::Producer(*v)
+                        }
+                        _ => ElementPush::Opaque,
+                    };
+                    self.element_pushes.entry(root).or_default().push(push);
+                }
                 if let Expr::LocalGet(v) = value.as_ref() {
                     if self.element_facts.push_is_contained(*v, *array_id) {
                         return;
@@ -1754,221 +1826,16 @@ fn expr_mentions_this(e: &Expr) -> bool {
     found
 }
 
-// ── Pass 4: numeric-proven fields ──────────────────────────────────────────
-
-/// Greatest-fixpoint proof that every reachable store into a raw-f64-declared
-/// chain field is number-producing. Parameter-mediated stores resolve through
-/// the actual argument expressions at the provenance `new` (constructor) or
-/// at every recorded call site (methods).
-/// Parameter environment for [`expr_numeric_by_construction`].
-enum ParamEnv<'x> {
-    /// Function scope: no parameters; const-local chasing applies.
-    None,
-    /// Method scope: params resolve through recorded call-site argument
-    /// lists (each argument evaluated in function scope).
-    Sites {
-        param_ids: &'x [u32],
-        sites: Vec<&'x [Expr]>,
-    },
-    /// Constructor scope: params pre-resolved to a numeric verdict through
-    /// the provenance `new` / `super(...)` argument chain.
-    Resolved(&'x HashMap<u32, bool>),
-}
-
-#[allow(clippy::too_many_arguments)]
-fn prove_numeric_fields(
-    chain: &[&Class],
-    members: &HashSet<u32>,
-    this_stores: &[ThisStoreRecord<'_>],
-    local_stores: &[(String, StoreValue<'_>)],
-    new_args: &[Expr],
-    method_calls: Option<&HashMap<String, Vec<&[Expr]>>>,
-    super_call_args: &HashMap<String, Vec<&[Expr]>>,
-    internally_invoked: &HashSet<String>,
-    not_bigint_locals: &HashSet<u32>,
-    const_local_inits: &HashMap<u32, Option<&Expr>>,
-) -> HashSet<String> {
-    let mut numeric: HashSet<String> = HashSet::new();
-    for class in chain {
-        for field in &class.fields {
-            if crate::typed_shape::type_is_raw_f64_candidate(&field.ty) {
-                numeric.insert(field.name.clone());
-            }
-        }
-    }
-    if numeric.is_empty() {
-        return numeric;
-    }
-    // Resolve the argument expressions that can flow into a given
-    // (context, param position): the provenance `new` args feed the root
-    // constructor; each parent constructor's params resolve through the
-    // recorded `super(...)` argument lists, evaluated under the CALLING
-    // constructor's (already-resolved) parameter environment. Derived-first
-    // chain order makes this a single top-down pass. The environment is
-    // computed against an EMPTY numeric-field set (strictly conservative —
-    // `super(this.x)` cannot occur, `this` is banned in super args).
-    let mut ctor_param_env: HashMap<String, HashMap<u32, bool>> = HashMap::new();
-    {
-        let empty_numeric: HashSet<String> = HashSet::new();
-        for (pos, class) in chain.iter().enumerate() {
-            let Some(ctor) = class.constructor.as_ref() else {
-                continue;
-            };
-            let mut env: HashMap<u32, bool> = HashMap::new();
-            if pos == 0 {
-                for (i, param) in ctor.params.iter().enumerate() {
-                    let ok = new_args
-                        .get(i)
-                        .map(|a| {
-                            expr_numeric_by_construction(
-                                a,
-                                &ParamEnv::None,
-                                members,
-                                &empty_numeric,
-                                not_bigint_locals,
-                                const_local_inits,
-                                0,
-                            )
-                        })
-                        .unwrap_or(false);
-                    env.insert(param.id, ok);
-                }
-            } else {
-                let caller_env = chain
-                    .get(pos - 1)
-                    .and_then(|caller| ctor_param_env.get(caller.name.as_str()));
-                let lists = super_call_args.get(class.name.as_str());
-                for (i, param) in ctor.params.iter().enumerate() {
-                    let ok = match (lists, caller_env) {
-                        (Some(lists), Some(caller_env)) if !lists.is_empty() => {
-                            lists.iter().all(|args| {
-                                args.get(i)
-                                    .map(|a| {
-                                        expr_numeric_by_construction(
-                                            a,
-                                            &ParamEnv::Resolved(caller_env),
-                                            members,
-                                            &empty_numeric,
-                                            not_bigint_locals,
-                                            const_local_inits,
-                                            0,
-                                        )
-                                    })
-                                    .unwrap_or(false)
-                            })
-                        }
-                        _ => false,
-                    };
-                    env.insert(param.id, ok);
-                }
-            }
-            ctor_param_env.insert(class.name.clone(), env);
-        }
-    }
-
-    loop {
-        let before = numeric.len();
-        let is_store_numeric = |field: &str,
-                                value: Option<&Expr>,
-                                context: Option<&(String, String, Vec<u32>)>,
-                                numeric: &HashSet<String>|
-         -> bool {
-            let _ = field;
-            let Some(value) = value else {
-                // `++`/`--` — ToNumeric of a proven-number field stays a
-                // number; if the field is currently claimed numeric the
-                // update preserves it.
-                return true;
-            };
-            let param_env: ParamEnv<'_> = match context {
-                None => ParamEnv::None,
-                Some((owner, name, param_ids)) => {
-                    if name == "constructor" {
-                        match ctor_param_env.get(owner.as_str()) {
-                            Some(env) => ParamEnv::Resolved(env),
-                            None => ParamEnv::Sites {
-                                param_ids: param_ids.as_slice(),
-                                sites: Vec::new(),
-                            },
-                        }
-                    } else {
-                        // A method that is ALSO invoked internally
-                        // (`this.m(...)` / `super.m(...)`) receives argument
-                        // expressions from method scope that the
-                        // function-scope site resolution below cannot see —
-                        // its parameters stay unproven even when every
-                        // external site is numeric (an internal
-                        // `this.m("s")` would otherwise poison a
-                        // "proven" field). Purely-external methods resolve
-                        // through their recorded call sites; purely-internal
-                        // ones have no sites and stay unproven either way.
-                        let sites: Vec<&[Expr]> = if internally_invoked.contains(name.as_str()) {
-                            Vec::new()
-                        } else {
-                            method_calls
-                                .and_then(|mc| mc.get(name))
-                                .map(|v| v.clone())
-                                .unwrap_or_default()
-                        };
-                        ParamEnv::Sites {
-                            param_ids: param_ids.as_slice(),
-                            sites,
-                        }
-                    }
-                }
-            };
-            expr_numeric_by_construction(
-                value,
-                &param_env,
-                members,
-                numeric,
-                not_bigint_locals,
-                const_local_inits,
-                0,
-            )
-        };
-        // Field initializers + ctor/method stores.
-        let mut retained: HashSet<String> = numeric.clone();
-        for rec in this_stores {
-            if retained.contains(&rec.field)
-                && !is_store_numeric(&rec.field, rec.value, rec.context.as_ref(), &numeric)
-            {
-                retained.remove(&rec.field);
-            }
-        }
-        for (field, sv) in local_stores {
-            if retained.contains(field) {
-                let ok = match sv {
-                    StoreValue::Update => true,
-                    StoreValue::Direct(v) => expr_numeric_by_construction(
-                        v,
-                        &ParamEnv::None,
-                        members,
-                        &numeric,
-                        not_bigint_locals,
-                        const_local_inits,
-                        0,
-                    ),
-                };
-                if !ok {
-                    retained.remove(field);
-                }
-            }
-        }
-        numeric = retained;
-        if numeric.len() == before || numeric.is_empty() {
-            break;
-        }
-    }
-    numeric
-}
-
-/// Number-by-construction proof for the numeric-field rule. Split out to
-/// stay under the 2000-line CI gate; still a child module, so `use super::*`
+/// Pass 4 — the numeric-field machinery: the number-by-construction expression
+/// proof, the per-candidate and per-element-group (#7770) reachable-store
+/// proofs, and the numeric-by-construction locals fixpoint. Split out to stay
+/// under the 2000-line CI gate; still a child module, so `use super::*`
 /// reaches the collector's private items.
 #[path = "ptr_shape_numeric.rs"]
 mod numeric;
-use numeric::expr_numeric_by_construction;
+use numeric::{
+    collect_numeric_by_construction_locals, prove_group_numeric_fields, prove_numeric_fields,
+};
 
 /// Conservative "cannot be a BigInt" for the spec Number-path argument.
 fn expr_provably_not_bigint(e: &Expr, not_bigint_locals: &HashSet<u32>) -> bool {
@@ -1998,3 +1865,8 @@ fn expr_provably_not_bigint(e: &Expr, not_bigint_locals: &HashSet<u32>) -> bool
 #[cfg(test)]
 #[path = "ptr_shape_opt_report_tests.rs"]
 mod opt_report_tests;
+
+/// #7770 group-wide numeric proof tests. Same sibling-file arrangement.
+#[cfg(test)]
+#[path = "ptr_shape_group_numeric_tests.rs"]
+mod group_numeric_tests;
diff --git a/crates/perry-codegen/src/collectors/ptr_shape_elements.rs b/crates/perry-codegen/src/collectors/ptr_shape_elements.rs
index 698c103f1f..e94e505dfa 100644
--- a/crates/perry-codegen/src/collectors/ptr_shape_elements.rs
+++ b/crates/perry-codegen/src/collectors/ptr_shape_elements.rs
@@ -86,18 +86,25 @@
 //! when any member fails, rather than dropping the member. See
 //! [`ElementShapeFacts::group_members`].
 //!
-//! ## `numeric_fields` is deliberately not claimed
+//! ## `numeric_fields` is claimed at GROUP scope (#7770)
 //!
-//! Phase 3b's numeric-field proof is an *exhaustive reachable store* proof,
-//! which containment makes possible because no alias exists. An element group
-//! has aliases by construction: a store through one member
-//! (`r.score = "s"` — a declared field, so rule 2 permits it) takes the
-//! store-side boxed-setter exit and downgrades that slot's raw-f64 layout,
-//! and another member's `load double` claiming `JsNumber` would then read
-//! NaN-boxed string bits as a number. Group members therefore claim no
-//! numeric fields at all — the same stand-down `proven_this.rs` and
-//! `ptr_shape_returns.rs` make, for the same reason. The shape proof by
-//! itself still retires the whole guard diamond.
+//! Phase 3b's numeric-field proof is an *exhaustive reachable store* proof.
+//! A single member cannot discharge it — a sibling's `r.score = "s"` (a
+//! declared field, so rule 2 permits it) takes the store-side boxed-setter
+//! exit and downgrades that slot's raw-f64 layout, and this member's
+//! `load double` claiming `JsNumber` would then read NaN-boxed string bits
+//! as a number. But the GROUP can: E1–E5 containment bounds every reference
+//! to the group's objects to the group's own members and the provenance
+//! `new`s at the push sites, so the union of the members' stores plus every
+//! push's constructor arguments IS the reachable-store set.
+//! `ptr_shape.rs` therefore computes one numeric-field set per array root
+//! (`ptr_shape_numeric.rs::prove_group_numeric_fields`) — the constructor
+//! parameter environment resolved as the meet over ALL provenance `new`
+//! argument lists — and every member carries that same set. Group integrity
+//! keeps the claim honest: a claim only survives if every member survives,
+//! because dropping any member drops them all. (`proven_this.rs` and
+//! `ptr_shape_returns.rs` still stand down entirely: their receivers are
+//! caller-aliased, so no bounded store universe exists to union over.)
 //!
 //! ## GC contract
 //!
@@ -191,10 +198,31 @@ impl ElementShapeFacts {
         out
     }
 
-    /// Locals whose object is reachable from an array, and which therefore
-    /// must not claim numeric fields (module doc).
+    /// Locals whose object is reachable from an array (either group half).
     pub(crate) fn is_group_member(&self, local: u32) -> bool {
-        self.pushed.contains_key(&local) || self.element_reads.contains_key(&local)
+        self.member_group_root(local).is_some()
+    }
+
+    /// The array root whose group `local` belongs to, if any. A member's
+    /// object is reachable through the array, so its numeric-field claim is
+    /// the GROUP's claim (module doc, #7770), never its own.
+    pub(crate) fn member_group_root(&self, local: u32) -> Option<u32> {
+        self.pushed
+            .get(&local)
+            .or_else(|| self.element_reads.get(&local))
+            .map(|(root, _)| *root)
+    }
+
+    /// The proven element class of array root `root`.
+    pub(crate) fn root_class(&self, root: u32) -> Option<&str> {
+        self.arrays.get(&root).map(String::as_str)
+    }
+
+    /// The proven root for an ARRAY local or alias id — `Some` only when the
+    /// array it references actually carries element-shape facts.
+    pub(crate) fn proven_array_root(&self, id: u32) -> Option<u32> {
+        let root = self.array_roots.get(&id)?;
+        self.arrays.contains_key(root).then_some(*root)
     }
 }
 
diff --git a/crates/perry-codegen/src/collectors/ptr_shape_elements_tests.rs b/crates/perry-codegen/src/collectors/ptr_shape_elements_tests.rs
index 06603aaa36..3458e16dd8 100644
--- a/crates/perry-codegen/src/collectors/ptr_shape_elements_tests.rs
+++ b/crates/perry-codegen/src/collectors/ptr_shape_elements_tests.rs
@@ -256,10 +256,15 @@ fn pushed_local_is_promoted() {
         .get(&2)
         .expect("a local whose only escape is a push into a proven array must promote");
     assert_eq!(fact.class_name, "C");
-    assert!(
-        fact.numeric_fields.is_empty(),
-        "an element-group member must never claim numeric fields: a sibling's \
-         store through the array is a reachable store this proof cannot see"
+    // #7770: the numeric claim is discharged at GROUP scope. This group's
+    // reachable stores are the (arg-less) provenance `new` and `o.x = 1`,
+    // both numeric, so the claim matches what the same class gets as a plain
+    // rule-1 candidate. The sibling-store direction has its own red tests in
+    // `ptr_shape_group_numeric` below.
+    assert_eq!(
+        fact.numeric_fields,
+        ["x", "y"].iter().map(|s| s.to_string()).collect(),
+        "a surviving group's members carry the group-wide numeric verdict"
     );
 }
 
@@ -497,9 +502,14 @@ fn bounded_element_read_is_provenance() {
         .get(&6)
         .expect("an in-bounds `a[i]` binding must be a Ptr<Shape> candidate");
     assert_eq!(fact.class_name, "C");
-    assert!(
-        fact.numeric_fields.is_empty(),
-        "an element read is aliased through the array by construction"
+    // #7770: the element read carries the GROUP's numeric verdict — here the
+    // only reachable stores are the arg-less provenance `new`'s (none), so
+    // both raw-f64-declared fields survive, exactly as they would on a plain
+    // rule-1 candidate of the same class.
+    assert_eq!(
+        fact.numeric_fields,
+        ["x", "y"].iter().map(|s| s.to_string()).collect(),
+        "a licensed `a[i]` binding carries the group-wide numeric verdict"
     );
 }
 
diff --git a/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs b/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs
new file mode 100644
index 0000000000..7bb11dd242
--- /dev/null
+++ b/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs
@@ -0,0 +1,703 @@
+//! #7770: the group-wide numeric-field proof and the numeric-by-construction
+//! locals that feed it.
+//!
+//! Every positive test fails against the pre-#7770 collector (element-group
+//! members stood down to zero numeric fields), and every negative test names
+//! the store channel whose poisoning must drop the claim — the direction the
+//! feature can be quietly wrong in, since a wrongly-claimed field's read is a
+//! bare raw `load double` with no value check.
+
+use super::*;
+use crate::collectors::PtrShapeLocal;
+use perry_hir::types::Type;
+use perry_hir::{BinaryOp, ClassField, CompareOp, Function, Module, Param, UpdateOp};
+
+// ── Fixture builders ───────────────────────────────────────────────────────
+
+/// Constructor parameter ids — deliberately far from the function-local ids
+/// the tests use, mirroring the module-wide id allocator.
+const CTOR_PX: u32 = 100;
+const CTOR_PY: u32 = 101;
+/// Method parameter id for `setX(v)`.
+const METH_PV: u32 = 110;
+
+fn field(name: &str) -> ClassField {
+    ClassField {
+        name: name.to_string(),
+        key_expr: None,
+        ty: Type::Number,
+        init: None,
+        is_private: false,
+        is_readonly: false,
+        decorators: Vec::new(),
+    }
+}
+
+fn num_param(id: u32, name: &str) -> Param {
+    Param {
+        id,
+        name: name.to_string(),
+        ty: Type::Number,
+        default: None,
+        decorators: Vec::new(),
+        is_rest: false,
+        arguments_object: None,
+    }
+}
+
+fn this_store(property: &str, value: Expr) -> Stmt {
+    Stmt::Expr(Expr::PropertySet {
+        object: Box::new(Expr::This),
+        property: property.to_string(),
+        value: Box::new(value),
+    })
+}
+
+/// `class P { x: number; y: number; constructor(x, y) { this.x = x; this.y = y; } }`
+fn class_p() -> Class {
+    Class {
+        id: 0,
+        name: "P".to_string(),
+        type_params: Vec::new(),
+        extends: None,
+        extends_name: None,
+        native_extends: None,
+        extends_expr: None,
+        heritage_lexically_shadowed: false,
+        fields: vec![field("x"), field("y")],
+        constructor: Some(Function {
+            id: 900,
+            name: "constructor".to_string(),
+            type_params: Vec::new(),
+            params: vec![num_param(CTOR_PX, "x"), num_param(CTOR_PY, "y")],
+            return_type: Type::Void,
+            body: vec![
+                this_store("x", Expr::LocalGet(CTOR_PX)),
+                this_store("y", Expr::LocalGet(CTOR_PY)),
+            ],
+            is_async: false,
+            is_generator: false,
+            is_strict: true,
+            is_exported: false,
+            captures: Vec::new(),
+            decorators: Vec::new(),
+            was_plain_async: false,
+            was_unrolled: false,
+        }),
+        methods: Vec::new(),
+        getters: Vec::new(),
+        setters: Vec::new(),
+        static_fields: Vec::new(),
+        static_methods: Vec::new(),
+        computed_members: Vec::new(),
+        decorators: Vec::new(),
+        is_exported: false,
+        aliases: Vec::new(),
+        is_nested: false,
+        alloc_width_hint: 0,
+        specialized_from: None,
+        static_accessor_names: Vec::new(),
+        static_accessor_fn_ids: Vec::new(),
+    }
+}
+
+/// `class Q` = `class P` plus `setX(v: number) { this.x = v; }`.
+fn class_q() -> Class {
+    let mut q = class_p();
+    q.name = "Q".to_string();
+    q.methods = vec![Function {
+        id: 901,
+        name: "setX".to_string(),
+        type_params: Vec::new(),
+        params: vec![num_param(METH_PV, "v")],
+        return_type: Type::Void,
+        body: vec![this_store("x", Expr::LocalGet(METH_PV))],
+        is_async: false,
+        is_generator: false,
+        is_strict: true,
+        is_exported: false,
+        captures: Vec::new(),
+        decorators: Vec::new(),
+        was_plain_async: false,
+        was_unrolled: false,
+    }];
+    q
+}
+
+fn new_of(class_name: &str, args: Vec<Expr>) -> Expr {
+    Expr::New {
+        class_name: class_name.to_string(),
+        args,
+        type_args: Vec::new(),
+        byte_offset: 0,
+        cap_args_appended: 0,
+    }
+}
+
+/// `const <id>: <C>[] = [];`
+fn let_arr(id: u32, class_name: &str) -> Stmt {
+    Stmt::Let {
+        id,
+        name: format!("a{id}"),
+        ty: Type::Array(Box::new(Type::Named(class_name.to_string()))),
+        mutable: false,
+        init: Some(Expr::Array(Vec::new())),
+    }
+}
+
+fn push(array_id: u32, value: Expr) -> Stmt {
+    Stmt::Expr(Expr::ArrayPush {
+        array_id,
+        value: Box::new(value),
+    })
+}
+
+/// `for (let <idx> = 0; <idx> < <bound>; <idx>++) { body }`
+fn counted_loop(idx: u32, bound: Expr, body: Vec<Stmt>) -> Stmt {
+    Stmt::For {
+        init: Some(Box::new(Stmt::Let {
+            id: idx,
+            name: format!("i{idx}"),
+            ty: Type::Number,
+            mutable: true,
+            init: Some(Expr::Number(0.0)),
+        })),
+        condition: Some(Expr::Compare {
+            op: CompareOp::Lt,
+            left: Box::new(Expr::LocalGet(idx)),
+            right: Box::new(bound),
+        }),
+        update: Some(Expr::Update {
+            id: idx,
+            op: UpdateOp::Increment,
+            prefix: false,
+        }),
+        body,
+    }
+}
+
+fn arr_len(arr: u32) -> Expr {
+    Expr::PropertyGet {
+        object: Box::new(Expr::LocalGet(arr)),
+        property: "length".to_string(),
+        byte_offset: 0,
+    }
+}
+
+/// `const <id> = <arr>[<idx>];` typed by the array's element class.
+fn let_elem(id: u32, arr: u32, idx: u32, class_name: &str) -> Stmt {
+    Stmt::Let {
+        id,
+        name: format!("r{id}"),
+        ty: Type::Named(class_name.to_string()),
+        mutable: false,
+        init: Some(Expr::IndexGet {
+            object: Box::new(Expr::LocalGet(arr)),
+            index: Box::new(Expr::LocalGet(idx)),
+        }),
+    }
+}
+
+fn read_field(id: u32, property: &str) -> Stmt {
+    Stmt::Expr(Expr::PropertyGet {
+        object: Box::new(Expr::LocalGet(id)),
+        property: property.to_string(),
+        byte_offset: 0,
+    })
+}
+
+fn store_field(id: u32, property: &str, value: Expr) -> Stmt {
+    Stmt::Expr(Expr::PropertySet {
+        object: Box::new(Expr::LocalGet(id)),
+        property: property.to_string(),
+        value: Box::new(value),
+    })
+}
+
+/// `i + 1` over the loop counter.
+fn counter_plus_one(idx: u32) -> Expr {
+    Expr::Binary {
+        op: BinaryOp::Add,
+        left: Box::new(Expr::LocalGet(idx)),
+        right: Box::new(Expr::Integer(1)),
+    }
+}
+
+fn classes_of<'a>(cs: &'a [Class]) -> HashMap<String, &'a Class> {
+    cs.iter().map(|c| (c.name.clone(), c)).collect()
+}
+
+fn facts_for(classes: &HashMap<String, &Class>) -> ModuleDispatchFacts {
+    let mut hir = Module::new("t");
+    let mut names: Vec<&String> = classes.keys().collect();
+    names.sort();
+    for n in names {
+        hir.classes.push(classes[n].clone());
+    }
+    super::super::collect_module_dispatch_facts(&hir)
+}
+
+/// The full Phase 3b verdict, element facts included — what codegen sees.
+fn promote(stmts: &[Stmt], classes: &HashMap<String, &Class>) -> HashMap<u32, PtrShapeLocal> {
+    let facts = facts_for(classes);
+    let els = super::super::ptr_shape_elements::collect_element_shape_facts(
+        stmts,
+        &HashSet::new(),
+        &HashMap::new(),
+        classes,
+        &facts,
+    );
+    collect_shape_proven_ptr_locals(
+        stmts,
+        &HashSet::new(),
+        &HashMap::new(),
+        classes,
+        &facts,
+        &HashSet::new(),
+        &els,
+    )
+}
+
+fn names(set: &[&str]) -> HashSet<String> {
+    set.iter().map(|s| s.to_string()).collect()
+}
+
+// ── The group proof, positive direction ────────────────────────────────────
+
+/// #7770's headline shape — the issue's reproducer: inline `new P(i, i + 1)`
+/// pushes under a counting loop, licensed `const r = a[i]` reads. The loop
+/// counter is numeric by construction, so the meet proves both fields.
+///
+/// Sabotage: gut `collect_numeric_by_construction_locals` (the counter arg
+/// stops resolving) or `prove_group_numeric_fields` (members stand down) and
+/// this fails.
+#[test]
+fn inline_push_loop_counter_args_prove_numeric_fields() {
+    let cs = [class_p()];
+    let classes = classes_of(&cs);
+    let stmts = vec![
+        let_arr(1, "P"),
+        counted_loop(
+            2,
+            Expr::Number(10.0),
+            vec![push(
+                1,
+                new_of("P", vec![Expr::LocalGet(2), counter_plus_one(2)]),
+            )],
+        ),
+        counted_loop(
+            5,
+            arr_len(1),
+            vec![let_elem(6, 1, 5, "P"), read_field(6, "x")],
+        ),
+    ];
+    let promoted = promote(&stmts, &classes);
+    let fact = promoted.get(&6).expect("the element read must promote");
+    assert_eq!(fact.class_name, "P");
+    assert_eq!(
+        fact.numeric_fields,
+        names(&["x", "y"]),
+        "loop-counter constructor args are numeric by construction"
+    );
+}
+
+/// A producer local with numeric args joins the meet and proves.
+#[test]
+fn producer_local_new_args_prove_numeric_fields() {
+    let cs = [class_p()];
+    let classes = classes_of(&cs);
+    let stmts = vec![
+        let_arr(1, "P"),
+        Stmt::Let {
+            id: 2,
+            name: "p".to_string(),
+            ty: Type::Named("P".to_string()),
+            mutable: false,
+            init: Some(new_of("P", vec![Expr::Number(1.0), Expr::Number(2.0)])),
+        },
+        push(1, Expr::LocalGet(2)),
+        store_field(2, "y", Expr::Number(3.5)),
+        counted_loop(
+            5,
+            arr_len(1),
+            vec![let_elem(6, 1, 5, "P"), read_field(6, "y")],
+        ),
+    ];
+    let promoted = promote(&stmts, &classes);
+    assert_eq!(
+        promoted.get(&2).expect("producer promotes").numeric_fields,
+        names(&["x", "y"])
+    );
+    assert_eq!(
+        promoted.get(&6).expect("reader promotes").numeric_fields,
+        names(&["x", "y"]),
+        "producer stores and args are part of the same group universe"
+    );
+}
+
+// ── The group proof, negative directions (one per store channel) ───────────
+
+/// A SIBLING member's string store drops the field for EVERY member — the
+/// exact hole the pre-#7770 stand-down existed to avoid.
+///
+/// Sabotage: key the proof on one member's `field_stores` instead of the
+/// group union and this fails.
+#[test]
+fn sibling_string_store_drops_the_field_group_wide() {
+    let cs = [class_p()];
+    let classes = classes_of(&cs);
+    let stmts = vec![
+        let_arr(1, "P"),
+        counted_loop(
+            2,
+            Expr::Number(3.0),
+            vec![push(
+                1,
+                new_of("P", vec![Expr::LocalGet(2), Expr::LocalGet(2)]),
+            )],
+        ),
+        // Loop A: a member that poisons `x`.
+        counted_loop(
+            5,
+            arr_len(1),
+            vec![
+                let_elem(6, 1, 5, "P"),
+                store_field(6, "x", Expr::String("s".to_string())),
+            ],
+        ),
+        // Loop B: a different member that only reads.
+        counted_loop(
+            8,
+            arr_len(1),
+            vec![let_elem(9, 1, 8, "P"), read_field(9, "x")],
+        ),
+    ];
+    let promoted = promote(&stmts, &classes);
+    for id in [6u32, 9u32] {
+        assert_eq!(
+            promoted
+                .get(&id)
+                .expect("members still promote")
+                .numeric_fields,
+            names(&["y"]),
+            "the poisoned field must drop for member {id}, the healthy one must stay"
+        );
+    }
+}
+
+/// The MEET over push sites: one non-numeric constructor argument at any
+/// site drops the parameter's field for the whole group.
+#[test]
+fn mixed_push_site_meet_drops_the_field() {
+    let cs = [class_p()];
+    let classes = classes_of(&cs);
+    let stmts = vec![
+        let_arr(1, "P"),
+        push(1, new_of("P", vec![Expr::Number(1.0), Expr::Number(2.0)])),
+        push(
+            1,
+            new_of("P", vec![Expr::String("s".to_string()), Expr::Number(3.0)]),
+        ),
+        counted_loop(
+            5,
+            arr_len(1),
+            vec![let_elem(6, 1, 5, "P"), read_field(6, "x")],
+        ),
+    ];
+    let promoted = promote(&stmts, &classes);
+    assert_eq!(
+        promoted.get(&6).expect("reader promotes").numeric_fields,
+        names(&["y"]),
+        "one string site must veto `x` for every member"
+    );
+}
+
+/// A producer local's `new` args join the same meet.
+#[test]
+fn producer_new_args_join_the_meet() {
+    let cs = [class_p()];
+    let classes = classes_of(&cs);
+    let stmts = vec![
+        let_arr(1, "P"),
+        Stmt::Let {
+            id: 2,
+            name: "p".to_string(),
+            ty: Type::Named("P".to_string()),
+            mutable: false,
+            init: Some(new_of(
+                "P",
+                vec![Expr::String("s".to_string()), Expr::Number(1.0)],
+            )),
+        },
+        push(1, Expr::LocalGet(2)),
+        counted_loop(
+            5,
+            arr_len(1),
+            vec![let_elem(6, 1, 5, "P"), read_field(6, "x")],
+        ),
+    ];
+    let promoted = promote(&stmts, &classes);
+    assert_eq!(
+        promoted.get(&6).expect("reader promotes").numeric_fields,
+        names(&["y"])
+    );
+}
+
+/// A method invoked on any member resolves its parameter through the merged
+/// group call sites: one string argument drops the stored-to field.
+#[test]
+fn method_site_string_arg_drops_the_field() {
+    let cs = [class_q()];
+    let classes = classes_of(&cs);
+    let call_set_x = |recv: u32, arg: Expr| {
+        Stmt::Expr(Expr::Call {
+            callee: Box::new(Expr::PropertyGet {
+                object: Box::new(Expr::LocalGet(recv)),
+                property: "setX".to_string(),
+                byte_offset: 0,
+            }),
+            args: vec![arg],
+            type_args: Vec::new(),
+            byte_offset: 0,
+        })
+    };
+    let stmts = vec![
+        let_arr(1, "Q"),
+        push(1, new_of("Q", vec![Expr::Number(1.0), Expr::Number(2.0)])),
+        counted_loop(
+            5,
+            arr_len(1),
+            vec![
+                let_elem(6, 1, 5, "Q"),
+                call_set_x(6, Expr::String("s".to_string())),
+            ],
+        ),
+        counted_loop(
+            8,
+            arr_len(1),
+            vec![let_elem(9, 1, 8, "Q"), read_field(9, "x")],
+        ),
+    ];
+    let promoted = promote(&stmts, &classes);
+    assert_eq!(
+        promoted.get(&9).expect("reader promotes").numeric_fields,
+        names(&["y"]),
+        "a method-mediated string store must drop `x` group-wide"
+    );
+    // The positive twin: a numeric argument keeps the claim.
+    let stmts_ok = vec![
+        let_arr(1, "Q"),
+        push(1, new_of("Q", vec![Expr::Number(1.0), Expr::Number(2.0)])),
+        counted_loop(
+            5,
+            arr_len(1),
+            vec![let_elem(6, 1, 5, "Q"), call_set_x(6, Expr::Number(7.0))],
+        ),
+    ];
+    let promoted_ok = promote(&stmts_ok, &classes);
+    assert_eq!(
+        promoted_ok.get(&6).expect("member promotes").numeric_fields,
+        names(&["x", "y"])
+    );
+}
+
+/// The group claim dies with the group: an undeclared-property store on one
+/// member removes every member's FACT, claim included.
+#[test]
+fn group_claim_dies_with_the_group() {
+    let cs = [class_p()];
+    let classes = classes_of(&cs);
+    let stmts = vec![
+        let_arr(1, "P"),
+        push(1, new_of("P", vec![Expr::Number(1.0), Expr::Number(2.0)])),
+        counted_loop(
+            5,
+            arr_len(1),
+            vec![
+                let_elem(6, 1, 5, "P"),
+                store_field(6, "extra", Expr::Number(1.0)),
+            ],
+        ),
+        counted_loop(
+            8,
+            arr_len(1),
+            vec![let_elem(9, 1, 8, "P"), read_field(9, "x")],
+        ),
+    ];
+    let promoted = promote(&stmts, &classes);
+    assert!(
+        !promoted.contains_key(&6) && !promoted.contains_key(&9),
+        "group integrity drops every member, so no claim can outlive a reshape"
+    );
+}
+
+// ── Numeric-by-construction locals ─────────────────────────────────────────
+
+fn numeric_locals_of(stmts: &[Stmt]) -> HashSet<u32> {
+    numeric::collect_numeric_by_construction_locals(
+        stmts,
+        &HashSet::new(),
+        &HashMap::new(),
+        &HashSet::new(),
+        &HashMap::new(),
+    )
+}
+
+/// The loop counter: `let i = 0` + `i++` and nothing else — the shape the
+/// provenance `new C(i, i + 1)` needs.
+#[test]
+fn loop_counter_is_numeric_by_construction() {
+    let stmts = vec![counted_loop(2, Expr::Number(10.0), Vec::new())];
+    assert!(numeric_locals_of(&stmts).contains(&2));
+}
+
+/// A self-referencing accumulator converges on the optimistic assumption.
+#[test]
+fn numeric_accumulator_is_numeric_by_construction() {
+    let stmts = vec![
+        Stmt::Let {
+            id: 3,
+            name: "acc".to_string(),
+            ty: Type::Number,
+            mutable: true,
+            init: Some(Expr::Number(0.0)),
+        },
+        Stmt::Expr(Expr::LocalSet(
+            3,
+            Box::new(Expr::Binary {
+                op: BinaryOp::Add,
+                left: Box::new(Expr::LocalGet(3)),
+                right: Box::new(Expr::Number(1.0)),
+            }),
+        )),
+    ];
+    assert!(numeric_locals_of(&stmts).contains(&3));
+}
+
+/// The poisons, one per rule: a no-init `Let` (undefined until assigned), a
+/// string write anywhere, a boxed id, and a param-like id with no `Let`.
+#[test]
+fn non_numeric_writes_and_bindings_are_excluded() {
+    let no_init = vec![
+        Stmt::Let {
+            id: 4,
+            name: "u".to_string(),
+            ty: Type::Number,
+            mutable: true,
+            init: None,
+        },
+        Stmt::Expr(Expr::LocalSet(4, Box::new(Expr::Number(1.0)))),
+    ];
+    assert!(
+        !numeric_locals_of(&no_init).contains(&4),
+        "a no-init Let is `undefined` until assigned"
+    );
+
+    let string_write = vec![
+        Stmt::Let {
+            id: 5,
+            name: "s".to_string(),
+            ty: Type::Number,
+            mutable: true,
+            init: Some(Expr::Number(0.0)),
+        },
+        Stmt::Expr(Expr::LocalSet(5, Box::new(Expr::String("x".to_string())))),
+    ];
+    assert!(!numeric_locals_of(&string_write).contains(&5));
+
+    // A closure-body write is still a write against the enclosing id.
+    let closure_write = vec![
+        Stmt::Let {
+            id: 6,
+            name: "c".to_string(),
+            ty: Type::Number,
+            mutable: true,
+            init: Some(Expr::Number(0.0)),
+        },
+        Stmt::Expr(Expr::Closure {
+            func_id: 99,
+            params: Vec::new(),
+            return_type: Type::Any,
+            body: vec![Stmt::Expr(Expr::LocalSet(
+                6,
+                Box::new(Expr::String("x".to_string())),
+            ))],
+            captures: Vec::new(),
+            mutable_captures: vec![6],
+            captures_this: false,
+            captures_new_target: false,
+            enclosing_class: None,
+            is_arrow: true,
+            is_async: false,
+            is_generator: false,
+            is_strict: false,
+        }),
+    ];
+    assert!(
+        !numeric_locals_of(&closure_write).contains(&6),
+        "closure-body writes must be part of the write set"
+    );
+
+    let boxed: HashSet<u32> = [7u32].into_iter().collect();
+    let boxed_local = vec![Stmt::Let {
+        id: 7,
+        name: "b".to_string(),
+        ty: Type::Number,
+        mutable: true,
+        init: Some(Expr::Number(0.0)),
+    }];
+    assert!(
+        !numeric::collect_numeric_by_construction_locals(
+            &boxed_local,
+            &boxed,
+            &HashMap::new(),
+            &HashSet::new(),
+            &HashMap::new(),
+        )
+        .contains(&7),
+        "a boxed local's write set is not this region's to enumerate"
+    );
+
+    // No `Let` at all (a parameter or catch binding shape): never a candidate.
+    let set_only = vec![Stmt::Expr(Expr::LocalSet(8, Box::new(Expr::Number(1.0))))];
+    assert!(!numeric_locals_of(&set_only).contains(&8));
+}
+
+/// `i++` as a VALUE is `ToNumeric(old)`, numeric exactly when the operand is
+/// provably not a BigInt.
+#[test]
+fn update_value_resolves_via_not_bigint() {
+    let store_update_arg = |target: u32| {
+        vec![Stmt::Let {
+            id: target,
+            name: "j".to_string(),
+            ty: Type::Number,
+            mutable: true,
+            init: Some(Expr::Update {
+                id: 20,
+                op: UpdateOp::Increment,
+                prefix: false,
+            }),
+        }]
+    };
+    let not_bigint: HashSet<u32> = [20u32].into_iter().collect();
+    let with_fact = numeric::collect_numeric_by_construction_locals(
+        &store_update_arg(21),
+        &HashSet::new(),
+        &HashMap::new(),
+        &not_bigint,
+        &HashMap::new(),
+    );
+    assert!(with_fact.contains(&21));
+    let without_fact = numeric::collect_numeric_by_construction_locals(
+        &store_update_arg(22),
+        &HashSet::new(),
+        &HashMap::new(),
+        &HashSet::new(),
+        &HashMap::new(),
+    );
+    assert!(
+        !without_fact.contains(&22),
+        "without the not-BigInt fact the update's value is unproven"
+    );
+}
diff --git a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs
index b11ab10c61..69b33bba18 100644
--- a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs
+++ b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs
@@ -1,14 +1,608 @@
-//! Number-by-construction proof for `collectors/ptr_shape.rs`'s numeric-field
-//! rule: does this expression evaluate to a JS Number for every input, per
-//! spec, never a string / BigInt / bool / undefined / pointer?
+//! Pass 4 of `collectors/ptr_shape.rs`: the numeric-field machinery.
+//!
+//! Four pieces, one contract. A field in `numeric_fields` licenses a bare
+//! `load double` that claims `JsNumber`/`F64` with **no coercion and no
+//! value check**, so everything here answers the same question — "is every
+//! reachable store into this slot number-producing by construction, per
+//! spec?" — never "does the declared type say number" (Perry does not
+//! enforce annotations).
+//!
+//! * [`expr_numeric_by_construction`] — the expression-level proof.
+//! * [`prove_numeric_fields`] — the per-receiver reachable-store fixpoint
+//!   (constructor chain, field initializers, method stores, in-function
+//!   stores), with constructor/method parameters resolved through the actual
+//!   argument expressions at the provenance `new`(s) / recorded call sites.
+//! * [`prove_group_numeric_fields`] (#7770) — the same proof discharged once
+//!   per element-shape-proven ARRAY: E1–E5 containment
+//!   (`collectors/ptr_shape_elements.rs`) bounds every reference to the
+//!   group's objects to the group's members and the provenance `new`s at the
+//!   push sites, so the union of their stores is exhaustive and the meet
+//!   over every push's constructor arguments resolves the parameter
+//!   environment.
+//! * [`collect_numeric_by_construction_locals`] (#7770) — locals whose every
+//!   write is number-producing (loop counters above all: `let i = 0` + `i++`),
+//!   so a provenance `new C(i, i + 1)` resolves. Same optimistic-fixpoint
+//!   shape as `collect_not_bigint_locals`, WITHOUT its declared-type leaf:
+//!   declared types stay untrusted here.
 //!
 //! Split out of `ptr_shape.rs` to stay under the 2000-line CI gate; declared
 //! there with `#[path]` so it remains a child module and can reach the
 //! collector's private items through `use super::*`.
 
 use super::*;
+
+// ── Parameter environments ─────────────────────────────────────────────────
+
+/// Parameter environment for [`expr_numeric_by_construction`].
+pub(super) enum ParamEnv<'x> {
+    /// Function scope: no parameters; const-local chasing applies.
+    None,
+    /// Method scope: params resolve through recorded call-site argument
+    /// lists (each argument evaluated in function scope).
+    Sites {
+        param_ids: &'x [u32],
+        sites: Vec<&'x [Expr]>,
+    },
+    /// Constructor scope: params pre-resolved to a numeric verdict through
+    /// the provenance `new` / `super(...)` argument chain.
+    Resolved(&'x HashMap<u32, bool>),
+}
+
+// ── The per-receiver reachable-store fixpoint ──────────────────────────────
+
+/// Greatest-fixpoint proof that every reachable store into a raw-f64-declared
+/// chain field is number-producing. Parameter-mediated stores resolve through
+/// the actual argument expressions at the provenance `new`(s) (constructor)
+/// or at every recorded call site (methods).
+///
+/// `new_arg_lists` carries ONE argument list per provenance `new`. A single
+/// rule-1 candidate has exactly one; an element group (#7770) has one per
+/// push site, and a constructor parameter is numeric only when EVERY list
+/// proves it — the meet. An empty slice means the provenance is unresolved
+/// and every parameter stays unproven.
+#[allow(clippy::too_many_arguments)]
+pub(super) fn prove_numeric_fields(
+    chain: &[&Class],
+    members: &HashSet<u32>,
+    this_stores: &[ThisStoreRecord<'_>],
+    local_stores: &[(String, StoreValue<'_>)],
+    new_arg_lists: &[&[Expr]],
+    method_calls: Option<&HashMap<String, Vec<&[Expr]>>>,
+    super_call_args: &HashMap<String, Vec<&[Expr]>>,
+    internally_invoked: &HashSet<String>,
+    not_bigint_locals: &HashSet<u32>,
+    const_local_inits: &HashMap<u32, Option<&Expr>>,
+    numeric_locals: &HashSet<u32>,
+) -> HashSet<String> {
+    let mut numeric: HashSet<String> = HashSet::new();
+    for class in chain {
+        for field in &class.fields {
+            if crate::typed_shape::type_is_raw_f64_candidate(&field.ty) {
+                numeric.insert(field.name.clone());
+            }
+        }
+    }
+    if numeric.is_empty() {
+        return numeric;
+    }
+    // Resolve the argument expressions that can flow into a given
+    // (context, param position): the provenance `new` args feed the root
+    // constructor; each parent constructor's params resolve through the
+    // recorded `super(...)` argument lists, evaluated under the CALLING
+    // constructor's (already-resolved) parameter environment. Derived-first
+    // chain order makes this a single top-down pass. The environment is
+    // computed against an EMPTY numeric-field set (strictly conservative —
+    // `super(this.x)` cannot occur, `this` is banned in super args).
+    let mut ctor_param_env: HashMap<String, HashMap<u32, bool>> = HashMap::new();
+    {
+        let empty_numeric: HashSet<String> = HashSet::new();
+        for (pos, class) in chain.iter().enumerate() {
+            let Some(ctor) = class.constructor.as_ref() else {
+                continue;
+            };
+            let mut env: HashMap<u32, bool> = HashMap::new();
+            if pos == 0 {
+                for (i, param) in ctor.params.iter().enumerate() {
+                    // Meet over every provenance `new`: a missing argument is
+                    // `undefined`, so it fails; no lists at all proves
+                    // nothing.
+                    let ok = !new_arg_lists.is_empty()
+                        && new_arg_lists.iter().all(|new_args| {
+                            new_args
+                                .get(i)
+                                .map(|a| {
+                                    expr_numeric_by_construction(
+                                        a,
+                                        &ParamEnv::None,
+                                        members,
+                                        &empty_numeric,
+                                        not_bigint_locals,
+                                        const_local_inits,
+                                        numeric_locals,
+                                        0,
+                                    )
+                                })
+                                .unwrap_or(false)
+                        });
+                    env.insert(param.id, ok);
+                }
+            } else {
+                let caller_env = chain
+                    .get(pos - 1)
+                    .and_then(|caller| ctor_param_env.get(caller.name.as_str()));
+                let lists = super_call_args.get(class.name.as_str());
+                for (i, param) in ctor.params.iter().enumerate() {
+                    let ok = match (lists, caller_env) {
+                        (Some(lists), Some(caller_env)) if !lists.is_empty() => {
+                            lists.iter().all(|args| {
+                                args.get(i)
+                                    .map(|a| {
+                                        expr_numeric_by_construction(
+                                            a,
+                                            &ParamEnv::Resolved(caller_env),
+                                            members,
+                                            &empty_numeric,
+                                            not_bigint_locals,
+                                            const_local_inits,
+                                            numeric_locals,
+                                            0,
+                                        )
+                                    })
+                                    .unwrap_or(false)
+                            })
+                        }
+                        _ => false,
+                    };
+                    env.insert(param.id, ok);
+                }
+            }
+            ctor_param_env.insert(class.name.clone(), env);
+        }
+    }
+
+    loop {
+        let before = numeric.len();
+        let is_store_numeric = |field: &str,
+                                value: Option<&Expr>,
+                                context: Option<&(String, String, Vec<u32>)>,
+                                numeric: &HashSet<String>|
+         -> bool {
+            let _ = field;
+            let Some(value) = value else {
+                // `++`/`--` — ToNumeric of a proven-number field stays a
+                // number; if the field is currently claimed numeric the
+                // update preserves it.
+                return true;
+            };
+            let param_env: ParamEnv<'_> = match context {
+                None => ParamEnv::None,
+                Some((owner, name, param_ids)) => {
+                    if name == "constructor" {
+                        match ctor_param_env.get(owner.as_str()) {
+                            Some(env) => ParamEnv::Resolved(env),
+                            None => ParamEnv::Sites {
+                                param_ids: param_ids.as_slice(),
+                                sites: Vec::new(),
+                            },
+                        }
+                    } else {
+                        // A method that is ALSO invoked internally
+                        // (`this.m(...)` / `super.m(...)`) receives argument
+                        // expressions from method scope that the
+                        // function-scope site resolution below cannot see —
+                        // its parameters stay unproven even when every
+                        // external site is numeric (an internal
+                        // `this.m("s")` would otherwise poison a
+                        // "proven" field). Purely-external methods resolve
+                        // through their recorded call sites; purely-internal
+                        // ones have no sites and stay unproven either way.
+                        let sites: Vec<&[Expr]> = if internally_invoked.contains(name.as_str()) {
+                            Vec::new()
+                        } else {
+                            method_calls
+                                .and_then(|mc| mc.get(name))
+                                .map(|v| v.clone())
+                                .unwrap_or_default()
+                        };
+                        ParamEnv::Sites {
+                            param_ids: param_ids.as_slice(),
+                            sites,
+                        }
+                    }
+                }
+            };
+            expr_numeric_by_construction(
+                value,
+                &param_env,
+                members,
+                numeric,
+                not_bigint_locals,
+                const_local_inits,
+                numeric_locals,
+                0,
+            )
+        };
+        // Field initializers + ctor/method stores.
+        let mut retained: HashSet<String> = numeric.clone();
+        for rec in this_stores {
+            if retained.contains(&rec.field)
+                && !is_store_numeric(&rec.field, rec.value, rec.context.as_ref(), &numeric)
+            {
+                retained.remove(&rec.field);
+            }
+        }
+        for (field, sv) in local_stores {
+            if retained.contains(field) {
+                let ok = match sv {
+                    StoreValue::Update => true,
+                    StoreValue::Direct(v) => expr_numeric_by_construction(
+                        v,
+                        &ParamEnv::None,
+                        members,
+                        &numeric,
+                        not_bigint_locals,
+                        const_local_inits,
+                        numeric_locals,
+                        0,
+                    ),
+                };
+                if !ok {
+                    retained.remove(field);
+                }
+            }
+        }
+        numeric = retained;
+        if numeric.len() == before || numeric.is_empty() {
+            break;
+        }
+    }
+    numeric
+}
+
+// ── #7770: the per-element-group proof ─────────────────────────────────────
+
+/// Discharge the reachable-store proof once per element-shape-proven array.
+///
+/// Soundness rests on the same containment that makes the SHAPE proof valid
+/// (`collectors/ptr_shape_elements.rs`, E1–E5): while the facts hold, every
+/// reference to a group's objects is a vetted producer local, a licensed
+/// element-read local, or the inline `new C(...)` at a push site — an
+/// unlicensed element read disqualifies the array, and `A[i].f = v` goes
+/// through an unlicensed `IndexGet`, so neither can coexist with the facts.
+/// The reachable-store set is therefore exactly:
+///
+/// * the constructor chain + field initializers, with the parameter
+///   environment resolved as the MEET over every push's `new` argument list;
+/// * every member's in-function field stores;
+/// * every method invoked on any member, with call sites merged group-wide.
+///
+/// The result is keyed by array root; every member of a surviving group
+/// carries the same set. Claims stay honest through group integrity: any
+/// member failing rule 2 drops every member's fact, claim included. Returns
+/// no entry (never a partial one) whenever any obligation fails — the
+/// members then simply claim nothing, exactly the pre-#7770 stand-down.
+#[allow(clippy::too_many_arguments)]
+pub(super) fn prove_group_numeric_fields<'a>(
+    classes: &HashMap<String, &'a Class>,
+    module_dispatch: &ModuleDispatchFacts,
+    element_facts: &ElementShapeFacts,
+    roots: &HashMap<u32, u32>,
+    field_stores: &HashMap<u32, Vec<(String, StoreValue<'a>)>>,
+    method_calls: &HashMap<u32, HashMap<String, Vec<&'a [Expr]>>>,
+    new_args: &HashMap<u32, &'a [Expr]>,
+    element_pushes: &HashMap<u32, Vec<ElementPush<'a>>>,
+    not_bigint_locals: &HashSet<u32>,
+    const_local_inits: &HashMap<u32, Option<&'a Expr>>,
+    numeric_locals: &HashSet<u32>,
+) -> HashMap<u32, HashSet<String>> {
+    let mut out: HashMap<u32, HashSet<String>> = HashMap::new();
+    'group: for (root, members) in element_facts.group_members() {
+        let Some(class_name) = element_facts.root_class(root) else {
+            continue;
+        };
+        let chain = chain_classes(classes, class_name);
+        if chain.is_empty() {
+            continue;
+        }
+        let fields = chain_field_names(&chain);
+        let methods = chain_method_map(&chain);
+        // Merge method call sites group-wide: a method's parameter is numeric
+        // only when every site on every member passes a numeric argument.
+        let mut merged_calls: HashMap<String, Vec<&'a [Expr]>> = HashMap::new();
+        for m in &members {
+            if let Some(mc) = method_calls.get(m) {
+                for (name, sites) in mc {
+                    merged_calls
+                        .entry(name.clone())
+                        .or_default()
+                        .extend_from_slice(sites);
+                }
+            }
+        }
+        // The same obligations the `'cand` loop imposes before it trusts a
+        // method walk, re-checked here so a claim can never rest on a weaker
+        // basis than the per-candidate proof it extends.
+        if !merged_calls.is_empty() && !module_dispatch.prototype_is_stable(classes, class_name) {
+            continue;
+        }
+        let mut analysis = ThisFlowAnalysis {
+            chain: &chain,
+            fields: &fields,
+            methods: &methods,
+            visited: HashSet::new(),
+            store_records: Vec::new(),
+            super_call_args: HashMap::new(),
+            internally_invoked: HashSet::new(),
+            allow_this_in_store_values: false,
+        };
+        if !analysis.ctor_chain_safe() {
+            continue;
+        }
+        for name in merged_calls.keys() {
+            if fields.contains(name.as_str()) {
+                continue 'group;
+            }
+            let Some((owner, func)) = methods.get(name.as_str()) else {
+                continue 'group;
+            };
+            if !analysis.method_safe(owner, func) {
+                continue 'group;
+            }
+        }
+        // One argument list per push — ALL of them, or no claim. A producer
+        // whose `new_args` went unrecorded, or a push shape E2 would never
+        // have admitted, forfeits the group's claim rather than narrowing
+        // the meet.
+        let mut new_lists: Vec<&'a [Expr]> = Vec::new();
+        for push in element_pushes.get(&root).map(Vec::as_slice).unwrap_or(&[]) {
+            match push {
+                ElementPush::Inline(args) => new_lists.push(args),
+                ElementPush::Producer(v) => match new_args.get(v) {
+                    Some(args) => new_lists.push(args),
+                    None => continue 'group,
+                },
+                ElementPush::Opaque => continue 'group,
+            }
+        }
+        if new_lists.is_empty() {
+            continue;
+        }
+        // The fixpoint's member set: every group member plus every alias of
+        // one — `r2.x` read as a store value proves through the same set.
+        let member_set: HashSet<u32> = members
+            .iter()
+            .copied()
+            .chain(
+                roots
+                    .iter()
+                    .filter(|(_, r)| members.contains(r))
+                    .map(|(m, _)| *m),
+            )
+            .collect();
+        let mut merged_stores: Vec<(String, StoreValue<'a>)> = Vec::new();
+        for m in &members {
+            if let Some(fs) = field_stores.get(m) {
+                merged_stores.extend(fs.iter().cloned());
+            }
+        }
+        let store_records = std::mem::take(&mut analysis.store_records);
+        let super_call_args = std::mem::take(&mut analysis.super_call_args);
+        let internally_invoked = std::mem::take(&mut analysis.internally_invoked);
+        let numeric = prove_numeric_fields(
+            &chain,
+            &member_set,
+            &store_records,
+            &merged_stores,
+            &new_lists,
+            Some(&merged_calls),
+            &super_call_args,
+            &internally_invoked,
+            not_bigint_locals,
+            const_local_inits,
+            numeric_locals,
+        );
+        if !numeric.is_empty() {
+            out.insert(root, numeric);
+        }
+    }
+    out
+}
+
+// ── #7770: numeric-by-construction locals ──────────────────────────────────
+
+/// Locals whose every write is number-producing by construction — above all
+/// the loop counter (`let i = 0` + `i++`) that feeds a provenance
+/// `new C(i, i + 1)`.
+///
+/// Candidates are ids bound by at least one `Stmt::Let` in the region —
+/// params and `catch` bindings have no `Let`, which is what keeps
+/// caller-controlled values out. Boxed and module-global ids are excluded:
+/// their write sets are not this region's to enumerate. A `Let` with no
+/// initializer poisons (the binding is `undefined` until assigned — the same
+/// verdict `Expr::Undefined` gets as a store value). `Update` (`++`/`--`)
+/// needs no record: ToNumeric of a value every checked write proved to be a
+/// Number is that number.
+///
+/// Optimistic greatest fixpoint, converging downward exactly like
+/// `collect_not_bigint_locals`: a self-referencing write (`s = s + x`)
+/// short-circuits on the running assumption, and a TDZ self-reference
+/// (`let x = x`) is vacuously sound — the read throws, so no value is ever
+/// stored or observed.
+pub(super) fn collect_numeric_by_construction_locals<'a>(
+    stmts: &'a [Stmt],
+    boxed_vars: &HashSet<u32>,
+    module_globals: &HashMap<u32, String>,
+    not_bigint_locals: &HashSet<u32>,
+    const_local_inits: &HashMap<u32, Option<&'a Expr>>,
+) -> HashSet<u32> {
+    let mut scan = WriteScan {
+        writes: HashMap::new(),
+        let_bound: HashSet::new(),
+    };
+    scan.walk_stmts(stmts);
+    let WriteScan { writes, let_bound } = scan;
+    let empty_members: HashSet<u32> = HashSet::new();
+    let empty_fields: HashSet<String> = HashSet::new();
+    let mut numeric: HashSet<u32> = let_bound
+        .into_iter()
+        .filter(|id| !boxed_vars.contains(id) && !module_globals.contains_key(id))
+        .collect();
+    loop {
+        let mut drop: Vec<u32> = Vec::new();
+        for &id in &numeric {
+            let ok = writes
+                .get(&id)
+                .map(|ws| {
+                    ws.iter().all(|w| match w {
+                        None => false,
+                        Some(e) => expr_numeric_by_construction(
+                            e,
+                            &ParamEnv::None,
+                            &empty_members,
+                            &empty_fields,
+                            not_bigint_locals,
+                            const_local_inits,
+                            &numeric,
+                            0,
+                        ),
+                    })
+                })
+                // A `let_bound` id always has its `Let` recorded; treat a
+                // missing entry as unproven rather than as vacuously true.
+                .unwrap_or(false);
+            if !ok {
+                drop.push(id);
+            }
+        }
+        if drop.is_empty() {
+            break;
+        }
+        for id in drop {
+            numeric.remove(&id);
+        }
+    }
+    numeric
+}
+
+/// Write collector for [`collect_numeric_by_construction_locals`]. Descends
+/// into closure bodies — ids are unique per lowering context, so a closure's
+/// write to an enclosing local records against the right id.
+struct WriteScan<'a> {
+    /// id -> every write's RHS; `None` = a `Let` with no initializer.
+    writes: HashMap<u32, Vec<Option<&'a Expr>>>,
+    /// ids bound by at least one `Stmt::Let` in the region.
+    let_bound: HashSet<u32>,
+}
+
+impl<'a> WriteScan<'a> {
+    fn walk_stmts(&mut self, stmts: &'a [Stmt]) {
+        for s in stmts {
+            self.walk_stmt(s);
+        }
+    }
+
+    fn walk_stmt(&mut self, s: &'a Stmt) {
+        match s {
+            Stmt::Let { id, init, .. } => {
+                self.let_bound.insert(*id);
+                self.writes.entry(*id).or_default().push(init.as_ref());
+                if let Some(e) = init {
+                    self.walk_expr(e);
+                }
+            }
+            Stmt::Expr(e) | Stmt::Throw(e) => self.walk_expr(e),
+            Stmt::Return(opt) => {
+                if let Some(e) = opt {
+                    self.walk_expr(e);
+                }
+            }
+            Stmt::If {
+                condition,
+                then_branch,
+                else_branch,
+            } => {
+                self.walk_expr(condition);
+                self.walk_stmts(then_branch);
+                if let Some(eb) = else_branch {
+                    self.walk_stmts(eb);
+                }
+            }
+            Stmt::While { condition, body } | Stmt::DoWhile { body, condition } => {
+                self.walk_expr(condition);
+                self.walk_stmts(body);
+            }
+            Stmt::For {
+                init,
+                condition,
+                update,
+                body,
+            } => {
+                if let Some(i) = init {
+                    self.walk_stmt(i.as_ref());
+                }
+                if let Some(c) = condition {
+                    self.walk_expr(c);
+                }
+                if let Some(u) = update {
+                    self.walk_expr(u);
+                }
+                self.walk_stmts(body);
+            }
+            Stmt::Try {
+                body,
+                catch,
+                finally,
+            } => {
+                self.walk_stmts(body);
+                if let Some(c) = catch {
+                    self.walk_stmts(&c.body);
+                }
+                if let Some(f) = finally {
+                    self.walk_stmts(f);
+                }
+            }
+            Stmt::Switch {
+                discriminant,
+                cases,
+            } => {
+                self.walk_expr(discriminant);
+                for case in cases {
+                    if let Some(t) = &case.test {
+                        self.walk_expr(t);
+                    }
+                    self.walk_stmts(&case.body);
+                }
+            }
+            Stmt::Labeled { body, .. } => self.walk_stmt(body.as_ref()),
+            Stmt::Break
+            | Stmt::Continue
+            | Stmt::LabeledBreak(_)
+            | Stmt::LabeledContinue(_)
+            | Stmt::PreallocateBoxes(_)
+            | Stmt::PreallocateTdzBoxes(_) => {}
+        }
+    }
+
+    fn walk_expr(&mut self, e: &'a Expr) {
+        match e {
+            Expr::LocalSet(id, rhs) => {
+                self.writes.entry(*id).or_default().push(Some(rhs));
+                self.walk_expr(rhs);
+            }
+            // Closure bodies are `Vec<Stmt>`, invisible to the child walker.
+            Expr::Closure { body, .. } => self.walk_stmts(body),
+            _ => {
+                perry_hir::walker::walk_expr_children(e, &mut |c| self.walk_expr(c));
+            }
+        }
+    }
+}
+
+// ── The expression-level proof ─────────────────────────────────────────────
+
 /// Number-by-construction: the expression's runtime value is a JS Number for
 /// every input, per spec — never a string/BigInt/bool/undefined/pointer.
+#[allow(clippy::too_many_arguments)]
 pub(super) fn expr_numeric_by_construction(
     e: &Expr,
     param_env: &ParamEnv<'_>,
@@ -16,6 +610,7 @@ pub(super) fn expr_numeric_by_construction(
     numeric_fields: &HashSet<String>,
     not_bigint_locals: &HashSet<u32>,
     const_local_inits: &HashMap<u32, Option<&Expr>>,
+    numeric_locals: &HashSet<u32>,
     depth: usize,
 ) -> bool {
     if depth > 16 {
@@ -30,6 +625,7 @@ pub(super) fn expr_numeric_by_construction(
             numeric_fields,
             not_bigint_locals,
             const_local_inits,
+            numeric_locals,
             depth + 1,
         )
     };
@@ -44,8 +640,6 @@ pub(super) fn expr_numeric_by_construction(
         Expr::Binary { op, left, right } => match op {
             // `+` concatenates strings; both sides must be numbers.
             BinaryOp::Add => rec(left) && rec(right),
-            // `- * / %` produce BigInt only for BigInt⊗BigInt; a provably
-            // non-BigInt operand forces the Number path.
             // `- * / %` produce a BigInt only for BigInt⊗BigInt; mixing a
             // BigInt with anything else THROWS (no value is stored). ONE
             // provably-non-BigInt operand therefore forces the completed
@@ -107,6 +701,11 @@ pub(super) fn expr_numeric_by_construction(
             ..
         } => rec(then_expr) && rec(else_expr),
         Expr::Sequence(es) => es.last().map(|x| rec(x)).unwrap_or(false),
+        // `i++` / `--i` as a VALUE: `ToNumeric(old)` (± the adjustment),
+        // which is a Number unless `old` is a BigInt — exactly the
+        // not-BigInt fact. (The WRITE side is judged by
+        // `collect_numeric_by_construction_locals`, not here.)
+        Expr::Update { id, .. } => not_bigint_locals.contains(id),
         // A parameter: numeric iff every recorded call site passes a numeric
         // argument at that position (missing argument = `undefined`, not
         // numeric). No recorded sites = unproven.
@@ -124,6 +723,7 @@ pub(super) fn expr_numeric_by_construction(
                                         numeric_fields,
                                         not_bigint_locals,
                                         const_local_inits,
+                                        numeric_locals,
                                         depth + 1,
                                     )
                                 }) == Some(true)
@@ -146,9 +746,14 @@ pub(super) fn expr_numeric_by_construction(
                             numeric_fields,
                             not_bigint_locals,
                             const_local_inits,
+                            numeric_locals,
                             depth + 1,
                         );
                     }
+                    // #7770: a local every one of whose writes is
+                    // number-producing by construction — loop counters
+                    // above all.
+                    return numeric_locals.contains(id);
                 }
             }
             false
diff --git a/scripts/check_test_registration.py b/scripts/check_test_registration.py
index 06b6d79412..c212d0b454 100644
--- a/scripts/check_test_registration.py
+++ b/scripts/check_test_registration.py
@@ -278,6 +278,18 @@ def _stem(rel: str) -> str:
         registered=lambda t: _read_hash_list(t, "test-parity/gc_repsel_corpus.txt"),
         entry_to_path=lambda e: "test-files/%s.ts" % e,
         min_candidates=45,
+        exclusions={
+            "test_gap_repsel_element_group_numeric": (
+                "parity fixture for #7770's numeric-field proof, not a moving-GC "
+                "witness: its read loop is raw f64 loads with near-zero "
+                "allocation, so the matrix's scavenge arms are INERT on it "
+                "(liveness gate: counter=0, 0/1 cells live) and a registered "
+                "green cell would be green for the wrong reason. GC-under-"
+                "relocation coverage for this feature lives in the reproducer "
+                "run recorded on PR #7774 (1,762 evacuating minors, 400,014 "
+                "objects moved, exit 0) and in the ordinary parity harness."
+            ),
+        },
     ),
     Mechanism(
         id="feature-matrix-probes",
diff --git a/test-files/test_gap_repsel_element_group_numeric.ts b/test-files/test_gap_repsel_element_group_numeric.ts
new file mode 100644
index 0000000000..470134fdf6
--- /dev/null
+++ b/test-files/test_gap_repsel_element_group_numeric.ts
@@ -0,0 +1,224 @@
+// #7770: group-wide numeric-field proof for element-shape groups
+// (collectors/ptr_shape_numeric.rs::prove_group_numeric_fields).
+//
+// A `Ptr<Shape>`-promoted `const r = a[i]` binding now claims numeric fields
+// when the WHOLE group proves them: the meet over every push's `new`
+// arguments, plus every member's stores. A proven field's number-context
+// read is a bare raw load — no `js_number_coerce`, no value check — so the
+// direction this can be quietly wrong in is a non-number reaching a claimed
+// slot. Every case below routes a non-number through one of the reachable
+// store channels and must be BYTE-EXACT against Node.
+//
+// The promotions and claims themselves are asserted structurally in
+// `collectors/ptr_shape_elements_tests.rs` and
+// `collectors/ptr_shape_group_numeric_tests.rs`; the zero-coercion IR is
+// asserted by the #7770 acceptance run. A green run here with zero
+// promotions would be vacuous (#7024/#7025) — this file only pins Node
+// equivalence.
+
+class P {
+  x: number;
+  y: number;
+  constructor(x: number, y: number) {
+    this.x = x;
+    this.y = y;
+  }
+}
+
+// 1. The issue's reproducer: every store numeric by construction (loop
+//    counter args), fields claimed, reads coercion-free.
+function run(n: number): number {
+  const a: P[] = [];
+  for (let i = 0; i < n; i++) a.push(new P(i, i + 1));
+  let s = 0;
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    s += r.x + r.y;
+  }
+  return s;
+}
+console.log("repro:", run(1000));
+
+// 2. A sibling member stores a STRING into a claimed field. The group meet
+//    must drop `x` (the read below re-checks), while `y` stays claimed.
+function siblingString(): string {
+  const a: P[] = [];
+  for (let i = 0; i < 3; i++) a.push(new P(i, i * 10));
+  for (let i = 0; i < a.length; i++) {
+    const w = a[i];
+    if (i === 1) (w as any).x = "poison";
+  }
+  let out = "";
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    // No `+` on the poisoned field: `o.x + 1` on a string-holding
+    // declared-number field is a PRE-EXISTING divergence (numeric-classified
+    // Add; reproduces with PERRY_PTR_SHAPE_LOCALS=0 and no arrays — #7773).
+    // Value-context reads pin what #7770 must not break.
+    out += `${r.x}|${typeof r.x}|${r.y + 1};`;
+  }
+  return out;
+}
+console.log("sibling-string:", siblingString());
+
+// 3. Criterion-5 sweep: null / plain object / BigInt / boolean through a
+//    member, read back in value context (typeof, ===) and — where it cannot
+//    throw — number context.
+function adversarial(): string {
+  const a: P[] = [];
+  for (let i = 0; i < 4; i++) a.push(new P(i, i));
+  for (let i = 0; i < a.length; i++) {
+    const w = a[i];
+    if (i === 0) (w as any).x = null;
+    if (i === 1) (w as any).x = { v: 7 };
+    if (i === 2) (w as any).x = 1n;
+    if (i === 3) (w as any).x = true;
+  }
+  let out = "";
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    out += `${typeof r.x}:${String(r.x)}:${r.x === null}:${(r.x as any) === 1n};`;
+    out += `y=${r.y + 1};`;
+  }
+  return out;
+}
+console.log("adversarial:", adversarial());
+
+// 4. Number-context read of the null-stored field: ToNumber(null) is 0, and
+//    a bare raw load of NaN-boxed null bits would be NaN — the exact
+//    divergence the dropped claim must prevent.
+function nullNumberContext(): number {
+  const a: P[] = [];
+  a.push(new P(5, 6));
+  for (let i = 0; i < a.length; i++) {
+    const w = a[i];
+    (w as any).x = null;
+  }
+  let s = 0;
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    s += (r.x as any) + 1;
+  }
+  return s;
+}
+console.log("null-number-context:", nullNumberContext());
+
+// 5. A method-mediated store with a non-number argument: the parameter
+//    resolves through the merged call sites, so `x` drops group-wide.
+class Q {
+  x: number;
+  y: number;
+  constructor(x: number, y: number) {
+    this.x = x;
+    this.y = y;
+  }
+  setX(v: number): void {
+    this.x = v;
+  }
+}
+function methodStore(): string {
+  const a: Q[] = [];
+  for (let i = 0; i < 3; i++) a.push(new Q(i, i));
+  for (let i = 0; i < a.length; i++) {
+    const w = a[i];
+    if (i === 2) w.setX("s" as any);
+    else w.setX(i * 2);
+  }
+  let out = "";
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    // No `+` on the poisoned field — same pre-existing divergence as case 2.
+    out += `${r.x}|${typeof r.x}|${r.y};`;
+  }
+  return out;
+}
+console.log("method-store:", methodStore());
+
+// 6. Mixed push sites: the meet over ALL provenance `new`s — one site passes
+//    a string for `x`, so `x` drops even though the other sites are numeric.
+function mixedPushSites(): string {
+  const a: P[] = [];
+  a.push(new P(1, 2));
+  a.push(new P("s" as any, 3));
+  a.push(new P(4, 5));
+  let out = "";
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    out += `${r.x}|${typeof r.x}|${r.y + 1};`;
+  }
+  return out;
+}
+console.log("mixed-push:", mixedPushSites());
+
+// 7. NaN / Infinity / -0 are NUMBERS: the claim survives them, and the bare
+//    raw load must reproduce them exactly (including -0 identity).
+function specialNumbers(): string {
+  const a: P[] = [];
+  a.push(new P(NaN, Infinity));
+  a.push(new P(-0, -Infinity));
+  for (let i = 0; i < a.length; i++) {
+    const w = a[i];
+    w.y = w.y / 2;
+  }
+  let out = "";
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    out += `${r.x}|${r.y}|${Object.is(r.x, -0)}|${r.x === 0};`;
+  }
+  return out;
+}
+console.log("special-numbers:", specialNumbers());
+
+// 8. Producer-local pushes plus post-push mutation through the producer —
+//    the store is a member store, part of the same group universe.
+function producerMix(n: number): number {
+  const a: P[] = [];
+  for (let i = 0; i < n; i++) {
+    const p = new P(i, 0);
+    a.push(p);
+    p.y = i * 0.5;
+  }
+  let s = 0;
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    s += r.x - r.y;
+  }
+  return s;
+}
+console.log("producer-mix:", producerMix(100));
+
+// 9. `r.x++` through a member (the member_update fast path consumes the
+//    claim): sequence and final values must match Node.
+function updateThroughMember(): string {
+  const a: P[] = [];
+  for (let i = 0; i < 3; i++) a.push(new P(i, 0));
+  let seen = "";
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    seen += `${r.x++},${r.x};`;
+  }
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    seen += `${r.x}`;
+  }
+  return seen;
+}
+console.log("update:", updateThroughMember());
+
+// 10. Group integrity: an undeclared-property store on one member voids the
+//     whole group (no claims, no promotion) — behavior must be unchanged.
+function undeclaredProp(): string {
+  const a: P[] = [];
+  a.push(new P(1, 2));
+  for (let i = 0; i < a.length; i++) {
+    const w = a[i];
+    (w as any).extra = "e";
+  }
+  let out = "";
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    out += `${r.x + 1}|${(r as any).extra};`;
+  }
+  return out;
+}
+console.log("undeclared-prop:", undeclaredProp());