spec/COVERAGE_MATRIX.md

Coverage Matrix — PROPERTIES.md ↔ harness

Target commit: 194e588 (pure-J Foundry F1).
Sources: spec/PROPERTIES.md (56 numbered properties); verify/PROPERTY_MAP.md (harness Primary/Related + measured results); verify/INVENTORY.md (non-mathematical / ignored note).
Measured log: logs/run-20261007-061701.log — PROPERTY_MAP reports 8 PASS / 1 FAIL / 0 BLOCKED (not 9/9).
No invented numbers. Status definitions exactly as Spec brief.

Status	Definition
covered	Listed in PROPERTY_MAP as Primary # or Related # and measured PASS
partial	Listed as Primary/Related but measured FAIL; or harness works around Core (e.g. recurrence via rec_step not rec_run); or emission / CSL / AceCert / WORM props called out as non-mathematical / ignored by harness
untested	Not mentioned in PROPERTY_MAP Primary or Related columns (and not in the ignored 47–56 band)

---

Prop	Short name	Status	Evidence	Notes
1	Goldilocks prime (decimal)	covered	goldilocks_add (Related)	PASS in PROPERTY_MAP
2	Goldilocks prime (hex / named constant)	covered	goldilocks_add (Related)	PASS in PROPERTY_MAP
3	Field elements are u64 reduced mod p	covered	goldilocks_add (Related)	PASS in PROPERTY_MAP
4	Elem construction reduces	untested	none	Not in PROPERTY_MAP Primary/Related
5	Congruence (2^{64} \equiv 2^{32}-1 \pmod{p})	covered	goldilocks_mul (Related 5–11)	PASS in PROPERTY_MAP
6	Fold constant EPSILON	covered	goldilocks_mul (Related 5–11)	PASS in PROPERTY_MAP
7	128-bit product split	covered	goldilocks_mul (Related 5–11)	PASS in PROPERTY_MAP
8	hi split into 32-bit halves	covered	goldilocks_mul (Related 5–11)	PASS in PROPERTY_MAP
9	Reduction identity (fold)	covered	goldilocks_mul (Related 5–11)	PASS in PROPERTY_MAP
10	Underflow handling on fold	covered	goldilocks_mul (Related 5–11)	PASS in PROPERTY_MAP
11	Final conditional reduction after fold	covered	goldilocks_mul (Related 5–11)	PASS in PROPERTY_MAP
12	Single-limb reduce	untested	none	Not in PROPERTY_MAP Primary/Related
13	Addition mod p	covered	goldilocks_add (Primary)	PASS in PROPERTY_MAP; verify/tests/goldilocks.ijs
14	Subtraction mod p	covered	goldilocks_sub (Primary)	PASS in PROPERTY_MAP; verify/tests/goldilocks.ijs
15	Multiplication via mulmod	covered	goldilocks_mul (Primary)	PASS in PROPERTY_MAP; verify/tests/goldilocks.ijs
16	Fermat inverse	partial	goldilocks_inv (Primary)	covered-but-FAIL — PROPERTY_MAP: 42*fp_inv(42) → 11152786313141180820 (not 1); log run-20261007-061701
17	Binary exponentiation	partial	goldilocks_inv (Related)	Listed with prop 16; same measured FAIL
18	Batch add/mul	untested	none	Not in PROPERTY_MAP Primary/Related
19	K_MAX	untested	none	Not in PROPERTY_MAP Primary/Related
20	MAX_DRIFT	untested	none	Not in PROPERTY_MAP Primary/Related
21	PIRTM_MAGIC	untested	none	Not in PROPERTY_MAP Primary/Related
22	PHI	untested	none	Not in PROPERTY_MAP Primary/Related; see Gaps
23	P_64 — first 64 primes	untested	none	Not in PROPERTY_MAP Primary/Related
24	GENESIS_HASH_SIZE	untested	none	Not in PROPERTY_MAP Primary/Related
25	Tier epsilons (contraction margins)	untested	none	Not in PROPERTY_MAP Primary/Related
26	PMat entry shape	covered	pmat_insert (Related)	PASS in PROPERTY_MAP
27	Insert domain checks	covered	pmat_insert (Primary)	PASS in PROPERTY_MAP; verify/tests/pmat.ijs
28	Grading condition (stated)	untested	none	Gap: validate_grading stub; not in harness map
29	Conservation theorem	covered	pmat_conservation (Primary)	PASS in PROPERTY_MAP; verify/tests/pmat.ijs
30	Composition preserves grading (stated)	untested	none	Not in PROPERTY_MAP Primary/Related
31	Compose monomial accumulation rule (as coded)	untested	none	Not in PROPERTY_MAP Primary/Related; see Gaps
32	Frobenius norm of PMat	untested	none	Not in PROPERTY_MAP Primary/Related
33	Gershgorin disk bound	covered	spectral_contractive, spectral_expansive (Related)	PASS in PROPERTY_MAP
34	Contractive test (Gershgorin)	covered	spectral_contractive, spectral_expansive (Related)	PASS in PROPERTY_MAP
35	Power iteration (Rayleigh)	untested	none	Not in PROPERTY_MAP Primary/Related
36	Contractive test (power iteration)	untested	none	Not in PROPERTY_MAP Primary/Related
37	Analyze fallback policy	covered	spectral_contractive, spectral_expansive (Related)	PASS in PROPERTY_MAP
38	Tested contractive / expansive examples	covered	spectral_contractive, spectral_expansive (Primary)	PASS in PROPERTY_MAP; verify/tests/spectral.ijs
39	Recurrence equation	partial	recurrence_converges (Related 39–45)	PASS measured, but PROPERTY_MAP notes harness loop via synth_weights+rec_step; Core rec_run still flattens StepInfo
40	Contraction condition	partial	recurrence_converges (Related 39–45)	Same workaround note as prop 39
41	Unique fixed-point guarantee (narrative)	partial	recurrence_converges (Related 39–45)	Same workaround note as prop 39
42	q estimate in step (as coded)	partial	recurrence_converges (Related 39–45)	Same workaround note as prop 39
43	Soft projection	partial	recurrence_converges (Related 39–45)	Same workaround note as prop 39
44	Weight budget split	partial	recurrence_converges (Related 39–45)	Same workaround note as prop 39
45	Projector	partial	recurrence_converges (Related 39–45)	Same workaround note as prop 39
46	Residual	partial	recurrence_converges (Primary)	PASS measured via rec_step loop; PROPERTY_MAP: Core rec_run packing still broken (x_next ; info flattens)
47	WORM / seal chain invariant (system-level)	partial	none (ignored)	INVENTORY: props 47–56 adjacent / gate-WORM theater, not in harness
48	Emission Suppress	partial	none (ignored)	INVENTORY non-mathematical / ignored by harness
49	Emission Attenuate scale	partial	none (ignored)	INVENTORY non-mathematical / ignored by harness
50	CSL neutrality	partial	none (ignored)	INVENTORY non-mathematical / ignored by harness
51	CSL beneficence	partial	none (ignored)	INVENTORY non-mathematical / ignored by harness
52	CSL commutation	partial	none (ignored)	INVENTORY non-mathematical / ignored by harness
53	AceCertificate safety margin	partial	none (ignored)	INVENTORY non-mathematical / ignored by harness
54	AceCertificate tail bound	partial	none (ignored)	INVENTORY non-mathematical / ignored by harness
55	Guardian spectral legality	partial	none (ignored)	INVENTORY non-mathematical / ignored by harness
56	Consensus / false-positive bound (narrative)	partial	none (ignored)	INVENTORY non-mathematical / ignored by harness

---

Summary counts

Status	Count
covered	20
partial	20
untested	16
Total	56

Partial breakdown (for handoff)

Reason	Props	Count
Measured FAIL (goldilocks_inv)	16, 17	2
Harness workaround (rec_step / rec_run packing)	39–46	8
Ignored / non-mathematical (INVENTORY 47–56)	47–56	10

Harness measured (PROPERTY_MAP / log run-20261007-061701)

Result	Count	Detail
PASS	8	goldilocks_add, goldilocks_mul, goldilocks_sub, pmat_insert, pmat_conservation, spectral_contractive, spectral_expansive, recurrence_converges
FAIL	1	goldilocks_inv / prop 16
BLOCKED	0	—

Cite: verify/PROPERTY_MAP.md Summary counts; verify/INVENTORY.md Math count line.