fcc-verify pass two: pins, integration vectors, claim algebra

PINS.json pins the foreign trees the suite is derived against:
axioma-spec 9a20f026 (registry of record, DVEC-001 v1.4) and
exp1-runner 4d2bf333 (integration-vector writer). The repo's own head
is deliberately unpinned; the head of this commit is the
verifier_commit harvested into the EXP-1 C at freeze, and a pin that
certifies the suite must postdate it.

Runner-replay integration vectors iv01 (UPHELD) and iv02 (REFUTED),
written by exp1-runner chain.py via the committed
tools/gen_integration.py, gated by SHA-256 manifest plus replay and
determinism since CI cannot run the foreign writer. They confirm the
verifier's independently reimplemented reader consumes the writer of
record byte-for-byte; the twenty-six hand-derived vectors remain the
primary conviction evidence.

F-INC-1 folded: a trial success that is not a JSON boolean is
INVALID-ATTEMPT (FABRICATION). Pass one scored success by Python
truthiness; a Tier B reimplementation has no licensed coercion for a
non-boolean, so two conformant verifiers could disagree on the same
bytes. Gate, not pin. Vector v26.

FCC-001-CLAIM-ALGEBRA-v0.1.md committed beside the spec: every
probabilistic guarantee derived from stated assumptions, the
assumption register as the proof boundary. A Tier B refuter needs the
proofs next to the text they implement.

Python 3 stdlib only; Fraction in the verdict path, no float in any
verdict decision.

AGPL-3.0.

Author: williamofai

PINS.json

@@ -0,0 +1,18 @@
+{
+  "calculus_version": "FCC-001-v0.4.1",
+  "registry_version": "DVEC-001 v1.4",
+  "pinned": [
+    {
+      "name": "axioma-spec",
+      "role": "registry of record (DVEC-001 v1.4)",
+      "head": "9a20f026a3ad3de68a758783891623f2fa2f6de4",
+      "pinned": "2026-07-04"
+    },
+    {
+      "name": "exp1-runner",
+      "role": "integration-vector writer",
+      "head": "4d2bf333f242593687cf379e8c19319fdcc5a19e",
+      "pinned": "2026-07-04"
+    }
+  ]
+}

README.md

@@ -87,10 +87,34 @@ harness, re-deriving per-episode outcomes from transcripts, are named in the
     fccverify/exact.py     exact Clopper-Pearson by binomial tail sums
     fccverify/verdict.py   the FCC-001 6.2 verdict pipeline
     fccverify/cli.py       command-line entry point
-    spec/                  FCC-001-SPEC-v0.4.1.md, the specification of record
-    golden/                committed vectors, one per verdict and cause
+    spec/                  FCC-001-SPEC-v0.4.1.md, the specification of
+                           record, and FCC-001-CLAIM-ALGEBRA-v0.1.md, the
+                           formal derivations behind it
+    golden/                committed vectors, one per verdict and cause,
+                           plus the runner-written integration pairs and
+                           their hash manifest
+    tools/                 gen_integration.py, the integration-vector
+                           writer harness (runs beside an exp1-runner
+                           checkout, not in CI)
+    PINS.json              foreign trees this suite was derived against
     VECTORS.md             hand derivation of every vector
 
+## Pass two
+
+Pass one built the verdict program and the hand-derived golden vectors.
+Pass two pins the foreign trees (PINS.json: axioma-spec for the registry of
+record, exp1-runner for the writer), commits the claim algebra beside the
+spec so a Tier B refuter has the proofs next to the text they implement,
+and adds the runner-replay integration vectors iv01 and iv02, written by
+the actual exp1-runner chain.py and gated by SHA-256 manifest since CI
+cannot run the foreign writer. The conviction hierarchy is unchanged: the
+hand-derived vectors are the primary evidence, derived from the
+specification in VECTORS.md; the integration pairs confirm the verifier's
+independently reimplemented reader consumes the writer of record
+byte-for-byte, nothing more. The head of the commit that closes pass two is
+the verifier_commit harvested into the EXP-1 C at freeze, which is why it
+cannot be pinned here: the pin certifies the suite, so it must postdate it.
+
 ## Licence
 
 AGPL-3.0. The verifier is meant to be cloned, read, and run by adversaries;

VECTORS.md

@@ -188,6 +188,15 @@ delta <= 0 (already excluded by positivity) would make NULL unreachable, the
 opposite degeneracy. Range constraints are enumerated per field in the shape
 gate, R1's table argument applied to ranges. INVALID-CLAIM (MALFORMED).
 
+**v26 FABRICATION, observation shape (F-INC-1).** Twelve trial records whose
+success is the JSON string "yes". Pass one scored success by Python
+truthiness, so the pair adjudicated REFUTED with k = 12, demonstrated against
+the signed pass-one tree; the JSON number 1 behaved identically. A Tier B
+reimplementation has no licensed coercion for a non-boolean, so two
+conformant verifiers could disagree on the same bytes. The gate, not the
+coercion, is pinned: success must be a JSON boolean, else INVALID-ATTEMPT
+(FABRICATION). Genuine booleans adjudicate unchanged.
+
 ---
 
 ## Coverage
@@ -199,15 +208,41 @@ gate, R1's table argument applied to ranges. INVALID-CLAIM (MALFORMED).
                      v11/v12/v13/v20/v22/v23/v25 (MALFORMED)
     INVALID-ATTEMPT  v14 (UNREGISTERED), v15 (INCOMPLETE),
                      v16/v21 (SNAPSHOT-MISMATCH),
-                     v17/v18/v19/v24 (FABRICATION)
+                     v17/v18/v19/v24/v26 (FABRICATION)
 
 Both REFUTED polarities present for NULL (v02, v03). Both THREAT signs present
 (v05 to v09) with the opposite-side and band-overlap disjointness cases that the
 one-definition rule requires. The boundary control (v04) fixes the tie-break.
 The committed-parameter perimeter is covered on both sides of N' (v15 below,
 v19 above), on canonicality (v20), on multiplicity for both chains (v22
 claimant, the single-genesis rule refuter), on type consumability for both
-chains (v23, v24), and on the range degeneracies that make a claim unrefutable
-or unreachable by construction (v25). The four INVALID-ATTEMPT causes reachable
-without the harness are covered; BEACON-VIOLATION content stays deferred, named
-in the verdict record, and lands with the harness pin.
+chains (v23, v24), on the range degeneracies that make a claim unrefutable
+or unreachable by construction (v25), and on evidence shape (v26). The four
+INVALID-ATTEMPT causes reachable without the harness are covered;
+BEACON-VIOLATION content stays deferred, named in the verdict record, and
+lands with the harness pin.
+
+---
+
+## Integration vectors
+
+Written by exp1-runner chain.py at the RUNNER_HEAD pinned in PINS.json, via
+the committed tools/gen_integration.py. They confirm integration: the
+verifier's own reader (reimplemented from the frame format of record,
+sharing no code with the writer) consumes the writer of record
+byte-for-byte. They do not carry the conviction; the hand-derived v-series
+above remains the primary evidence. CI cannot regenerate them (foreign
+writer), so the gate is the SHA-256 manifest in
+golden/integration-manifest.json plus verdict replay and byte-determinism,
+enforced by tests/test_integration.py.
+
+**iv01 UPHELD.** NULL claim, standing parameters (delta = 5/100, alpha' =
+1/100); refuter k = 6, n = 12, N' = 12. The v01 arithmetic exactly: CI' at
+alpha' straddles the band, not disjoint, UPHELD. The claimant chain also
+carries an AX:FCC:TS:v1 record between the state frame and C, exercising the
+reader's tolerance of registered non-C tags on a claimant chain, a surface
+no hand vector touches.
+
+**iv02 REFUTED.** Same claim; refuter k = 12, n = 12, N' = 12. The v02
+arithmetic exactly: p_lo solves p^12 = 0.005, p_lo = 0.6431 > 0.525, CI'
+entirely above the band, disjoint, REFUTED.

fccverify/verdict.py

@@ -304,6 +304,10 @@ def _stage1_claim(frames, v):
 # {claim_c_hash, claim_alpha_prime, k, n} and returns either
 # (True, pass_detail) or (False, cause, fail_detail). Adding a committed
 # parameter means adding a row; there is no second place to forget.
+#
+# Judges validate integer operands through _is_int, never bare
+# isinstance(_, int): Python booleans are int subclasses, and a bare
+# isinstance would let a JSON true in as 1 (A3).
 
 def _judge_binds_claim(reg, ctx):
     """The genesis must commit the hash of the C it attacks (FCC-7.1)."""
@@ -427,6 +431,18 @@ def _stage2_attempt(refuter_frames, claim_c_hash, claim_alpha_prime, v):
                        "attempt.observation_wellformed", "fail",
                        "an AX:OBS:v1 trial record lacks a success field")
             return None
+        # F-INC-1: success must be a JSON boolean. Truthiness coercion would
+        # import Python semantics into the calculus; a Tier B
+        # reimplementation has no licensed coercion for a non-boolean, so
+        # two conformant verifiers could disagree. Bare isinstance(_, bool)
+        # is total and correct here; do not route this through _is_int,
+        # whose job is the opposite exclusion (A3).
+        if not isinstance(rec["success"], bool):
+            v.terminal(INVALID_ATTEMPT, "FABRICATION",
+                       "attempt.observation_wellformed", "fail",
+                       "an AX:OBS:v1 trial record's success is not a JSON "
+                       "boolean")
+            return None
         n += 1
         if rec["success"]:
             k += 1

golden/integration-manifest.json

@@ -0,0 +1,22 @@
+[
+  {
+    "cause": null,
+    "expected": "UPHELD",
+    "name": "iv01_integration_upheld.bin",
+    "note": "runner-written pair, k=6 n=12, v01 arithmetic; claimant chain carries an AX:FCC:TS:v1 record",
+    "refuter": "iv01_integration_upheld.refuter.bin",
+    "refuter_sha256": "f9e8ef1a000486cb05af6e9c4afd3bfa2ff32115d95cc4b4f98ec5ce69805f58",
+    "sha256": "559341efe8b749f72008d18081aed8446ac8f9bbf0e846574b75d03ab4186167",
+    "written_by": "exp1-runner chain.py at the RUNNER_HEAD pinned in PINS.json"
+  },
+  {
+    "cause": null,
+    "expected": "REFUTED",
+    "name": "iv02_integration_refuted.bin",
+    "note": "runner-written pair, k=12 n=12, v02 arithmetic",
+    "refuter": "iv02_integration_refuted.refuter.bin",
+    "refuter_sha256": "7e02356c2aeb008a78d172d19a85352425d90ec7bae1c3e6cae1f91e756fe173",
+    "sha256": "3698a006dd0be08a183d84b2eaa5c140443366cd9c7bfec1444200e8180e9923",
+    "written_by": "exp1-runner chain.py at the RUNNER_HEAD pinned in PINS.json"
+  }
+]

golden/iv01_integration_upheld.bin

@@ -248,5 +248,15 @@
     "name": "v25_invalid_claim_delta_range.bin",
     "note": "delta=150/100 not strictly below 1: band swallows [-1, 1]",
     "pass": true
+  },
+  {
+    "cause": "FABRICATION",
+    "expected": "INVALID-ATTEMPT",
+    "got": "INVALID-ATTEMPT",
+    "got_cause": "FABRICATION",
+    "has_refuter": true,
+    "name": "v26_invalid_attempt_obs_shape.bin",
+    "note": "trial success is the string 'yes', not a JSON boolean",
+    "pass": true
   }
 ]