From 5b3cc75d1585a00ee1420a556af5b77748c418fa Mon Sep 17 00:00:00 2001
From: Dylan Roy <249851642+d6g8k5htny-coder@users.noreply.github.com>
Date: Thu, 22 Oct 2026 23:40:04 -0500
Subject: [PATCH] VERIFIER-C7-01: re-pin C299 negative matcher to observed C7
 diagnostic (L21:2, typed eventually binder)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Tighten only: position pinned from any \d+:\d+ to 21:2; conclusion re-pinned to C7 rendering
'(∀ᶠ (w : E d) in 𝓝 0, ...)'. Fixture moved 23:2 -> 21:2 with three added rejection cases
(old 23:2, off-by-one col 21:3, old C6 binder). Forbidden list, error count, expression
pins and require_final_predicates stop unchanged. credit 0; OBL OPEN.
---
 frontiers/critical_ridge_20261020/c299_hosted_verify.py  | 6 +++---
 .../critical_ridge_20261020/test_c299_hosted_verify.py   | 9 ++++++---
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/frontiers/critical_ridge_20261020/c299_hosted_verify.py b/frontiers/critical_ridge_20261020/c299_hosted_verify.py
index 521bd0175..b8a870153 100644
--- a/frontiers/critical_ridge_20261020/c299_hosted_verify.py
+++ b/frontiers/critical_ridge_20261020/c299_hosted_verify.py
@@ -212,7 +212,7 @@ def validate_negative_draft(name, returncode, output):
     if (returncode != 1 or output.count('error:') != 1
             or any(x in flat.lower() for x in forbidden)):
         raise RuntimeError('negative control failed for an unrelated reason')
-    pattern = (r'\A[^\n]*' + re.escape(name) + r'\.lean:\d+:\d+: error: Type mismatch\s*\n'
+    pattern = (r'\A[^\n]*' + re.escape(name) + r'\.lean:21:2: error: Type mismatch\s*\n'
                r'(?P<expression>.*?)\nhas type\s*\n(?P<actual>.*?)'
                r'\nbut is expected to have type\s*\n(?P<expected>.*?)\s*\Z')
     match = re.fullmatch(pattern, output.strip(), flags=re.S)
@@ -234,9 +234,9 @@ def validate_negative_draft(name, returncode, output):
         premise = r'\(∀ v ∈ V, v ≠ 0 → hessian d f p v v < 0\)'
     if not re.fullmatch(premise + r' → ' + re.escape(expected), actual):
         raise RuntimeError('actual type is not the omitted premise followed by the expected conclusion')
-    # Fixed candidate-2 binder names and all four same-ridge conclusion fields.
+    # Fixed C7 binder rendering (observed at negative-project L21:2) and all four same-ridge conclusion fields.
     conclusion = (r'∃ r, r 0 = 0 ∧ ContDiffAt ℝ 2 r 0 ∧ '
-                  r'\(∀ᶠ w in 𝓝 0, ∀ \(z : ↥V\), \(fderiv ℝ f \(p \+ w \+ ↑\(r w\)\)\) ↑z = 0\) ∧ '
+                  r'\(∀ᶠ \(w : E d\) in 𝓝 0, ∀ \(z : ↥V\), \(fderiv ℝ f \(p \+ w \+ ↑\(r w\)\)\) ↑z = 0\) ∧ '
                   r'∀ \(w : E d\) \(z : ↥V\), hessian d f p \(w \+ ↑\(\(fderiv ℝ r 0\) w\)\) ↑z = 0')
     if not re.fullmatch(conclusion, expected):
         raise RuntimeError('expected conclusion does not match all four candidate ridge fields')
diff --git a/frontiers/critical_ridge_20261020/test_c299_hosted_verify.py b/frontiers/critical_ridge_20261020/test_c299_hosted_verify.py
index 4892e513e..4968ecbc8 100644
--- a/frontiers/critical_ridge_20261020/test_c299_hosted_verify.py
+++ b/frontiers/critical_ridge_20261020/test_c299_hosted_verify.py
@@ -180,10 +180,10 @@ def test_source_preflight_can_collect_before_final_predicate_qualification(self)
     def test_inactive_draft_negative_sections_reject_forged_fields(self):
         """Section/token-only matching would accept unrelated existential fields."""
         v = self.verifier()
-        # Synthetic prospective rendering only; no actual Lean diagnostic observed.
+        # Pinned to the C7 rendering observed locally (Lean v4.34.1) at L21:2.
         conclusion = (
             '∃ r, r 0 = 0 ∧ ContDiffAt ℝ 2 r 0 ∧ '
-            '(∀ᶠ w in 𝓝 0, ∀ (z : ↥V), (fderiv ℝ f (p + w + ↑(r w))) ↑z = 0) ∧ '
+            '(∀ᶠ (w : E d) in 𝓝 0, ∀ (z : ↥V), (fderiv ℝ f (p + w + ↑(r w))) ↑z = 0) ∧ '
             '∀ (w : E d) (z : ↥V), hessian d f p (w + ↑((fderiv ℝ r 0) w)) ↑z = 0')
         target = 'TorusCriticalRidge.exists_negative_partial_gradient_ridge'
         for name, expression, premise in (
@@ -193,7 +193,7 @@ def test_inactive_draft_negative_sections_reject_forged_fields(self):
                 ('WithoutNegativeDefiniteness',
                  target + ' f p V hsmooth hcritical',
                  '(∀ v ∈ V, v ≠ 0 → hessian d f p v v < 0)')):
-            proper = (name + '.lean:23:2: error: Type mismatch\n  ' + expression
+            proper = (name + '.lean:21:2: error: Type mismatch\n  ' + expression
                       + '\nhas type\n  ' + premise + ' → ' + conclusion
                       + '\nbut is expected to have type\n  ' + conclusion + '\n')
             result = v.validate_negative_draft(name, 1, proper)
@@ -202,6 +202,9 @@ def test_inactive_draft_negative_sections_reject_forged_fields(self):
             for code, bad in (
                     (0, proper), (-9, proper),
                     (1, proper.replace(name + '.lean', 'Other.lean')),
+                    (1, proper.replace('.lean:21:2:', '.lean:23:2:')),
+                    (1, proper.replace('.lean:21:2:', '.lean:21:3:')),
+                    (1, proper.replace('(∀ᶠ (w : E d) in', '(∀ᶠ w in')),
                     (1, proper.replace('ContDiffAt ℝ 2 r 0', 'True')),
                     (1, proper.replace('fderiv ℝ f', 'fderiv ℝ other')),
                     (1, proper.replace(premise + ' → ', 'Continuous f → ', 1)),