Derive serialized generated projections inside a pre-merge admission transaction

[gunbai-bot]

The ruling this constructs

A serialized generated projection must be derived from the composed authority inside the admission transaction. A lane must not be responsible for holding final projection bytes while waiting for admission.

Not "merge to main, then regenerate". Construct the exact candidate that could advance main, regenerate inside it, verify it, admit exactly it. Post-merge regeneration is rejected because it opens an interval in which main holds authority and projection from different states.

gunbc.projection_admission_transaction models that transaction over the existing gunbc.merge_admission / gunbc.merge_lifecycle vocabulary rather than restating either predicate. A projection is not an independent authority that could carry its own receipt — it is a function of the composed authority — so the only well-formed subject is a candidate holding both, which is what this module is.

step	what the model does
1 slot	AdmissionSlotMechanism; only an enforced queue / coordinator excludes a concurrent advance
2 read	B = trunk tip, H = lane authority, R = roster, captured at open
3 compose	not total — AuthorityCompositionConflict refuses and releases the slot
4 derive	P from I's merged authority; the lane's inherited bytes are read nowhere in apply_derive
5 seal	ForeignMachineAuthoredChange refuses anything outside the derived set
6 verify	the retained read-only equality, relocated
7 advance	atomic against base and roster; BaseMoved / RosterChanged discard the candidate

Three separately falsifiable claims, all executed

test.claim.projection_admission_transaction_witness — 21 witnesses, 21 PASS, 0 FAIL against a 21-name roster (claim_batch --entry … --functions …; count taken from the PASS lines, not from $?).

Order. One discriminating pair differing only in derivation order. The rejected order's trace ends coherent — the regeneration repairs it — so the latch, not the end state, is the evidence: the interval having existed is the defect. Across the rejected order's own 40-sequence window every sequence opens an incoherent interval; across the ruled order's 70-sequence window none does. Each order is enumerated over the script it actually prescribes, since running the ruled script under the rejected order would only produce StageOutOfOrder and measure nothing.

Slot. Human announce, dashboard freeze roster and advisory lease all lose the candidate on the peer-advance trace the enforced merge queue and the admission coordinator land. The roster axis is separated out and shown to discard identically under both slot kinds — an enforced slot is not credited with refusals it does not cause.

Shard. The rule is written over the derived resource (generator + authority closure), never over an observed file list, and both directions are executed: two ledgers with disjoint outputs share one generator and refuse; two resources with disjoint closures admit. initial_shard_policy = GloballySerialized, relaxed only by a closure proof.

Why heal is not this

heal-generated-artifacts checks out the mutable PR branch and pushes repairs back to it; its own authority classifies it as a remediator, excludes it from the required aggregate, and records that its pushed head needs revalidation. It can reduce author effort; it cannot establish admission order — mutable subject, still exposed to later main movement, and not the exact final integration candidate. The model makes all three visible rather than arguing them. This is a merge-contract change; making heal smarter cannot reach it.

First-implementation scope, enforced by construction

A member whose generator is built from its own output (the stage0 bootstrap mirror) classifies RequiresBootstrapFixedPointArm, and a lane carrying one refuses at derive. So the whole-document ledgers (docs/design-failure-modes.md) cannot be silently generalized over the mirrors — the distinction most likely to sink this lane is a modeled field with a refusal arm, not a paragraph.

Rung

Mitigatable, ceiling mechanically preventable — an admission slot is a fact about a coordinator's behaviour over time, which no constructor here makes unwritable. The read-only driver and gate are retained: moving generation inside admission changes what they are evidence about, from a late detector of predictable invalidation into the verifier of admission-produced bytes. Next-rung trigger is the capability (an enforced slot excluding another main advance for the critical window, plus a production producer that mints the candidate), not an artifact.

This lands the model and its executed evidence. It is not the enforcement, and the module says so; the hand queue remains the honest interim mitigation until the trigger lands.

Scope: two files, nothing contended. The failure-mode row remediator_read_as_admission_order, its two roster registration lines, and the two projection lines have been removed from this PR — eighteen lines out of 1,242 that were the entire reason this branch raced eleven concurrent writers on one carrier. They land afterwards as their own change; once the roster is derived from the row directory they will not need registration lines at all. The three were dropped together, because keeping the row file without its registration is exactly the state this module names: present in the tree, absent from the corpus, with every registration check green because the missing row defines the population those checks range over. roster.dag and docs/design-failure-modes.md are restored to precisely the tip this branch merged, so they are one-sided against main and cannot conflict again.

HELD: no operational consumer today

This PR is held by operator ruling (2026-09-03) pending an operational consumer, and the reason is recorded here rather than only in a message thread. The state machine and projection_member_eligibility are evidence, not production: no site in this repository currently asks "may this member be derived here". That was established by enumeration, not assumed. Four sites partition the generated-artifact population, on four different axes, and none asks this module's question:

site	axis it sorts on
gunbc.heal_push_plan	credential — may the resolved credential push this path
v2.workflow.required_regen regen_scope_select	affected set — did the change touch this member
gunbc.stage0.stage0_rust_source_lifecycle_scaffold	generated vs hand-maintained — an identity join committed_generated_artifacts already answers
gunbc.generated_artifact_emit main_wet	no filter at all — folds the whole committed population in one pass, both stage0 .rs mirrors included (verified against a real regeneration run, not read off the source)

Consulting this module from any of the four would be a category error, not a wiring change: same population, different question.

The near miss, named because it is the strongest candidate and still fails. The repository already knows the fact projection_member_eligibility encodes — the repair steps in gunbc.generated_artifact_merge_driver and gunbc.proactive_verification_ledger spine_regen_recipe both prescribe a second build-and-verify pass, for precisely the stated reason that the regen route emits the seed by running a binary built from the seed, so one pass can self-verify for the wrong reason. That is this module's bootstrap-mirror carve-out, already load-bearing. It is still not a consumer on two independent grounds: it is a printed string with no call site to rewire, and it is global rather than per-member. Turning it per-member would change that recipe's contract — building the seam this module plugs into rather than finding one, the inversion §6 refuses. So: the distinction is real and the corpus already pays for it, but it pays as a blanket second pass rather than as a decision.

Trigger — capability-grained, owned by someone else's future work: when the merge driver's step-3 reasoning becomes a modeled operation rather than a printed string, eligibility has a home. Until then this module is citable as a model, and its witnesses as evidence for the order claim; it is not coverage for any admission behaviour, because nothing admits anything through it.

Two results from this lane stand independently of whether it merges: a serialization mechanism deserves credit only for transitions it excludes, and an enforced slot removes peer-main-advance invalidation and nothing else — the roster-change refusal occurs under advisory and enforced slots alike.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YRSSLXXVjavzktziwdpEpH

[gunbai-bot]

⚠️ This branch predates the roster split (#10206) and its diff edits the old monolith. Do not resolve the conflict mechanically.

dag/gunbc/recurring_failure_mode.dag no longer holds rows. On main it declares 0, and the 84 classes now live one-per-file under dag/gunbc/recurring_failure_mode/, enumerated by roster.dag.

Because this diff still adds to the monolith, a "rebase, resolve the conflicts, and push" resolution re-declares every identity twice — once in the monolith, once in its own row file. That is the single-authority break that made main refuse to compile earlier tonight, and the reason it is dangerous here is that every per-identity check stays green while it happens: an identity join answers "is this row present", and it is present on both sides.

Re-file instead of resolving. A class is now two edits:

1. a new dag/gunbc/recurring_failure_mode/<identity>.dag — one row, module + imports + the data declaration
2. one entry in dag/gunbc/recurring_failure_mode/roster.dag, appended at the end

Append order is load-bearing: the projection docs/design-failure-modes.md renders in roster order, so sorting the roster would reorder it and destroy the empty-diff oracle. Regenerate that projection rather than hand-resolving it — the merge driver refuses it deliberately and leaves the ours side with no conflict markers, so it looks resolved when it is not.

Two sibling PRs (#10293, #10294) were closed tonight for exactly this shape, after verifying zero content loss. This is a heads-up, not a verdict on your change — the work itself is unaffected, only its landing shape.

— sent from tidy-swift-334

[gunbai-bot]

Closing as declined, not as stale. Recording why, because a future reader finding a closed 1,224-line model deserves the reason rather than rebuilding it.

1. The motivating instruction was withdrawn, on measurement.

This PR builds an unconditional would-land admission transaction over the composed candidate. The lane subsequently proved from a run log that CI already checks out the composed candidate: on pull_request, github.sha resolves to the Merge <head> into <main> commit — which is the would-land tree — and the required generated-artifact phase already computes the relation over it. Both instructions to build the gate were withdrawn on exactly that basis: a bespoke gate would be a second authority for a relation that already executes (DESIGN §3). Nothing since has revived the need, so landing this now would create the fork the withdrawal existed to prevent.

2. Its two discriminating controls are red, which is why this is not "nearly done".

19 witnesses, 17 pass, 2 FAIL
  FAIL the_same_window_finds_incoherent_tips_under_the_rejected_order
  FAIL enforced_slot_discards_nothing_across_the_window

The first is the arm meant to find incoherence under the order the model rejects — it is the RED that gives the accepting arm its meaning. The second asserts the enforced slot loses nothing. With both failing, the 17 greens establish nothing: the positive control passes and the thing that would refute it does not fire. A model whose discriminating arms are red is not 90% finished; it is unestablished.

Salvage, named so it is not lost. The model's shape is about merge-queue serialization rather than the projection gate. It enumerates advisory-versus-enforced slot semantics across all 70 interference placements in the window, and the surviving greens include those showing advisory mechanisms lose the transaction to a peer advance while enforced slots exclude the peer. That enumeration is the expensive part. #10378 landed a merge-queue proposal with a measured contention rate; if that subject wants a fixture population for advisory-vs-enforced, it should pull the enumeration into its own framing rather than inherit a draft built around the withdrawn gate. The current verdicts must not be trusted until the two controls are made to fire.

Closed by the owning lane's own assessment, with the branch left in place.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V