[luisleo526]

The public scoreboard may list only some markets in pairs. Add an optional
otherMarkets object to the facts schema that carries the counts of every
other market and nothing that names one: twelve integer members (lanes,
markets, additional timeframes, probe counts, graded, tier summaries, engine
errors) and the tier counts, with additionalProperties false at both levels.

The validator checks the same equations over the listed pairs plus the
aggregate when it is present (lane, market and timeframe dimensions, count,
tier and scope sums, the aggregate's own tally and bounds). When it is absent
the validation is unchanged, so every published facts file keeps validating.
hardLane stays the first listed pair with hard probes.

The frozen description fixture no longer names the non-listed markets; its
numbers are the old lane rows summed into the aggregate. The receipt tests now
derive the facts digest from the fixture bytes instead of pinning the old file.
Tests cover the aggregate in the validator, release binding and retention,
cards, descriptions, fan-out and receipts, with exact diagnostics for every
refusal. facts/facts.json is not changed.

🤖 Generated with Claude Code

[graphify-labs]

Graphify reviewed this change.

No issues found by static checks — no coupling regressions or blocking issues in the code graph. That is not the same as safe to merge: see what was not checked.

Not checked: tests were not run; formal verification proved 0 of 1 changed function(s) (1 not verified).

Formal verification. PR-changed functions: 0/1 verified (0 proven, 0 may-equivalent, 0 distinguished) · 1 not verified (1 vacuous).

Not verified on this run: scoreboard\_invariants (vacuous: never exercised).

---

Graphify review — findings

Adds an optional scoreboard.otherMarkets aggregate to the facts schema, so markets outside the named pairs are published as counts and tiers only, with no symbol, venue or name. scoreboard_invariants folds that aggregate into the lane, market, timeframe, probe and tier totals and still checks scope sums, but the lane and market counts it accepts are only loosely tied to the probes it holds. hardLane keeps naming just the first named pair with hard probes, so it can be null while otherMarkets.hardProbes is nonzero, and the README and release-chain docs spell that out.

Review partial — this diff was larger than one review pass covers, so later files were not reviewed; some findings may be missing.

Analysis details — impact, health, verification

Impact & health

Graphify review

Impact — 750 functions depend on the 692 functions this change touches.

Health — this change adds coupling hotspots:

• worse: validate_facts() — 15 callers, 6 callees
• new: required — 0 callers, 12 callees

Verification — 750 functions in the blast radius were not formally verified this run (proofs are advisory here).

Gate & verification

graphify gate

PASS — objectively clean (no health regressions, tests not run — proofs not run this pass (advisory)). Grounded, not self-assessed.

Advisory (not blocking):

• verification_scope: 750 function(s) in the blast radius were not formally verified this run

Docs that may be stale (advisory)

• tools/release-dry-run/README.md § Historical workflow replay (lines 38-101): references changed symbols api
• tools/release-dry-run/README.md § Checking the checks (lines 160-188): references changed symbols file

Formal verification

Could not verify: Could not verify scoreboard\_invariants.

The verifier did not have enough to check scoreboard\_invariants, so it is saying so rather than guessing. No false assurance is the whole point.

Guarantee: No guarantee either way, this is an honest abstention, not a pass.

Note: Reason: not verifiable: all 60 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)

· 1 grounded finding(s) anchored inline below; 1 more finding(s) on lines outside this diff (see the check run).

[graphify-labs]

⚠️ Health regression — required

fans out to 12 callees (efferent coupling).

Grounded coupling-delta finding (deterministic), not an LLM guess.