Calibrate the reference-occurrence census before the corpus run: its coverage is not unproven, it is refuted

[gunbai-bot]

The candidate reference-occurrence producer's coverage of the family roster was recorded as
unestablished. It is now refuted, by execution, on a hand-authored two-module subject.

Two claims this PR made in an earlier revision are refuted by its own later measurements

Recorded first rather than quietly edited out, because a stepping-stone PR carrying known-false
current claims is a false evidence authority, and a later PR cannot retroactively make it truthful.

1. "type annotation and generic type argument both emit TypeOccurrence, converged" — false. A
   type named as a generic argument emits no occurrence at all. The row that made it look
   observed came from somewhere else in the fixture entirely (below).
2. "a name inside an import statement's brace list produces no reference occurrence" — false. The
   first name in the list is emitted as a reference occurrence; every later name carries no role.

Both were established the same wrong way — by reading a count — and both were caught the same
right way, by a control over a spelling nothing else in the subject can stand in for. That is the
fixture law this PR now carries: a calibration spelling must be unique AND free of every construct
that re-mentions a name, because an import list re-mentions every name it imports.

What was measured

step0_calibration_probe runs tools.reference_occurrence_binding_census over a fixture manifest and
renders one line per observed occurrence. Re-derive it with:

gunbc run --source-root dag --source-root src/v2 \
  --entry dag/test/claim/namespace_step0_census_calibration_witness_test.dag \
  --function step0_calibration_probe

authored family	what the instrument emits
type annotation	TypeOccurrence
top-level value, function value, nullary constructor, variant expression	LexicalValueOccurrence — converged, four ways
ordinary call	CallableOccurrence — discriminated
qualified container.member	two occurrences — the head as a lexical value, the member as a FieldOccurrence, neither a namespace segment. Split, not discriminated (below)
generic type argument	no denominator row at all
payload constructor in expression position	no denominator row at all
variant in match-pattern position	no denominator row at all

In the other direction, two things that reference nothing are emitted as reference occurrences: the
label of a named argument — the n in cal_called(n: 1) — stamped CallableOccurrence, and the
head of an import list, stamped as whatever category its spelling would carry. The population is
short real occurrences and long invented ones simultaneously; the errors are over different
populations and cannot cancel.

The counts behind that table are not transcribed here. step0_family_observation is the authority and
the controls join against it, so a wrong row goes red rather than standing in prose — and the earlier
version of this section named "two blind families" while the table had grown to three, which is
exactly the rot a transcribed count produces. The denominator-defect roster now derives its
omission rows from step0_unobserved_families() for the same reason.

ConstructorOccurrence and NamespaceSegmentOccurrence are uninhabited in this subject — not
dead. The fixture is small and hand-authored; an arm with no inhabitants here may have them in the
corpus. What is established is that no construction written here reached them.

"I found no row" and "there is no row" are different sentences

Only the second is a finding, and the difference is a perturbation control. A second subject
removes every appearance of one variant — its declaration, its import-list entry, and its match arm —
and the observed occurrence count changes by zero. Both counts are nonzero, so this is not two
silences agreeing. That is removing_a_variant_entirely_does_not_change_the_occurrence_count.

The positive control does the matching work in the other direction: one spelling, twice in one
file at one revision, comes back CallableOccurrence in call-head position and
LexicalValueOccurrence as a bare value. So the instrument discriminates rather than being
uniformly coarse — an instrument coarse everywhere could be excused as a lower bound; this one sees
this and not that, and cannot.

A cardinality assertion is blind to substitution, at every layer it appeared

This is the single stated rule of the PR, because it caught four separate defects in this lane:

• the family-roster contract check compared a count of families, so it would have passed over any
  substitution in the roster — replaced with set inclusion over the family, law and receipt-field
  names;
• the import-list measurement above read a count that did not move while the population did;
• two of the four metamorphic invariants were first written over sizes, where one demanded that a
  real addition add nothing and another would have passed clean over the fabrication it exists to
  catch;
• and every figure this census eventually publishes has the same exposure.

Completeness is an identity join, not a count equality (DESIGN §5). The four invariants are
therefore stated over the tag-and-category multiset — and that grain is declared honestly in the
source: cardinality rejected, tag-plus-category established (discriminating here only because
the fixture law makes every perturbed spelling unre-mentionable), exact authored-occurrence identity
not established by these controls, since the key is not an OccurrenceId and carries no
containment path or semantic slot.

Why no law we wrote would have caught it

The denominator and the observations come from one walk. Every conservation law balances by
construction over whatever that walk produced, so a family it never emits is invisible to all of
them. The anti-join cannot reach it either: an anti-join needs a population to join against, and
those occurrences were never in one. The unobserved-derivation law was written against a denominator
derived from the diagnostic; the same disease sat one layer above it.

Three consequences, carried as typed rows

1. The removed-edge roster is owned by the strip — and the reason is now stronger, not weaker. The
imported-binding grain, one row per imported name, cannot be sourced from the occurrence walk. Not
because the walk is silent there, which is what this PR first claimed, but because what it emits is
fabricated and position-dependent: an import-list entry names a binding to introduce rather than
referring to a declaration from a use site, and only its first entry is admitted. A roster sourced
from the walk would have been neither empty nor right. The strip parses the statements and their
brace lists and is the only thing that knows what it removed, so the census has two producers by
construction, joined on identity.

2. The census unit is declared. The denominator is the reference occurrence; a reader hears
reference; for one family those are different numbers. "Every occurrence receives exactly one
outcome" holds perfectly while the census answers a different question than "every authored reference
is accounted for" — the laws balance and the figure is still wrong. One number carries both findings:
a blind family maps to zero occurrences per authored reference, an observed one to one, a
split one to two. A fold joins that mapping against the observation table, so two authored tables
about one instrument cannot drift apart.

3. Three ranks below coverage, not one. A converged family is counted in the wrong bucket; a
split family is counted twice with nothing in the row schema to say so; an unobserved family is
not counted anywhere. These are different claims and only the first can be reported as coverage at
any grain. A family the instrument splits is explicitly not discriminated: one authored reference
arriving as two occurrences is only discriminated if the rows can be joined back to the one authored
slot, and the row carries no parent occurrence and no semantic-slot identity — which this module's
own grain statement already admits about its comparison key. So FamilySplitAcrossUnjoinedOccurrences
is its own arm below discrimination, and the measured partition is three unobserved, four
converged, one split, two discriminated. The discrimination count went down when this landed,
because the model got more truthful rather than because the instrument got worse. There is no arm of
step0_calibration_standing in which a partially blind roster renders as coverage, and the census's
rung is the minimum across its families.

The refusal arm is carried, not erased

The witness's subject accessors mapped a census refusal to the empty list and to zero. The
liveness control closed the false green that could produce, but a gate compensating for an erased
refusal is not the same thing as not erasing it — the refusal was destroyed and reconstructed
downstream as an observed population of size zero, which is the absorbing fallback DESIGN §5 names.
Every accessor now returns CalSubjectObserved { denominator_size, rows } | CalSubjectRefused { cause },
every control opens the carrier, and a refusal on either side of a two-subject invariant reds.
Liveness is now a property of the observed arm rather than a repair of a missing one, and
step0_calibration_probe is the located reader a red sends you to.

The roster becomes one axis

Step0ReferenceFamily had carried SameSpellingInTwoModules beside TypeReference and
OrdinaryFunctionCall. That is not a way of writing a reference but a shape of the name pool one
resolves against, and holding both on one axis made the roster unable to say that a homonym can occur
under any family. It moves to the binding-topology axis, where it composes with every family row
rather than standing beside six.

Two producer branches are declared unauthorable from source, with the harness that would reach
them, rather than covered by rows that never execute — a permanently green check gets cited as
evidence, which is worse than an absent one.

Not in this PR

No corpus run, no pre/post pairing, and no repair to the producer. The denominator was never
supposed to come from the observation walk, so patching that walk is not the fix. The mechanism behind
the fabrications is measured in a separate PR and repaired in a third, because the stamper is shared
and its blast radius — every node requested as a lexical-value declaration, which includes imports,
function and lambda parameters, type parameters and pattern binders — must be enumerated before it is
edited, not inside the measurement.

Deliberately not claimed: most rows in the first run came back Unresolved, including
cross-module spellings in a fixture where the provider is supplied and imported. Two explanations
predict that identical output and the discriminator has not been run, so it is an observation about
the probe, not a finding about the resolver.

The floor's cost refusals are a DECLARED RUNG DROP, not an open question

Cited so a reader lands on the trigger: gunbc.rung_drop floor_cost_claim_qualification_unavailable
— "Per-claim cost qualification is unavailable at the subject grain the gate consumes", declared
2026-09-01, projected in docs/design-rung-drops.md.

The rule is one reroll per exact head. Not "per head per signature" — that spelling parses as a
counter key, licensing many rerolls per distinct signature, and it is self-defeating on this row's
own claim: these arms vary across attempts of one unchanged tree, so a changed signature is the
expected outcome of a reroll rather than new information, and every reroll would license the next.
The signature is an eligibility predicate, never a budget. And eligibility is read off the run's
phase verdict — phases_run, failed, the FAILED PHASE lines — never off this class's own
disposition counters, which enumerate cost dispositions and cannot report that another phase failed.

One reroll was taken on this branch, on head 0a3e0e8c2d, and it is appended to that row's INSTANCES
list with run id, head, floor job and both arms rather than tallied. Its first version justified
eligibility with claims_failed=0 — the repudiated inside-the-subject form — and the row now carries
the correction visibly, on the evidence that actually decides it: phases_run=3 phases_failed=1 with
a single FAILED PHASE floor line and no other.

It is not carried forward. f64177c424277542f549ca22f24a20a42e3d85ed and
200591eb6f2cebc0037501c3f104cb820beab95e each completed CI green on their first attempt with no
reroll, so the budget for those heads was never spent — a receipt belongs to the tree it was
established on, and reading a green as a settle without binding it to a revision is the same defect
this lane keeps finding one layer out.

The claims and margins are not transcribed here either. Re-derive with
claim_executor --required-ci --required-lane witnesses and read the [over-cost] and
INTERRUPTED-BEFORE-VERDICT lines; the instances list on the drop row carries the per-run readings.
No budget was widened here — widening a cost requirement to get a lane green is the escape hatch §5
forbids — and the deficit belongs to the owners of those witnesses, who should learn it from a receipt
rather than from an incident.

Two things I had to correct in my own reading, recorded because they are the kind of error this PR is
about. The 500ms deadline is not a check that reports something other than what it claims: it is a
valid observation of this execution attempt, and it stays REQUIRED as attempt-safety and
verdict-availability — removing it lets runaway evaluation consume the executor unbounded. What it
cannot do is qualify the claim as an isolated subject. And "the whole distribution translates with
load" was my inference, withdrawn; what I actually established is narrower — for the one pair I
compared, the shared-fill triggered_by and provenance were identical with only the milliseconds
moving, which refutes payer transfer for that pair and says nothing about cause.

The merge that neither side could win

Integrating main produced a four-way case worth naming, because it is the merge driver's refusal
doing exactly the job it exists for. Main deleted two bridge arms from the generated dispatch
file while this branch added a builtin arm. Taking this branch's bytes resurrects two arms main
removed — and the compiler says so, E0004 non-exhaustive, since main's merged interpreter no longer
matches them. Taking main's bytes drops the builtin and nothing builds at all. Neither side is
correct, which is why a low-level driver that answered true here would have silently dropped
authority-derived content.

The file was rebuilt from main's side plus this branch's three builtin lines only to bootstrap a
compiler able to run the regenerator, and then the regenerator adjudicated it:
claim_executor --required-regen reports first_generation_equal=true over planned=executed=156.
That is the check that matters — a successful build proves only that nothing contradicts, not that
the artifact is what the authority generates.

dag/gunbc/rung_drop.dag conflicted inside a single 52,000-character line, where git can show
nothing useful and neither side reads as an overlap. Main appended its verdict-grain section before
the row's closing paragraph; this branch's reroll instance appends after it. Resolved by hand and
verified by content that each side's material survives exactly once.

Main's addition carries a same-head control — run 33806159353, two attempts on runners srv4-14
and srv4-19 at one unchanged head, opposite verdicts — which is stronger evidence for that row's
redraw reading than any instance this branch cites, because it is established by construction rather
than by correlation across runs.

Review state

Four approving reviews stand, three of them at superseded heads, and they do not settle this PR:
an approve means no blocking defect found, not that the change is what was asked for. Codex review
59402 (request_changes, at b280e56b, six commits back) is unread, not cleared — its stdout
artifact is truncated by a 1 MiB server-side cap with the verdict past the end, and the dashboard
exposes no other artifact for it. Treated as unread rather than resolved.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RvMEJFpYsy55NRdJ1Az4Vd

[gunbai-bot]

All twelve controls are green locally, each executed on the real acceptance path with a compiler
built from this branch. In the order that matters:

• the_instrument_observed_this_subject_and_is_not_silent — first, because every absence below it
  is vacuous without it. An instrument that refused, or saw nothing, answers "no row for CalRight"
  exactly as a blind one does.
• removing_a_variant_entirely_does_not_change_the_occurrence_count — the perturbation control.
  Deleting a variant's declaration, its import-list entry and its match arm moves the observed count
  by zero, with both counts nonzero. That is what makes this there is no row rather than I
  found no row; only the second sentence is a finding.
• a_call_head_and_a_bare_function_value_are_stamped_differently — the positive discriminator. One
  spelling, twice in one file, comes back CallableOccurrence and LexicalValueOccurrence. An
  instrument coarse everywhere could be excused as a lower bound; one that sees this and not that
  cannot.
• Then the two blind families, the fabricated named-argument row, the nullary-constructor stamping,
  the qualified-reference split, both roster-totality identity joins, the unit-mapping join, and the
  standing fold returning the measured 2 unobserved / 6 converged / 2 discriminated.

Also filed here: this is the rostered selection_view_read_as_population class in its inherited
form, where the view is somebody else's and therefore reads as an authority. The census consumes
module.occurrence_transport.references — a role-filtered view built beside the authored-occurrence
population index.entries — as though it were the population. The receipt is appended to that row
rather than written as a novel finding, because an instance of a known class tells the next person
where else to look. Its recognition rule gains the inherited-view form: a references or
declarations sibling beside an entries is the tell.

The repair recorded there is deliberately not "switch views". A consumer must declare its own
total eligibility disposition over the source population — every member either in the subject or
excluded by a named cause — because silence from a view someone else built is exactly how a family
disappears with nobody deciding it should, and that holds even where two views agree today.

Next measurement, not in this PR: whether index.entries carries an entry for the payload
constructor that the references view drops, and if so with what role. Presence alone cannot separate
"the population lacks it" from "the classification is blind" from "the filter predicate is wrong" —
three answers with three different repairs — so the probe must report identity, role, and whether
the references view admitted it.

— sent from jolly-badger-374

🤖 Generated with Claude Code

https://claude.ai/code/session_01RvMEJFpYsy55NRdJ1Az4Vd

[briansrls]

REQUEST_CHANGES on exact head 520ca1f764715e52512756d552c9fe0f82140560.

The prior axes, qualified-two-row, ordinal, located-reader, and prose blockers are materially closed, and this SHA is fully green/CLEAN. Two source-level blockers remain; neither needs more measurement.

1. The constructor-equality blocker is not closed throughout. step0_family_observation_key still serializes OccurrenceCategory constructors through step0_occurrence_category_label and compares the joined String; cal_rows_named_in_category likewise compares category labels. The executed outcome controls also classify binding source and disposition through cal_binding_source_of / cal_disposition_label strings, and the metamorphic key is a concatenated authored_name:category-label string. A duplicated or changed renderer label can therefore make a constructor substitution invisible—the shared-corruption case this round was meant to remove. Compare constructors directly (or use a typed { authored_name, category } key and typed predicates); keep labels only for rendering. The PR body should then say constructor inclusion, not inclusion over names.

2. The standing can still claim full discrimination while a split family remains. After unobserved becomes empty, step0_calibration_standing branches only on first(converged). If convergence is repaired while step0_split_families() remains nonempty, the Absent arm returns CalibrationDiscriminatesEveryFamily, despite FamilySplitAcrossUnjoinedOccurrences explicitly meaning that family is not discriminated. Add a split-capped arm or require split == 0 before the full-discrimination constructor is reachable.

Keep the operator’s no-more-measurement ruling intact: these are structural corrections to the carrier and selectors, not requests for another probe or corpus run.