diff --git a/OrchardMath/Millennium/HardySign.lean b/OrchardMath/Millennium/HardySign.lean
index dfa6603..703cc47 100644
--- a/OrchardMath/Millennium/HardySign.lean
+++ b/OrchardMath/Millennium/HardySign.lean
@@ -19,9 +19,13 @@ odd numbers, the exact identity
 turns the multinomial comparison into supermultiplicativity of `oddProd`, which
 is a two-line induction.
 
-Scope. This is the combinatorial engine only. It is not a formalization of the
-Bui-Hall conjecture, of the integral reduction, of the generating-function
-positivity argument, or of anything about the Riemann zeta function.
+Scope, stated precisely. Formalized here are (a) the cleared numerator
+inequality underlying equation (13), and (b) the unconstrained sign-character
+sum that feeds equation (12). NOT formalized: the generating-function
+coefficient identities that turn these into statements about `F` and `log R`,
+the restriction of the character sum to even-weight sign vectors, the integral
+reduction of section 1, the positivity transfer through `exp`, the Bui-Hall
+conjecture itself, and anything about the Riemann zeta function.
 -/
 import Mathlib.Data.Nat.Choose.Multinomial
 import Mathlib.Tactic
@@ -143,9 +147,12 @@ theorem multinomial_le_multinomial_two_mul (s : Finset α) (f : α → ℕ) :
       _ ≤ _ := step
   exact Nat.le_of_mul_le_mul_left step' hpos
 
-/-- **Equation (13) of the source note.** The coefficient of `F` at an all-even
-multi-index is strictly positive, in the cleared integer form
-`multinomial a < 4 * multinomial (2a)`. -/
+/-- **The cleared numerator inequality of equation (13).** The note concludes
+that the coefficient of `F` at an all-even multi-index is strictly positive;
+after clearing the factor `1 / N` and the generating-function identification,
+that reduces to `multinomial a < 4 * multinomial (2a)`, which is what is proved
+here. The identification of this quantity with a coefficient of `F` is not
+formalized. -/
 theorem multinomial_lt_four_mul_multinomial_two_mul (s : Finset α) (f : α → ℕ) :
     Nat.multinomial s f < 4 * Nat.multinomial s (fun i => 2 * f i) := by
   have h := multinomial_le_multinomial_two_mul s f
@@ -159,13 +166,14 @@ theorem hardy_coeff_pos (a : Fin 4 → ℕ) :
       < 4 * Nat.multinomial Finset.univ (fun i => 2 * a i) :=
   multinomial_lt_four_mul_multinomial_two_mul _ _
 
-/-! ### The character sum behind equation (12)
+/-! ### A supporting character identity
 
-The note's coefficient formula for `log R` rests on the claim that summing the
-character `ε ↦ ε ^ α` over the eight sign vectors of even weight gives `8` when
-the entries of `α` all share a parity, and `0` otherwise. The content is the
-unconstrained sum below; the even-weight version follows by averaging against
-the product character. -/
+Equation (12) of the note extracts the coefficients of `log R` using a sum of
+`ε ↦ ε ^ α` over the **eight** sign vectors of even weight. What is proved here
+is the **unconstrained** sum over all `2 ^ n` sign vectors. The even-weight
+version follows from it by averaging against the product character, but that
+averaging step, and the coefficient extraction for `log R` itself, are NOT
+formalized here. So this is an input to equation (12), not equation (12). -/
 
 /-- The sign attached to a Boolean coordinate. -/
 def sgn (b : Bool) : ℤ := if b then -1 else 1
@@ -206,7 +214,8 @@ theorem sum_sign_character (n : ℕ) (α : Fin n → ℕ) :
     rw [(Nat.not_even_iff_odd.mp hj).neg_one_pow]
     ring
 
-/-- Specialized to the four coordinates of the Hardy quadruple. -/
+/-- Specialized to four coordinates. Note this is the full 16-term sign sum,
+not the 8-term even-weight sum appearing in equation (12). -/
 theorem sum_sign_character_four (α : Fin 4 → ℕ) :
     (∑ ε : Fin 4 → Bool, ∏ j, sgn (ε j) ^ α j)
       = if ∀ j, Even (α j) then 16 else 0 := by
diff --git a/verification/hardy-sign/README.md b/verification/hardy-sign/README.md
index b781703..9d23616 100644
--- a/verification/hardy-sign/README.md
+++ b/verification/hardy-sign/README.md
@@ -46,16 +46,22 @@ the proof's use of Bui-Hall Theorem 3 as an external published input.
 
 ## 3. Machine-checked fragment
 
-`OrchardMath/Millennium/HardySign.lean` proves in Lean, from Mathlib only, the
-two combinatorial pillars of section 3:
-
-- **Equation (13)**, the argument's only genuine inequality:
-  `multinomial a < 4 * multinomial (2a)`, for any finite index set. The route
-  replaces the note's letter-duplication injection with the exact identity
+`OrchardMath/Millennium/HardySign.lean` proves in Lean, from Mathlib only, two
+ingredients of section 3. Their scope is narrower than the equations they feed,
+and the distinction matters:
+
+- **The cleared numerator inequality behind equation (13)**, which is the
+  argument's only genuine inequality: `multinomial a < 4 * multinomial (2a)`,
+  for any finite index set. The route replaces the note's letter-duplication
+  injection with the exact identity
   `(prod_i oddProd (f i)) * multinomial (2f) = multinomial f * oddProd (sum f)`,
   reducing the claim to supermultiplicativity of the odd-number product.
-- **Equation (12)**, the sign-character sum: summing `eps^alpha` over all sign
-  vectors gives `2^n` when every exponent is even and `0` otherwise.
+  Identifying this quantity with a coefficient of `F` is **not** formalized.
+- **A supporting character identity for equation (12)**: summing `eps^alpha`
+  over all `2^n` sign vectors gives `2^n` when every exponent is even and `0`
+  otherwise. Equation (12) needs the **eight** even-weight sign vectors, not all
+  sixteen; that averaging step, and the coefficient extraction for `log R`, are
+  **not** formalized. This is an input to equation (12), not equation (12).
 
 `OrchardMath/Millennium/HardySignAudit.lean` restates each result externally and
 prints transitive axiom use. Every declaration depends only on `propext`,
@@ -67,6 +73,10 @@ Build: `lake build OrchardMath.Millennium.HardySignAudit`.
 
 - The integral reduction of section 1 is checked only to degree 12, not proved
   formally. Formalizing it needs measure theory well beyond this fragment.
+- Section 2, the generating-function identities (8), (9) and (10), is not
+  checked here at all.
+- The two Lean results are ingredients of equations (12) and (13), not those
+  equations. No generating-function coefficient identity is formalized.
 - The generating-function step, `(1-Q)R = exp F` and coefficientwise
   positivity of `exp F`, is not formalized. Mathlib has `exp` and `log` for
   univariate power series only, so this needs multivariate infrastructure that
diff --git a/verification/hardy-sign/verify_from_source.py b/verification/hardy-sign/verify_from_source.py
index 85da68a..38d2629 100644
--- a/verification/hardy-sign/verify_from_source.py
+++ b/verification/hardy-sign/verify_from_source.py
@@ -143,9 +143,19 @@ def predicted_sign(k, l, m, n):
 
 
 def source_says_negative(k, l, m, n):
-    """Conjecture 1 condition: negative exactly when |i^k+i^l+i^m+i^n| = 2."""
-    z = sum(complex(0, 1) ** e for e in (k, l, m, n))
-    return abs(abs(z) - 2.0) < 1e-9
+    """Conjecture 1 condition: negative exactly when |i^k+i^l+i^m+i^n| = 2.
+
+    Exact integer test. i^e cycles through (1,0), (0,1), (-1,0), (0,-1) as
+    (real, imag), so the sum is a Gaussian integer and |sum| = 2 is the
+    integer condition re^2 + im^2 == 4. No floating point, no tolerance.
+    """
+    table = ((1, 0), (0, 1), (-1, 0), (0, -1))
+    re = im = 0
+    for e in (k, l, m, n):
+        a, b = table[e % 4]
+        re += a
+        im += b
+    return re * re + im * im == 4
 
 
 # ------------------------------------------------------------------- the runs
@@ -209,6 +219,12 @@ def main():
         if sum(a) % 2 == 0 and sum(a) <= MAXDEG:
             print(f"   HARDY{a} = {hardy_from_source(*a)}")
 
+    failures = len(red_fail) + len(sign_fail) + len(equiv_fail)
+    print()
+    print("RESULT:", "ALL CHECKS PASSED" if failures == 0
+          else f"{failures} FAILURE(S)")
+    return 1 if failures else 0
+
 
 if __name__ == "__main__":
-    main()
+    raise SystemExit(main())