diff --git a/changelog.d/7831-declared-numeric-type-is-not-a-proof.md b/changelog.d/7831-declared-numeric-type-is-not-a-proof.md
new file mode 100644
index 0000000000..dc87c133f4
--- /dev/null
+++ b/changelog.d/7831-declared-numeric-type-is-not-a-proof.md
@@ -0,0 +1,48 @@
+### Fixed
+
+- **A declared numeric type is no longer treated as proof that the value is a
+  number** (#7773, #7776). Perry does not enforce annotations at runtime, but
+  codegen answered `is_numeric_expr` = `true` on the strength of one and then
+  emitted bare f64 arithmetic on whatever the slot actually held.
+
+  That is worse than producing a `NaN`, because arithmetic on a NaN-BOXED value
+  is not a no-op: `fadd`/`fmul` propagate the input NaN's payload, so a
+  NaN-boxed string comes back out of the instruction still tagged as that
+  string and flows on as if nothing happened — `typeof (v * 2)` answered
+  `"string"`. Four divergences from Node, all silent: `o.x + 1` gave `NaN`
+  where Node concatenates; `const v = o.x; v + 1` looked as though the `+ 1`
+  had evaporated; `v * 2` returned the string; and summing a `P[]` with one
+  `as any`-stored `Q` element gave `NaN`.
+
+  A new `numeric_proof_is_declared_only` separates "an annotation said so" from
+  a real proof. It is deliberately narrower than
+  `expr_may_return_boxed_value_from_raw_f64_fallback` (which answers "is there
+  a raw-f64 tier worth trying" and stays true for reads with no boxed fallback
+  at all): element-shape and class-field loop facts, `Ptr<Shape>` numeric
+  fields, scalar replacement, POD records and typed arrays all answer `false`
+  and keep their bare loads. `+` then lowers through an inline NaN-box tag test
+  — `fadd` on the fast arm, `js_dynamic_string_or_number_add` on the cold one —
+  because the spec's `+` dispatches on the runtime value; every other
+  arithmetic operator is a plain `ToNumber` and only needed the existing
+  residual-coerce rule taught to see a refined LOCAL.
+
+  `expr/mod.rs::lower_numeric_binary_value` turned out to be a second
+  arithmetic tier that bypasses `binary::lower` entirely and emits bare
+  `fadd`/`fmul` with no residual coerce at all; it was the path both
+  refined-local shapes took, and it now hands declared-only operands down the
+  same way its two existing `Mod` cases do.
+
+  Two details are load-bearing and are pinned by the test. The diamond covers
+  the whole `+` **tree**, not one node each: per-node diamonds make the outer
+  add of `s += o.x + 1` consume a phi that LLVM cannot prove is a canonical
+  double, which killed the `fadd` in the loop (+38% before fusing, +8.6%
+  after). And every leaf is tested except those `expr_produces_canonical_raw_f64`
+  vouches for — testing only the declared-only leaves skips the ACCUMULATOR,
+  which holds a string the moment this lowering's own cold arm concatenates,
+  and summed `16zw1113151719` down to `16zw`.
+
+  Measured on the quiet M1 mini, same runtime in both arms: element-shape clone
+  218 → 217 ms (−0.5%, untouched), `this.v + 1` in a method 70 → 76 ms (+8.6%),
+  `s += p.x + p.y` with an escaped receiver 196 → 263 ms (+34.2%). The cost
+  falls only on reads nothing could prove, which already pay an inline header
+  precheck or a `js_typed_feedback_class_field_get_guard` call.
diff --git a/crates/perry-codegen/src/codegen/closure.rs b/crates/perry-codegen/src/codegen/closure.rs
index cc6649b715..69a7431ac5 100644
--- a/crates/perry-codegen/src/codegen/closure.rs
+++ b/crates/perry-codegen/src/codegen/closure.rs
@@ -978,6 +978,7 @@ pub(super) fn compile_closure(
         temp_roots: crate::rooting::TempRootPool::default(),
         shadow_slot_map,
         persistent_shadow_slots: std::collections::HashSet::new(),
+        declared_only_numeric_locals: std::collections::HashSet::new(),
         shadow_slot_clears_after_stmt,
         arena_state_slot: None,
         class_keys_slots: HashMap::new(),
diff --git a/crates/perry-codegen/src/codegen/entry.rs b/crates/perry-codegen/src/codegen/entry.rs
index 2d83315a46..b416ea3219 100644
--- a/crates/perry-codegen/src/codegen/entry.rs
+++ b/crates/perry-codegen/src/codegen/entry.rs
@@ -816,6 +816,7 @@ pub(super) fn compile_module_entry(
             temp_roots: crate::rooting::TempRootPool::default(),
             shadow_slot_map: main_shadow_slot_map,
             persistent_shadow_slots: std::collections::HashSet::new(),
+            declared_only_numeric_locals: std::collections::HashSet::new(),
             shadow_slot_clears_after_stmt: main_shadow_slot_clears_after_stmt,
             arena_state_slot: None,
             class_keys_slots: HashMap::new(),
@@ -1485,6 +1486,7 @@ pub(super) fn compile_module_entry(
             temp_roots: crate::rooting::TempRootPool::default(),
             shadow_slot_map: init_shadow_slot_map,
             persistent_shadow_slots: std::collections::HashSet::new(),
+            declared_only_numeric_locals: std::collections::HashSet::new(),
             shadow_slot_clears_after_stmt: init_shadow_slot_clears_after_stmt,
             arena_state_slot: None,
             class_keys_slots: HashMap::new(),
diff --git a/crates/perry-codegen/src/codegen/function.rs b/crates/perry-codegen/src/codegen/function.rs
index af8230201e..4b6026f983 100644
--- a/crates/perry-codegen/src/codegen/function.rs
+++ b/crates/perry-codegen/src/codegen/function.rs
@@ -770,6 +770,7 @@ pub(super) fn compile_function(
         unsigned_i32_locals: native_facts.unsigned_i32_locals(),
         shadow_slot_map,
         persistent_shadow_slots: std::collections::HashSet::new(),
+        declared_only_numeric_locals: std::collections::HashSet::new(),
         shadow_slot_clears_after_stmt,
         shadow_slots_bound: bound_param_slots,
         temp_roots: crate::rooting::TempRootPool::default(),
diff --git a/crates/perry-codegen/src/codegen/method.rs b/crates/perry-codegen/src/codegen/method.rs
index 70c0bbac63..eadaff919c 100644
--- a/crates/perry-codegen/src/codegen/method.rs
+++ b/crates/perry-codegen/src/codegen/method.rs
@@ -509,6 +509,7 @@ pub(super) fn compile_method(
         temp_roots: crate::rooting::TempRootPool::default(),
         shadow_slot_map,
         persistent_shadow_slots: std::collections::HashSet::new(),
+        declared_only_numeric_locals: std::collections::HashSet::new(),
         shadow_slot_clears_after_stmt,
         arena_state_slot: None,
         class_keys_slots: HashMap::new(),
@@ -1572,6 +1573,7 @@ pub(super) fn compile_static_method(
         temp_roots: crate::rooting::TempRootPool::default(),
         shadow_slot_map,
         persistent_shadow_slots: std::collections::HashSet::new(),
+        declared_only_numeric_locals: std::collections::HashSet::new(),
         shadow_slot_clears_after_stmt,
         arena_state_slot: None,
         class_keys_slots: HashMap::new(),
diff --git a/crates/perry-codegen/src/expr/binary.rs b/crates/perry-codegen/src/expr/binary.rs
index f00a2bea78..cb1a9a2a63 100644
--- a/crates/perry-codegen/src/expr/binary.rs
+++ b/crates/perry-codegen/src/expr/binary.rs
@@ -18,7 +18,7 @@ use crate::native_value::{
 use crate::type_analysis::{
     add_operands_have_pod_materialization_hazard,
     expr_may_return_boxed_value_from_raw_f64_fallback, is_bigint_expr, is_bool_expr,
-    is_numeric_expr,
+    is_numeric_expr, numeric_proof_is_declared_only,
 };
 use crate::types::{DOUBLE, I1, I128, I32, I64};
 
@@ -51,6 +51,166 @@ fn lower_rooted_dynamic_binary(
     })
 }
 
+/// `+` where both operands are statically numeric but at least one of them is
+/// numeric only because a DECLARED type said so (#7773, #7776).
+///
+/// Nothing enforces annotations at runtime, so a `x: number` slot reached
+/// through `as any` really can hold a string — and then the spec says `+` is
+/// string concatenation, which is what Node does. Trusting the annotation cost
+/// two different wrong answers, both silent:
+///
+/// * `o.x + 1` produced `NaN`, because the number-context read's cold arm
+///   `js_number_coerce`s unconditionally; Node prints `s1`.
+/// * through a refined local the add did not even coerce — `fadd` on a
+///   NaN-BOXED value propagates the input payload on both AArch64 and x86-64,
+///   so the string came back out of the add still a string, and the `+ 1`
+///   looked like it had evaporated.
+///
+/// So re-check at runtime instead of assuming. The fast arm keeps the inline
+/// `fadd`; only a value that is not a canonical double reaches the dynamic
+/// helper, which is the one that implements the spec's `+`.
+///
+/// **The whole `+` TREE becomes one diamond, not one per node.** That is a
+/// correctness-neutral but performance-critical detail, and doing it the
+/// obvious way first is what showed why. Per-node diamonds make the outer add
+/// of `s += o.x + 1` consume a PHI, and LLVM cannot prove a phi over
+/// (`fadd`, runtime call) is a canonical double — so the outer test never
+/// folded, its cold arm stayed live in the loop, and `Acc.run`'s hot loop lost
+/// its `fadd` to an unconditional call. Measured on the bench mini that shape
+/// went 86 ms -> 119 ms. Fusing the tree removes the phi entirely: one test
+/// over the tree's violable LEAVES, one branch, then either all-`fadd` or
+/// all-`js_dynamic_string_or_number_add`.
+///
+/// Associativity is preserved rather than assumed away: both arms rebuild the
+/// ORIGINAL tree shape. `1 + (2 + "x")` is `"12x"` and `(1 + 2) + "x"` is
+/// `"3x"`, so a flattened re-association would be a wrong answer — the leaves
+/// are collected in evaluation order for rooting, but the arms are rebuilt
+/// node-for-node.
+///
+/// Every leaf is tested EXCEPT those that `expr_produces_canonical_raw_f64`
+/// vouches for (literals, `Math.*`, an explicit coerce, non-`+` arithmetic).
+/// Testing only the declared-only leaves is not enough, and the accumulator is
+/// the counter-example: `let s = 0; s += r.x + r.y` types `s` as `Number`, but
+/// the moment this very lowering's cold arm concatenates, `s` HOLDS A STRING
+/// while its static type still says otherwise. Skipping it summed
+/// `16zw1113151719` down to `16zw` — the fast arm `fadd`ed a NaN-boxed string
+/// and passed it through unchanged, which is the original bug reintroduced one
+/// level up. `expr_produces_canonical_raw_f64` declines to vouch for a
+/// `LocalGet` precisely because a local is a slot somebody can store into.
+///
+/// The residual cost lands where it is already small: every read that reaches
+/// here is one the compiler could NOT prove, so it pays an inline header
+/// precheck or a `js_typed_feedback_class_field_get_guard` call for its shape
+/// check regardless. The proven tiers (element-shape / class-field loop facts,
+/// `Ptr<Shape>` numeric fields, scalar replacement, POD records, typed arrays)
+/// never get here at all — `numeric_proof_is_declared_only` answers `false`.
+fn lower_declared_only_numeric_add(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<String> {
+    let mut leaves = Vec::new();
+    add_tree_leaves(expr, &mut leaves);
+    let needs_test: Vec<bool> = leaves
+        .iter()
+        .map(|leaf| !crate::type_analysis::expr_produces_canonical_raw_f64(ctx, leaf))
+        .collect();
+
+    with_operands_rooted(ctx, &leaves, |ctx, values| {
+        let mut cond: Option<String> = None;
+        for (value, is_tested) in values.iter().zip(needs_test.iter()) {
+            if !is_tested {
+                continue;
+            }
+            let is_num = crate::stmt::emit_js_value_is_number(ctx, value);
+            cond = Some(match cond {
+                Some(prev) => ctx.block().and(I1, &prev, &is_num),
+                None => is_num,
+            });
+        }
+        // The caller only routes here when a leaf is declared-only, and every
+        // such leaf is a field / element / local read — none of which
+        // `expr_produces_canonical_raw_f64` vouches for. So there is always at
+        // least one test; an empty condition would mean the two predicates had
+        // drifted apart, which is worth a hard error rather than a silent
+        // unguarded `fadd`.
+        let Some(all_num) = cond else {
+            anyhow::bail!(
+                "declared-only `+` tree has no testable leaf: \
+                 numeric_proof_is_declared_only and expr_produces_canonical_raw_f64 disagree"
+            );
+        };
+
+        let fast_idx = ctx.new_block("declared_add.numeric");
+        let slow_idx = ctx.new_block("declared_add.dynamic");
+        let merge_idx = ctx.new_block("declared_add.merge");
+        let fast_label = ctx.block_label(fast_idx);
+        let slow_label = ctx.block_label(slow_idx);
+        let merge_label = ctx.block_label(merge_idx);
+        ctx.block().cond_br(&all_num, &fast_label, &slow_label);
+
+        ctx.current_block = fast_idx;
+        let fast_val = rebuild_add_tree(ctx, expr, values, &mut 0, true);
+        let fast_end = ctx.block().label.clone();
+        ctx.block().br(&merge_label);
+
+        ctx.current_block = slow_idx;
+        let slow_val = rebuild_add_tree(ctx, expr, values, &mut 0, false);
+        let slow_end = ctx.block().label.clone();
+        ctx.block().br(&merge_label);
+
+        ctx.current_block = merge_idx;
+        Ok(ctx
+            .block()
+            .phi(DOUBLE, &[(&fast_val, &fast_end), (&slow_val, &slow_end)]))
+    })
+}
+
+/// The `+` tree's operand leaves, in evaluation order — a left-to-right walk,
+/// so `with_operands_rooted` lowers them in the order JS evaluates them.
+fn add_tree_leaves<'a>(expr: &'a Expr, out: &mut Vec<&'a Expr>) {
+    if let Expr::Binary {
+        op: BinaryOp::Add,
+        left,
+        right,
+    } = expr
+    {
+        add_tree_leaves(left, out);
+        add_tree_leaves(right, out);
+    } else {
+        out.push(expr);
+    }
+}
+
+/// Rebuild the `+` tree over already-lowered leaf values, node for node, so the
+/// original associativity survives. `fast` picks the inline `fadd`; otherwise
+/// every node goes through the spec-`+` helper.
+fn rebuild_add_tree(
+    ctx: &mut FnCtx<'_>,
+    expr: &Expr,
+    values: &[String],
+    next_leaf: &mut usize,
+    fast: bool,
+) -> String {
+    if let Expr::Binary {
+        op: BinaryOp::Add,
+        left,
+        right,
+    } = expr
+    {
+        let l = rebuild_add_tree(ctx, left, values, next_leaf, fast);
+        let r = rebuild_add_tree(ctx, right, values, next_leaf, fast);
+        return if fast {
+            ctx.block().fadd(&l, &r)
+        } else {
+            ctx.block().call(
+                DOUBLE,
+                "js_dynamic_string_or_number_add",
+                &[(DOUBLE, &l), (DOUBLE, &r)],
+            )
+        };
+    }
+    let value = values[*next_leaf].clone();
+    *next_leaf += 1;
+    value
+}
+
 fn lower_arithmetic_operand(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<(String, bool)> {
     // #6884: a statically typed numeric TypedArray read is Number|undefined,
     // not an unconditional raw f64. In arithmetic context the OOB `undefined`
@@ -145,7 +305,17 @@ fn lower_arithmetic_operand(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<(String,
 fn operand_needs_residual_coerce(ctx: &FnCtx<'_>, expr: &Expr, fallback_coerced: bool) -> bool {
     !fallback_coerced
         && (!is_numeric_expr(ctx, expr)
-            || expr_may_return_boxed_value_from_raw_f64_fallback(ctx, expr))
+            || expr_may_return_boxed_value_from_raw_f64_fallback(ctx, expr)
+            // #7773: a local REFINED to `Number` from a declared field/element
+            // type is `is_numeric_expr`, but the hazard predicate above only
+            // knows how to look at reads, so `const v = o.x; v * 2` emitted a
+            // bare `fmul`. Arithmetic on a NaN-box preserves the payload, so
+            // that multiply returned the string unchanged — `typeof (v * 2)`
+            // answered `"string"`. Every non-`+` arithmetic operator is a plain
+            // `ToNumber` on its operands, so a coerce is the whole fix here;
+            // `+` needs the concat dispatch and gets it from
+            // `lower_declared_only_numeric_add`.
+            || matches!(expr, Expr::LocalGet(_)) && numeric_proof_is_declared_only(ctx, expr))
 }
 
 /// Lower an operand in number context: route through
@@ -519,6 +689,15 @@ pub(crate) fn lower(ctx: &mut FnCtx<'_>, expr: &Expr) -> Result<String> {
                         right,
                     );
                 }
+                // Both sides are statically numeric — but "statically" can mean
+                // "an annotation said so", and annotations are not enforced
+                // (#7773, #7776). Re-check the tag at runtime rather than
+                // emitting a bare `fadd` on a value that may be NaN-boxed.
+                if numeric_proof_is_declared_only(ctx, left)
+                    || numeric_proof_is_declared_only(ctx, right)
+                {
+                    return lower_declared_only_numeric_add(ctx, expr);
+                }
             }
             // BigInt arithmetic fast path. NaN-tagged bigints compare
             // unordered under `fadd`/`fsub`/`fmul`/`fdiv`/`frem` (the
diff --git a/crates/perry-codegen/src/expr/mod.rs b/crates/perry-codegen/src/expr/mod.rs
index b3d19b9cb0..37a06e8353 100644
--- a/crates/perry-codegen/src/expr/mod.rs
+++ b/crates/perry-codegen/src/expr/mod.rs
@@ -744,6 +744,23 @@ pub(crate) struct FnCtx<'a> {
     /// protected temporary this function lowers.
     pub temp_roots: crate::rooting::TempRootPool,
 
+    /// #7773: LocalIds whose `Number`/`Int32` type was REFINED from a read
+    /// whose own numeric answer is only a declared type — `const v = o.x` on a
+    /// `x: number` field, or `const e = arr[i]` on a `number[]`.
+    ///
+    /// The refinement is load-bearing (an un-annotated `const` is `Any` in the
+    /// HIR, so without it every ordinary field read loses the numeric fast
+    /// path), but it copies an annotation rather than proving anything. The
+    /// local then reads as `is_numeric_expr`, which licenses a bare `fadd` /
+    /// `fmul` on whatever the slot holds — and arithmetic on a NaN-boxed value
+    /// PRESERVES ITS PAYLOAD, so a string laundered in through `as any` came
+    /// back out of a multiply still tagged as a string (`typeof (v * 2)` was
+    /// `"string"`).
+    ///
+    /// Consumed by `type_analysis::numeric_proof_is_declared_only`, which turns
+    /// the trust into a four-instruction runtime tag test instead.
+    pub declared_only_numeric_locals: std::collections::HashSet<u32>,
+
     /// Cached pointer to this function's `InlineArenaState` slot —
     /// allocated lazily on the first `new ClassName()` site that uses
     /// the inline bump-allocator path. The slot lives in the function
@@ -2393,6 +2410,26 @@ fn lower_numeric_binary_value(
         return Ok(None);
     }
 
+    // #7773: `is_numeric_expr` answering `true` is not always a PROOF — for a
+    // class-field read, an array element, or a local refined from one, it is
+    // just the declared type repeated back, and nothing enforces declared types
+    // at runtime. This tier emits a bare `fadd`/`fmul` with no residual coerce
+    // at all, and arithmetic on a NaN-BOXED value propagates the payload
+    // instead of producing NaN — so a string laundered into a `x: number` slot
+    // came back out of `v * 2` still a string (`typeof` said `"string"`).
+    //
+    // Hand those to `binary::lower`, which has both remedies: the runtime tag
+    // test that keeps `+` on the spec's string-concat dispatch, and the
+    // residual `js_number_coerce` that gives every other operator its
+    // `ToNumber`. Same hand-off shape as the two Mod cases below, and for the
+    // same reason — it must run before operand lowering so an `Ok(None)` emits
+    // no dead loads or duplicate records.
+    if crate::type_analysis::numeric_proof_is_declared_only(ctx, left)
+        || crate::type_analysis::numeric_proof_is_declared_only(ctx, right)
+    {
+        return Ok(None);
+    }
+
     // Hand this proven shape to `binary::lower`, which owns the existing
     // integer remainder and negative-zero repair. This must run before operand
     // lowering so returning `None` emits no dead loads or duplicate records.
diff --git a/crates/perry-codegen/src/stmt/let_stmt.rs b/crates/perry-codegen/src/stmt/let_stmt.rs
index 1c8739b298..4e23d1b3d4 100644
--- a/crates/perry-codegen/src/stmt/let_stmt.rs
+++ b/crates/perry-codegen/src/stmt/let_stmt.rs
@@ -290,6 +290,27 @@ pub(crate) fn lower_let(
         ty.clone()
     };
 
+    // #7773: the refinement above copies a DECLARED type — `const v = o.x` on a
+    // `x: number` field answers `Number` because the annotation says so, not
+    // because anything proved it. Nothing enforces annotations at runtime, so
+    // record the local as violable; `numeric_proof_is_declared_only` then makes
+    // arithmetic on it re-check the tag instead of trusting the type outright.
+    //
+    // Only the Any → numeric direction matters. A local the user DECLARED
+    // `number` is equally unenforced, but it is also the shape every honest
+    // program is made of; the refined case is the one where codegen invented
+    // the numeric claim itself, and it is the one both reported shapes need.
+    if matches!(ty, perry_hir::types::Type::Any)
+        && matches!(
+            refined_ty,
+            perry_hir::types::Type::Number | perry_hir::types::Type::Int32
+        )
+    {
+        if init.is_some_and(|e| crate::type_analysis::numeric_proof_is_declared_only(ctx, e)) {
+            ctx.declared_only_numeric_locals.insert(id);
+        }
+    }
+
     // Track closure func_id → local_id mapping so the closure
     // call site in lower_call can look up rest param info.
     if let Some(perry_hir::Expr::Closure {
diff --git a/crates/perry-codegen/src/stmt/loops.rs b/crates/perry-codegen/src/stmt/loops.rs
index 9e67e21048..6e8938f915 100644
--- a/crates/perry-codegen/src/stmt/loops.rs
+++ b/crates/perry-codegen/src/stmt/loops.rs
@@ -4569,7 +4569,7 @@ fn dynamic_bound_private_counter_is_safe(
     advanced_by_increment && !stmts_mutate_local(body, counter_id)
 }
 
-pub(super) fn emit_js_value_is_number(ctx: &mut FnCtx<'_>, value: &str) -> String {
+pub(crate) fn emit_js_value_is_number(ctx: &mut FnCtx<'_>, value: &str) -> String {
     let n_bits = ctx.block().bitcast_double_to_i64(value);
     let tag = ctx.block().and(
         I64,
diff --git a/crates/perry-codegen/src/stmt/mod.rs b/crates/perry-codegen/src/stmt/mod.rs
index 2efdefe3d8..635ba339c1 100644
--- a/crates/perry-codegen/src/stmt/mod.rs
+++ b/crates/perry-codegen/src/stmt/mod.rs
@@ -31,7 +31,7 @@ mod unused_expr;
 
 pub(crate) use if_stmt::lower_if;
 pub(crate) use let_stmt::lower_let;
-pub(crate) use loops::{lower_do_while, lower_for, lower_while};
+pub(crate) use loops::{emit_js_value_is_number, lower_do_while, lower_for, lower_while};
 pub(crate) use switch_stmt::lower_switch;
 pub(crate) use try_stmt::lower_try;
 
diff --git a/crates/perry-codegen/src/type_analysis.rs b/crates/perry-codegen/src/type_analysis.rs
index 34840e3ac0..53e8c71cf3 100644
--- a/crates/perry-codegen/src/type_analysis.rs
+++ b/crates/perry-codegen/src/type_analysis.rs
@@ -38,7 +38,8 @@ pub(crate) use numeric::{
 pub(crate) use pod::{
     add_operands_have_pod_materialization_hazard,
     expr_may_return_boxed_value_from_raw_f64_fallback, expression_has_numeric_length,
-    is_fixed_width_buffer_numeric_read, is_numeric_typed_array_class, pod_record_field_is_numeric,
+    is_fixed_width_buffer_numeric_read, is_numeric_typed_array_class,
+    numeric_proof_is_declared_only, pod_record_field_is_numeric,
     scalar_replaced_array_element_is_raw_f64, scalar_replaced_field_is_raw_f64,
     scalar_replaced_field_raw_f64_store_state,
 };
diff --git a/crates/perry-codegen/src/type_analysis/pod.rs b/crates/perry-codegen/src/type_analysis/pod.rs
index 87391a4f8b..4bdd9110bc 100644
--- a/crates/perry-codegen/src/type_analysis/pod.rs
+++ b/crates/perry-codegen/src/type_analysis/pod.rs
@@ -437,6 +437,137 @@ pub(crate) fn expr_may_return_boxed_value_from_raw_f64_fallback(
     }
 }
 
+/// True when this expression's "the value is a Number" answer rests ONLY on a
+/// **declared** type — a class-field annotation or an array's element type —
+/// which nothing enforces at runtime (CLAUDE.md, Known Limitations: annotations
+/// are erased, so `(o as any).x = "s"` stores a string into a `x: number` slot).
+///
+/// This is deliberately NARROWER than
+/// [`expr_may_return_boxed_value_from_raw_f64_fallback`], which answers "is
+/// there a raw-f64 tier worth trying" and stays `true` for reads that end up
+/// with no boxed fallback at all. Here every arm that carries a REAL proof —
+/// a guard, a closed store universe, or scalar replacement — answers `false`,
+/// because for those the value provably is a double and a runtime re-check
+/// would be dead code:
+///
+/// * element-shape loop fact — the preheader pinned the element class and the
+///   per-element residual check requires `GC_OBJ_TYPED_LAYOUT_INTACT`;
+/// * class-field loop fact — the preheader shape check already ran;
+/// * `Ptr<Shape>` `numeric_fields` — every reachable store is a number;
+/// * scalar replacement — there is no heap slot for anyone to write;
+/// * POD record fields — the layout is native, not a NaN-boxed slot;
+/// * masked-window element facts — the window was proven.
+///
+/// What remains is the guarded class-field / element diamond, whose cold arm
+/// exists precisely because the declared type can be wrong. Answering `true`
+/// there is cheap by construction: that read already pays either an inline
+/// header precheck or a `js_typed_feedback_class_field_get_guard` call, so a
+/// four-instruction tag test beside it is noise.
+///
+/// Conservative direction: a missed `false` costs those four instructions; a
+/// missed `true` is a wrong answer (#7773, #7776), so unproven reads answer
+/// `true`.
+pub(crate) fn numeric_proof_is_declared_only(ctx: &FnCtx<'_>, expr: &Expr) -> bool {
+    match expr {
+        Expr::PropertyGet {
+            object, property, ..
+        } => {
+            // `.length` is produced by the runtime, not read out of a
+            // user-writable slot.
+            if property == "length" {
+                return false;
+            }
+            if !expr_may_return_boxed_value_from_raw_f64_fallback(ctx, expr) {
+                return false;
+            }
+            if crate::expr::element_shape_loop_fact_for_property_get(ctx, object, property)
+                .is_some()
+            {
+                return false;
+            }
+            if pod_record_field_is_numeric(ctx, object, property) {
+                return false;
+            }
+            // Scalar replacement, reached through the local and through `this`
+            // inside an inlined constructor — the same two spellings
+            // `is_numeric_expr` handles.
+            if let Expr::LocalGet(id) = object.as_ref() {
+                if ctx
+                    .scalar_replaced
+                    .get(id)
+                    .is_some_and(|fields| fields.contains_key(property.as_str()))
+                {
+                    return false;
+                }
+            }
+            if matches!(object.as_ref(), Expr::This) {
+                if let Some(target_id) = ctx.scalar_ctor_target.last().copied() {
+                    if ctx
+                        .scalar_replaced
+                        .get(&target_id)
+                        .is_some_and(|fields| fields.contains_key(property.as_str()))
+                    {
+                        return false;
+                    }
+                }
+            }
+            let Some(class_name) = receiver_class_name(ctx, object) else {
+                return false;
+            };
+            if let Expr::LocalGet(recv_id) = object.as_ref() {
+                if crate::expr::class_field_loop_fact_lookup(
+                    &ctx.class_field_loop_facts,
+                    *recv_id,
+                    &class_name,
+                    property,
+                )
+                .is_some()
+                {
+                    return false;
+                }
+            }
+            let ptr_shape_numeric = ctx
+                .ptr_shape_receiver_fact(object.as_ref())
+                .map(|fact| fact.class_name == class_name && fact.numeric_fields.contains(property))
+                .unwrap_or(false);
+            !ptr_shape_numeric
+        }
+        Expr::IndexGet { object, index } => {
+            if !expr_may_return_boxed_value_from_raw_f64_fallback(ctx, expr) {
+                return false;
+            }
+            if let Expr::LocalGet(arr_id) = object.as_ref() {
+                if crate::expr::masked_window_fact_for_index(ctx, *arr_id, index).is_some() {
+                    return false;
+                }
+            }
+            // A typed array's storage is native bytes — a non-numeric store is
+            // converted on the way in, so the read cannot surface one.
+            !receiver_class_name(ctx, object)
+                .as_deref()
+                .is_some_and(is_numeric_typed_array_class)
+        }
+        // A local whose `Number` type was REFINED from one of the reads above
+        // inherits its violability — the refinement copied a declared type, it
+        // did not prove anything (#7773 second shape: `const v: any = o.x`
+        // typed `v` numeric, so `v * 2` became a bare `fmul` on whatever the
+        // slot held and a NaN-boxed string passed straight through it).
+        Expr::LocalGet(id) => ctx.declared_only_numeric_locals.contains(id),
+        // `a + b` is numeric only when both sides are, so it is violable when
+        // either side is; `a || b` / `a && b` / `a ?? b` pass one operand
+        // VALUE through, so the same holds. Both mirror `is_numeric_expr`.
+        Expr::Binary {
+            op: perry_hir::BinaryOp::Add,
+            left,
+            right,
+        }
+        | Expr::Logical { left, right, .. } => {
+            numeric_proof_is_declared_only(ctx, left) || numeric_proof_is_declared_only(ctx, right)
+        }
+        _ => false,
+    }
+}
+
 pub(crate) fn is_fixed_width_buffer_numeric_read(method: &str) -> bool {
     matches!(
         method,
diff --git a/test-files/test_gap_declared_numeric_field_holds_string_7773.ts b/test-files/test_gap_declared_numeric_field_holds_string_7773.ts
new file mode 100644
index 0000000000..bb0d3ed7f3
--- /dev/null
+++ b/test-files/test_gap_declared_numeric_field_holds_string_7773.ts
@@ -0,0 +1,181 @@
+// A declared type is a hint, not a layout fact (CLAUDE.md, Known Limitations:
+// annotations are erased, nothing validates them at runtime). Codegen answered
+// `is_numeric_expr` = true on the strength of one anyway, and then emitted bare
+// f64 arithmetic on whatever the slot actually held.
+//
+// That is worse than it sounds, because arithmetic on a NaN-BOXED value is not
+// a no-op that yields NaN — `fadd`/`fmul` propagate the input NaN's payload, so
+// a NaN-boxed string comes back out of the instruction STILL TAGGED AS THAT
+// STRING. `typeof (v * 2)` answered "string", and `v + 1` looked as though the
+// `+ 1` had simply evaporated.
+//
+// Three divergences, all silent:
+//   #7773 shape 1 — `o.x + 1` gave NaN (the number-context read's cold arm
+//                   coerces unconditionally); Node concatenates.
+//   #7773 shape 2 — through a refined local (`const v = o.x`) there was no
+//                   coerce at all, so the string passed straight through.
+//   #7776         — a heterogeneous element stored via `as any`, then summed.
+//
+// The escape is required in every case: a non-escaping receiver gets
+// scalar-replaced, which is a real proof, and prints correctly already.
+
+class C {
+  x: number;
+  constructor(x: number) {
+    this.x = x;
+  }
+}
+function poison(o: C): void {
+  (o as any).x = "s";
+}
+
+// #7773 shape 1: the add is spec'd to dispatch on the RUNTIME value.
+function directAdd(): string {
+  const o = new C(1);
+  poison(o);
+  return `${o.x + 1}`;
+}
+
+// #7773 shape 2: through a local whose `number` type codegen INFERRED by
+// copying the declared field type. Every operator, because only `+` concatenates
+// — the rest are plain ToNumber and must give NaN, not a passed-through string.
+function throughRefinedLocal(): string {
+  const o = new C(1);
+  poison(o);
+  const v: any = o.x;
+  return `${v + 1} ${v - 1} ${v * 2} ${v / 2} ${typeof (v * 2)}`;
+}
+
+// The number on the left: `1 + v` concatenates the other way round.
+function numberOnTheLeft(): string {
+  const o = new C(1);
+  poison(o);
+  const v: any = o.x;
+  return `${1 + v}`;
+}
+
+// #7776: a different-shape element reached through `as any`. The element-shape
+// fast clone correctly declines this array at runtime (it is heterogeneous);
+// the divergence was in the generic path that then ran.
+//
+// This one also pins a SECOND bug, found while fixing the first: the
+// accumulator. `s` is declared `number` by `let s = 0`, and it really is one —
+// until index 4 concatenates and `s` holds a string for the remaining five
+// iterations while its static type still says `Number`. A fix that tests only
+// the operands whose DECLARED type is suspect skips `s`, `fadd`s a NaN-boxed
+// string, passes it through unchanged, and prints `16zw` — the original bug,
+// one level up. So the expected value here is load-bearing digit by digit, not
+// just "not NaN".
+class P {
+  x: number;
+  y: number;
+  constructor(x: number, y: number) {
+    this.x = x;
+    this.y = y;
+  }
+}
+class Q {
+  x: string;
+  y: string;
+  constructor(x: string, y: string) {
+    this.x = x;
+    this.y = y;
+  }
+}
+function heterogeneousElements(): string {
+  const a: P[] = [];
+  for (let i = 0; i < 10; i++) a.push(new P(i, i + 1));
+  (a as any)[4] = new Q("z", "w");
+  let s = 0;
+  for (let i = 0; i < a.length; i++) {
+    const r = a[i];
+    s += r.x + r.y;
+  }
+  return `${s}`;
+}
+
+// An array's declared ELEMENT type is violable the same way a field's is.
+function arrayElement(): string {
+  const a: number[] = [1, 2, 3];
+  (a as any)[1] = "q";
+  return `${a[1] + 1} ${a[0] + 1} ${a[1] * 2}`;
+}
+
+// An INHERITED field resolves through the same class walk, so it must get the
+// same treatment.
+class Base {
+  n: number;
+  constructor(n: number) {
+    this.n = n;
+  }
+}
+class Derived extends Base {
+  constructor(n: number) {
+    super(n);
+  }
+}
+function inheritedField(): string {
+  const d = new Derived(3);
+  (d as any).n = "j";
+  return `${d.n + 1}`;
+}
+
+// `a + b + c` is left-associative, and the inner Add is only numeric when both
+// of ITS operands are — the recursion in the predicate has to agree with the
+// one in `is_numeric_expr` or the chain re-acquires the bad proof one level up.
+function chainedAdd(): string {
+  const p = new P(1, 2);
+  (p as any).y = "Y";
+  return `${p.x + p.y + 1}`;
+}
+
+// THE OTHER DIRECTION — these must keep answering as numbers. A fix that
+// coerced or dispatched everything would pass every assertion above while
+// quietly turning ordinary arithmetic into string concatenation, so the honest
+// shapes are asserted for VALUE, not merely for "does not crash".
+function honestArithmetic(): string {
+  const pts: P[] = [];
+  for (let i = 0; i < 5; i++) pts.push(new P(i, i * 2));
+  let s = 0;
+  for (let i = 0; i < pts.length; i++) {
+    const q = pts[i];
+    s += q.x + q.y;
+  }
+  const one = new P(3, 4);
+  const viaLocal: any = one.x;
+  return `${s} ${one.x + one.y} ${viaLocal + 1} ${viaLocal * 2} ${typeof (viaLocal + 1)}`;
+}
+
+// A guard failure on an HONEST value must stay on the numeric answer. Adding a
+// dynamic property makes the class-field guard fail, so this takes the boxed
+// fallback with a value that really is a number — the arm that would break if
+// the fix reached for "always concatenate" instead of a runtime tag test.
+function addExtra(o: C): void {
+  (o as any).extra = 7;
+}
+function honestGuardFailure(): string {
+  const o = new C(5);
+  addExtra(o);
+  const v: any = o.x;
+  return `${typeof v} ${v * 2} ${v + 1}`;
+}
+
+// A typed array converts on STORE, so its declared element type is not violable
+// and must keep the native read path.
+function typedArrayUnaffected(): string {
+  const t = new Float64Array(3);
+  t[0] = 1.5;
+  (t as any)[1] = "5";
+  return `${t[0] + 1} ${t[1] + 1}`;
+}
+
+console.log("direct add:", directAdd());
+console.log("refined local:", throughRefinedLocal());
+console.log("number on left:", numberOnTheLeft());
+console.log("heterogeneous:", heterogeneousElements());
+console.log("array element:", arrayElement());
+console.log("inherited field:", inheritedField());
+console.log("chained add:", chainedAdd());
+console.log("honest arithmetic:", honestArithmetic());
+console.log("honest guard failure:", honestGuardFailure());
+console.log("typed array:", typedArrayUnaffected());