Update card to modular Coq library + add extracted certifier

README.md

@@ -40,9 +40,11 @@ holds on its dense output. Under that invariant, greedy NMS is
 provably equivalent to a sort + threshold filter on the score axis.
 The deployment graph can drop NMS at zero AP cost.
 
-## Theorem
+## Theorems
 
-The companion Rocq library proves
+The companion Rocq library is structured into four modules
+(`Core.v`, `Bridge.v`, `Probability.v`, `Pipeline.v`). The keystone
+collapse theorem in `Core.v` is
 
 ```
 Theorem nms_collapse_onepeak :
@@ -52,8 +54,32 @@ Theorem nms_collapse_onepeak :
 ```
 
 instantiated for box-NMS, soft-NMS, mask-NMS, heatmap local-NMS, and
-DETR-style filtering. All proofs closed in Rocq 9 with no admits and
-no axioms beyond Stdlib's standard `R` foundations.
+DETR-style filtering.
+
+The bridge from a Lipschitz score head to `Separated` is in `Bridge.v`
+(`lipschitz_bridge_substantive`, `SepRespectingHead`). Architectural
+discharges of the bridge precondition appear in `Pipeline.v`:
+
+```
+Theorem detr_equilibrium_yields_separated  (* DETR / set-prediction *)
+Theorem anchor_stride_yields_separated     (* FCOS / RetinaNet / ATSS *)
+```
+
+The training-side chain from SGD to the Separated locus is closed end
+to end in `Pipeline.v`:
+
+```
+Theorem squared_hinge_sgd_pl_convergence
+Theorem L_separated_sq_zero_iff_separated_general
+Theorem real_training_to_collapse
+```
+
+PAC generalization from a finite training sample is in `Probability.v`
+via Hoeffding's lemma (`hoeffding_lemma_symmetric`,
+`hoeffding_iid_finite_class_one_sided`).
+
+All proofs closed in Rocq 9 with no admits and no axioms beyond
+Stdlib's standard `R` foundations.
 
 ## COCO val2017 mAP
 
@@ -146,9 +172,34 @@ python experiments/coco_eval.py \
 
 Reports both standard and NMS-free AP on COCO val2017.
 
+## Certification
+
+`nms_cert.ml` is the OCaml extraction of the decidable certifier
+(`Separated_check`, `Separated_dec`, `sep_certify_finite`) from the
+Rocq library. `nms_cert_main.ml` is a small CLI driver: detections in,
+`CERTIFIED <slack>` or `REJECTED` out. Build:
+
+```
+ocamlfind ocamlopt nms_cert.ml nms_cert_main.ml -o nms_cert
+```
+
+Usage:
+
+```
+./nms_cert TAU THETA SLACK < detections.txt
+```
+
+Each input line is whitespace-separated `score x1 y1 x2 y2` with
+integer scores and integer bounding-box pixels. `CERTIFIED` means
+the corresponding `Separated` predicate holds on the input list at
+that slack — by `nms_collapse_onepeak`, NMS is then equivalent to a
+threshold filter on the same list.
+
 ## Files
 
 - `fcos_certified.safetensors` — model weights (FCOS-ResNet50-FPN, 319 tensors).
+- `nms_cert.ml` — extracted certifier (Separated_check, Separated_dec, sep_certify_finite).
+- `nms_cert_main.ml` — CLI driver around the extracted certifier.
 - `README.md` — this card.
 
 ## Citation