Skip to content

Cuts 2 and 3 of the #11596 recut: the kernel's producers, and declared-id admission - #11932

Merged
briansrls merged 8 commits into
mainfrom
session/calm-koi-99
Sep 21, 2026
Merged

briansrls merged 8 commits into
mainfrom
session/calm-koi-99

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 21, 2026 •

Copy link
Copy Markdown
Contributor

Cuts 2 and 3 of the gunbc#11596 recut, against the identity kernel that landed in gunbc#11669. Roadmap node review-sheet-identity-producer-and-admission.

The kernel landed as pure semantics with three enrolled consumer frontier rows whose triggers name execution rather than import. This is that execution, and it repairs the production converge the kernel deliberately did not touch.

Cut 2 — the producers, which decide no standing

  • review_sheet_marker_query(marker_field, marker_value) is one query shape over a field parameter, with review_sheet_current_marker_field and review_sheet_superseded_marker_field beside it. Two callers now build a marker query; a second spelling of has { key='K' and value='V' } is the fork that would let one drift into asking a different question while both reported the same fact. mimeType and trashed=false belong to the shape for the same reason.
  • gunbc.review_sheet_legacy_extent_producer holds the Drive superseded-marker producer and the subject-bound operator-declaration reader. Each turns one reading into a LegacyExtentEvidence value and stops. What that evidence establishes is the kernel's answer and only its answer — the separation is the lesson of the closed An identity that moved, a search that only knew where it moved to, and the duplicate that followed #11596, which computed the reading and the conclusion in one place, where no type recorded the difference.
  • gunbc.review_sheet_identity_converge ensure_review_spreadsheet_on_identity replaced the observation-only ensure_review_spreadsheet rather than landing beside it (DESIGN §3, replacement migrations cut over at the root). It is a third module because the kernel imports the converge for the observation shape, so the converge cannot import the kernel back.

The load-bearing fact is enforced by the shape of legacy_search_visibility_basis, which has exactly two answers because the corpus can make exactly two. A find is self-proving and scoped to that observation. Every other answer — including a clean 200 with an empty list — leaves visibility unresolved, because appProperties are private to the requesting application and nothing here observes the OAuth application identity of its own token. There is no compatible-empty arm in any spelling, and no comparison of service-account principals, which are the wrong identity grain.

Cut 3 — declared-id admission

gunbc.review_sheet_declared_id_admission is the only consumer of the kernel's LegacyFileSelection. It reconciles the intended subject, then the standing, then a contradicting observation, then an exact file-by-id preflight — cheap refusals first, so a declaration naming another subject is refused without spending a request discovering that.

drive.Files.GetFile is new, and its field mask names every required field of DriveFile: a mask of id alone decodes short and reports a landed read as a transport failure. admit_preflighted_file binds the readback to the requested id, not to the status — a 200 says the request worked, not that it worked on the file that was asked for.

The refusal this cut exists to install, and the one a later reader will want to widen: a selection beside an unresolved extent stays unresolved. The operator has said which file they choose, not that no other lineage exists. The discharge is an "absent" declaration, which is a statement about the world and has a kernel arm.

What changes on the live path

A current-marked file beside an unsettled superseded extent now refuses instead of adopting. It writes nothing either way, so adopting looks harmless — but reporting it as converged asserts a single lineage nobody established, and the kernel names collapsing that arm into ReviewSheetSingleLineage as what "reported success over a drive that held two". Adopting quietly would be the absorbing fallback DESIGN §5 refuses: the deficit would stop being visible.

The refusal is loud, names the discharge, and is retired by an operator declaration for that exact subject at review_sheet_legacy_declaration_path. The steady state still converges with one — a_current_hit_with_a_matching_declaration_adopts_without_writing is that control. This does not re-open the hand repair of the live sheet.

What the operator has to do, exactly

The next live converge run will refuse until an absent-declaration exists on the converging host. Write this file at /etc/gunbc/review-sheet-legacy-extent-declaration.json:

{
  "drive_id": "0ANpu9VSqUzO-Uk9PVA",
  "marker_key": "gunbcReviewSheet",
  "marker_value": "ci-prospect-sheet",
  "current_marker_field": "properties",
  "superseded_marker_field": "appProperties",
  "legacy_extent": "absent",
  "basis": "<what you actually did to establish this -- e.g. listed the Customer Acquisition shared drive as its owner in the Drive UI on <date> and saw no other review sheet>"
}

Notes that will save a round trip:

  • All five subject members are required and none is defaulted. A missing member refuses and names itself; a member that disagrees with the live subject refuses as "a different identity subject". Filling one in from the subject being asked about would make every declaration match by construction, which would turn the kernel's subject wall into a decoration — so the reader transcribes and the kernel compares.
  • basis is required and must be non-empty. A declaration with no stated basis is an assertion with nothing behind it. Write what you actually did; nothing machine-reads it.
  • legacy_extent admits exactly "absent" and "selected". Anything else — a spelling, a hedge, "probably absent" — refuses rather than being read as the nearest admitted value.
  • "absent" is a claim about the world: no file carrying appProperties.gunbcReviewSheet exists in that drive. Only declare it if that is what you established. The whole point of this lane is that an empty search cannot establish it for you — a human who can see the drive can.
  • The "selected" form is the Cut 3 path and is for a different situation: two lineages were observed and you are choosing between them. It carries the same five members plus "file_id", and it is refused unless the id is one an observation actually returned.
  • The path is a declared row, not an argument. gunbc run passes arguments only as argv, and on this fleet an argv word is readable by any job payload a PR can influence — so a caller-supplied path would also be a caller-supplied answer.

Consumer and executing route (DESIGN §3c)

Both cuts are called from gunbc.review_sheet_spreadsheet_actuator converge_review_spreadsheet, reached from converge_drive_half via the argv-free entry converge_drive_half_cli. The declaration file is read once per pass and handed to both the extent producer and the admission: two reads would be two demands for one fact with the converge as their least common ancestor, and they could disagree if the operator edits between them.

All three kernel frontier rows retire. The roster stays as an empty list because gunbc.census_closure_frontier folds it by name.

Evidence — 37 claims, all executed

test.claim.review_sheet_legacy_declaration_wet_witness (12 claims) writes a real declaration into a throwaway temp directory and reads it back through the production reader, the production JSON reader, the production subject transcription, the production kernel join and the production decision — one composed call, no supplied value anywhere in that chain. Enrolled on the required floor's local-repo wet lane.

claim
Discriminating red an_absent_declaration_beside_an_empty_current_search_refuses_the_create_by_real_execution — the exact state the live converge was in when it minted the duplicate. The file is really absent, so the refusal comes from the production reader failing to find it. The replaced fold answered Apply here.
Positive control a_matching_declaration_beside_an_empty_current_search_authorizes_the_create_by_real_execution — without it, a converge that refused everything would pass the red and never create anything again.
Red, Cut 3 a_selection_beside_an_unresolved_extent_stays_unresolved
Control, Cut 3 a_selection_between_two_observed_lineages_stands_for_adjudication

What the evidence does not establish, said here rather than left to be assumed: the two Drive legs — the superseded-marker query and the file-by-id preflight — are supplied at their response boundary and execute on the operator's live converge run, not in CI. No claim in this change says otherwise.

Scope

One PR rather than two: Cut 3 rewrites the same converge_review_spreadsheet body Cut 2 introduces, so the cuts do not separate cleanly, and a stacked PR on a non-main base gets no CI here.

Out of scope and untouched: Cut 4 (UpdateFileProperties PATCH and readback) and Cut 5 (legacy-generation retirement) belong to the separate roadmap node review-sheet-properties-write-and-legacy-retirement. No marker relocation. The closed #11596's combined migration route is not executed or salvaged.

🤖 Generated with Claude Code

gunbc-ci-auto-heal and others added 3 commits September 21, 2026 02:55
…d-id admission

gunbc#11669 landed the review-sheet identity kernel as pure semantics with three
enrolled consumer frontier rows whose triggers name EXECUTION rather than import.
This is that execution, and it repairs the production converge the kernel
deliberately did not touch.

CUT 2 -- THE PRODUCERS, WHICH DECIDE NO STANDING.

  review_sheet_marker_query(marker_field, marker_value) is ONE query shape over a
  field parameter, with review_sheet_current_marker_field and
  review_sheet_superseded_marker_field beside it. Two callers now build a marker
  query; a second spelling of "has { key='K' and value='V' }" is the fork that
  would let one drift into asking a different question while both reported the
  same fact. mimeType and trashed=false belong to the shape for the same reason.

  gunbc.review_sheet_legacy_extent_producer holds the Drive superseded-marker
  producer and the subject-bound operator-declaration reader. Each turns ONE
  reading into a LegacyExtentEvidence value and stops. What that evidence
  ESTABLISHES is the kernel's answer and only its answer -- the separation is the
  whole lesson of the closed #11596, which computed the reading and the conclusion
  in the same place, where no type recorded the difference.

  THE LOAD-BEARING FACT IS ENFORCED BY THE SHAPE OF legacy_search_visibility_basis,
  which has exactly two answers because the corpus can make exactly two. A find is
  self-proving and scoped to that observation. EVERY other answer, including a
  clean 200 with an empty list, leaves visibility unresolved -- appProperties are
  private to the requesting APPLICATION, and nothing here observes the OAuth
  application identity of its own token. There is no compatible-empty arm, in any
  spelling, and no comparison of service-account principals, which are the wrong
  identity grain.

  gunbc.review_sheet_identity_converge ensure_review_spreadsheet_on_identity
  REPLACED the observation-only ensure_review_spreadsheet rather than landing
  beside it (DESIGN section 3: replacement migrations cut over at the root). It is
  a third module because the kernel imports the converge for the observation
  shape, so the converge cannot import the kernel back.

CUT 3 -- DECLARED-ID ADMISSION.

  gunbc.review_sheet_declared_id_admission is the only consumer of the kernel's
  LegacyFileSelection. It reconciles the intended SUBJECT, then the STANDING, then
  a CONTRADICTING OBSERVATION, then an exact FILE-BY-ID PREFLIGHT -- cheap
  refusals first, so a declaration naming another subject is refused without
  spending a request discovering that.

  drive.Files.GetFile is new, and its field mask names every required field of
  DriveFile: a mask of "id" alone decodes short and reports a landed read as a
  transport failure. admit_preflighted_file binds the readback to the REQUESTED
  ID, not to the status -- a 200 says the request worked, not that it worked on
  the file that was asked for.

  THE REFUSAL THIS CUT EXISTS TO INSTALL, and the one a later reader will want to
  widen: a selection beside an UNRESOLVED extent stays unresolved. The operator has
  said which file they choose, not that no other lineage exists. The discharge is
  an "absent" declaration, which is a statement about the world and has a kernel arm.

WHAT CHANGES ON THE LIVE PATH, stated plainly because it is a behaviour change.
A current-marked file beside an unsettled superseded extent now REFUSES instead of
adopting. It writes nothing either way, so adopting looks harmless -- but reporting
it as converged asserts a single lineage nobody established, and the kernel names
collapsing that arm into ReviewSheetSingleLineage as what "reported success over a
drive that held two". Adopting quietly would be the absorbing fallback DESIGN
section 5 refuses: the deficit would stop being visible. The refusal is loud, names
the discharge, and is retired by an operator declaration for that exact subject at
review_sheet_legacy_declaration_path. The steady state still converges with one --
a_current_hit_with_a_matching_declaration_adopts_without_writing is that control.

CONSUMER AND EXECUTING ROUTE, per DESIGN section 3c. Both cuts are called from
gunbc.review_sheet_spreadsheet_actuator converge_review_spreadsheet, reached from
converge_drive_half via the argv-free entry converge_drive_half_cli. The
declaration file is read ONCE per pass and handed to both the extent producer and
the admission: two reads would be two demands for one fact with the converge as
their least common ancestor, and they could disagree if the operator edits between
them. All three kernel frontier rows retire; the roster stays as an empty list
because gunbc.census_closure_frontier folds it by name.

EVIDENCE. 37 claims, all executed, no supplied value standing in for the
declaration route:

  test.claim.review_sheet_legacy_declaration_wet_witness -- 12 claims that WRITE a
  real declaration into a throwaway temp directory and READ IT BACK through the
  production reader, the production JSON reader, the production subject
  transcription, the production kernel join and the production decision. One
  composed call. Enrolled on the required floor's local-repo wet lane.

  DISCRIMINATING RED: an_absent_declaration_beside_an_empty_current_search_refuses_the_create
  -- the exact state the live converge was in when it minted the duplicate. The
  file is really absent, so the refusal comes from the production reader failing to
  find it. The replaced fold answered Apply here.
  POSITIVE CONTROL: a_matching_declaration_beside_an_empty_current_search_authorizes_the_create
  -- without it a converge that refused everything would pass the red and never
  create anything again.

  RED for Cut 3: a_selection_beside_an_unresolved_extent_stays_unresolved, with
  a_selection_between_two_observed_lineages_stands_for_adjudication as its control.

WHAT THE EVIDENCE DOES NOT ESTABLISH, said here rather than left to be assumed: the
two Drive legs -- the superseded-marker query and the file-by-id preflight -- are
supplied at their response boundary and execute on the operator's live converge run,
not in CI. No claim in this change says otherwise.

OUT OF SCOPE and untouched: Cut 4 (UpdateFileProperties PATCH and readback) and
Cut 5 (legacy-generation retirement) belong to the separate roadmap node
review-sheet-properties-write-and-legacy-retirement. No marker relocation. The
closed #11596's combined migration route is not executed or salvaged.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review finding on gunbc#11932. The annotation carried "AN OBSERVATION BEATS A
DECLARATION" and "THE ORDER IS NOT A PREFERENCE" twice: refactoring the function
to take the declaration as a parameter prepended a new block and left the old one
standing above it. Two copies of one rationale on one carrier is the fork DESIGN
section 3 names, and the second paragraph differed only in wording -- "Reading the
declaration first" against "Preferring the declaration" -- which is the shape that
rots worst, because a later editor repairs one and leaves the other.

The surviving block keeps the read-exactly-once consumption fact, which was the
genuinely new paragraph and was never duplicated.

Checked the mechanism rather than only the reported line: a block replacement that
leaves its old annotation behind would do this silently anywhere I used it. Scanned
all seven modules this branch touches for repeated annotation openers -- no other
orphans.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review observation on gunbc#11932 (review 69480). The annotation on
selection_against_sole_observed_file said agreement "is a no-op in substance --
the converge would have adopted that file anyway". That is true on
ReviewSheetSingleLineage, where ensure_review_spreadsheet_on_identity answers
Noop, and FALSE on ReviewSheetLegacyOnlyLineage, where it REFUSES. Prose claiming
more than the code does, on the one arm where the difference decides whether an
operator declaration matters at all.

THE BEHAVIOUR IS KEPT AND THE ANNOTATION NOW DESCRIBES IT. Admitting a declared
selection on a legacy-only lineage is a real adjudication, and it is narrow rather
than a widening of that refusal: the extent is SETTLED on that arm, because a
legacy-only lineage is reached only through a positive find, which is self-proving;
the id is one that observation returned; and the file-by-id preflight confirms it
names a readable spreadsheet first. What it authorizes is an ADOPTION -- a read and
a format -- never a create beside the file and never a write to it, so the
duplicate this lane exists to prevent stays impossible. It is the operator's route
past a legacy-only sheet until the separately roadmapped write cut lands.

AND THE ASYMMETRY IS NOW EXECUTABLE RATHER THAN ASSERTED. A reviewer had to derive
it by reading two modules, which is the tell that it lived in prose and nowhere
else. a_legacy_only_selection_adjudicates_a_refusal_a_single_lineage_one_does_not
asserts all four facts -- the ensure refuses on legacy-only and Noops on single,
the selection stands on both -- so an edit collapsing the two arms in either
direction goes red instead of quietly changing what a declaration is worth.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

HOLD — exact head 97882b0e118a9a9a143118c1f4aacdd4a5ba21cf.

The producer split, subject-bound declaration reader, exact file-by-id preflight, and the ordinary current-hit/unresolved-legacy refusal are all materially better than #11596. One authority leak remains in Cut 3.

P0 — a duplicated current side lets a selection bypass an unresolved legacy extent

The PR’s load-bearing rule is stated correctly: a selection beside an unresolved extent stays unresolved. selection_against_standing enforces that for:

CurrentMarkerObservedLegacyExtentUnresolved { file_id: A, ... }

but not for:

ReviewSheetConflictingLineages {
  current_file_ids: [A, C],
  legacy: LegacyExtentUnsettled { ... },
}

On the conflict arm, a selection is admitted when its id appears in current_file_ids or in settled_legacy_ids(legacy). settled_legacy_ids(LegacyExtentUnsettled) correctly returns [], but a selected current id still passes. The route then performs the file-by-id preflight and converge_review_spreadsheet returns SpreadsheetAdoptedByDeclaredId(A).

That admits this incident-compatible state:

current properties search -> A and C
legacy appProperties extent -> unresolved because this OAuth app cannot see old private markers
invisible original lineage -> B may still exist
operator selection -> A
result -> adopted A / success

The fact that two current files were observed does not make the unresolved legacy namespace disappear. The selection adjudicates A versus C; it does not establish that invisible B does not exist. This is the exact conclusion-from-insufficient-extent class the recut exists to close, reached through the conflict arm rather than the single-current arm.

Required repair

Match on the legacy verdict before admitting any selection from ReviewSheetConflictingLineages:

  • LegacyExtentUnsettled -> reject every selection;
  • LegacyExtentSettledEmpty -> a selected observed current id may stand;
  • LegacyExtentFound -> a selected id may stand only if it is in the observed current or legacy populations.

Add a discriminating pair on the actual pure admission path:

  1. current [A,C] + legacy unsettled + select A -> SelectionRejected;
  2. same current [A,C] + legacy settled empty + select A -> SelectionStandsForAdjudication.

The existing a_selection_beside_an_unresolved_extent_stays_unresolved covers only the single-current disposition and does not exercise this arm.

Exact-head CI is green, but this is an untested semantic branch, not a compilation failure. No other blocking source finding on this head.

…uction

THE ARM THAT LEAKED. selection_against_standing's ReviewSheetConflictingLineages
arm asked ONE question -- does some observed population name this id? -- with the
UNSETTLED legacy side contributing no candidates to it. That is true, and it is
not enough: a selected CURRENT id still named a population, so a selection beside
an unresolved superseded extent was admitted through the current side while this
module's own law refused the identical situation one arm away, in
CurrentMarkerObservedLegacyExtentUnresolved.

The admitted shape was: current-marker observation [A, C], legacy extent
UNRESOLVED, operator selects A, preflight succeeds, adopted. The operator has
adjudicated A against C. Nothing established that an invisible superseded-marked
B does not exist -- a different marker field with a different visibility, which
is the whole content of this lane.

THE REPAIR IS THE ORDER, AND IT IS BY CONSTRUCTION. The arm now delegates to
selection_against_conflicting_lineages, which matches the LegacyExtentVerdict
FIRST. The LegacyExtentUnsettled arm carries no SelectionStandsForAdjudication
constructor at all, so re-admitting it is an edit a reader has to write rather
than a condition they can loosen (DESIGN 4b: construction over validation;
DESIGN 5: a failure arm refuses, never widens). SettledEmpty offers the observed
current ids; Found offers the union of the two observed populations.

settled_legacy_ids and legacy_observed_ids_text are gone: both existed only to
feed the single-question shape, and the per-side wording their refusal needed is
now passed from each SETTLED arm, so the operator still learns WHICH observation
failed to return their file.

BOTH CONTROLS, SHOWN RED BY MUTATION RATHER THAN ASSERTED, against a local gunbc
over the full source roots:

  current [A,C] + unsettled    + select A -> SelectionRejected
  current [A,C] + settled empty + select A -> SelectionStandsForAdjudication

Mutation 1, restoring the defect (unsettled routed to the current population):
the refusal claim returned false and the settled-empty claim stayed true.
Mutation 2, an over-prohibition (settled-empty offering no ids): the
settled-empty claim returned false and the refusal claim stayed true. Each
control discriminates in one direction only, which is what keeps the fix from
being a module that refuses every selection.

an_unsettled_legacy_side_offers_no_ids_to_select is retargeted to the new
refusal text: its case now lands on the unsettled arm rather than on the
unobserved-file one, and it goes red under mutation 1 with the new control.

The load-bearing fact is untouched: an empty appProperties search still
establishes only that this OAuth client received no matching rows. No
compatible-empty arm in any spelling; the marker is where it was.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@gunbai-bot

gunbai-bot Bot commented Sep 21, 2026

Copy link
Copy Markdown
Contributor Author

The P0 is repaired in 578e29653f7.

The order, not a guard. The ReviewSheetConflictingLineages arm now delegates to selection_against_conflicting_lineages, which matches the LegacyExtentVerdict first:

  • LegacyExtentUnsettled — refuses, and carries no SelectionStandsForAdjudication constructor at all, so the unsettled case has no path to admission rather than a condition a later reader can loosen;
  • LegacyExtentSettledEmpty — an observed current id may stand;
  • LegacyExtentFound — an id may stand only from the union of the two observed populations.

settled_legacy_ids and legacy_observed_ids_text are deleted. Both existed only to feed the single-question shape; the per-side wording their refusal needed is now passed from each settled arm, so the refusal still tells an operator which observation failed to return their file.

Both controls, each shown red by mutation rather than asserted, run against a locally built gunbc over --source-root dag --source-root src/v2:

claim repaired mutation 1 (defect restored) mutation 2 (settled-empty offers no ids)
a_selection_among_conflicting_current_files_beside_an_unsettled_extent_refuses true false true
a_selection_among_conflicting_current_files_beside_a_settled_empty_extent_stands true true false

Each discriminates in one direction only, which is what stops the repair from being a module that refuses every selection.

an_unsettled_legacy_side_offers_no_ids_to_select is retargeted to the new refusal text — its case now lands on the unsettled arm rather than on the unobserved-file one — and it goes red under mutation 1 alongside the new control.

Nothing widened: no compatible-empty arm in any spelling, the marker is where it was, Cut 4 and Cut 5 untouched.

One thing outside this fix. This branch’s merge base predates src/v1/stage0/linked_partition_crates.generated.txt landing on main (#11863) — the file is absent from the branch tree, and a local cargo build -p v1-compiler --bin gunbc refuses on it (build.rs cannot read the projection). Worth a merge from main before landing.

The change request is on the GitHub review and new commits do not clear it, so it needs a dismissal or a re-review from you.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

SOURCE APPROVE — exact head 5a792d21c21c22e59bae5c486cdb8295c91167c0.

The prior P0 is closed on the actual admission path.

ReviewSheetConflictingLineages now delegates to selection_against_conflicting_lineages, which matches the LegacyExtentVerdict before examining candidate ids:

  • LegacyExtentUnsettled has only a SelectionRejected construction;
  • LegacyExtentSettledEmpty offers only the observed current ids;
  • LegacyExtentFound offers the observed current + observed legacy union.

Therefore [current-A,current-C] + legacy-unsettled + select current-A can no longer reach SelectionStandsForAdjudication, while the same current population beside a settled-empty legacy extent remains admissible. The new discriminating pair executes exactly those neighboring states, so the repair is not an over-prohibition. The exact file-by-id preflight and production actuator remain downstream unchanged.

The merge from main retained the repair and the generated linked-partition artifact; I found no new source blocker in the relevant route.

One nonblocking annotation debt remains: the older comment above selection_against_standing says only the conflicting-lineage standing admits a selection, while the intentionally supported agreeing sole-lineage cases are explained later and pinned by a witness. Do not move this approved head merely for that prose cleanup; record it for a follow-up.

At review time, compiler and clippy are successful and the exact-head floor is still running. Merge/queue only after all required checks for this SHA are terminal-success and the head remains unchanged.

Brian Searls and others added 3 commits September 21, 2026 17:35
…s a write

Review 69620. The sentence defending the ReviewSheetLegacyOnlyLineage
admission claimed it authorizes "an ADOPTION -- a read and a format -- never a
create beside the file and never a write to it". Half of that is false and it
is the half defending the only behavioural widening in the diff:
SpreadsheetAdoptedByDeclaredId reaches format_converged_spreadsheet, which
formats through converge_review_sheet_format, which issues Sheets batchUpdate
operations against the selected id. Verified by following the route rather
than by reading the annotation.

Corrected rather than gated. The write IS authorized on this arm, and the
annotation now says so and says why: a legacy-only lineage is reached only
through a positive find, which is self-proving, so there is no unread
generation the write could be landing on -- the file formatted is the file
observation returned and the operator then named by id. The adjacent unsettled
arm has no such proof and now admits no selection at all. Withholding the
format only here would adopt a sheet and leave it unformatted, which is a
half-converged state nobody asked for.

The true half is kept and marked as the one that carries the lane's guarantee:
never a CREATE beside the file. That claim is about minting a second lineage,
not about touching the one the operator adjudicated, and it still holds.

This is the same class commit 97882b0 fixed one arm away on this branch --
prose asserting more than the code does (DESIGN §4c, §4d over-assertion).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Side-chat review of 5a792d2 recorded this as annotation debt rather than a
gate. Fixing it now, in the same commit window as review 69620's correction,
so the head moves once instead of twice.

The sentence above selection_against_standing said only
ReviewSheetConflictingLineages admits a selection. Three arms do:
ReviewSheetSingleLineage and ReviewSheetLegacyOnlyLineage both route to
selection_against_sole_observed_file. The distinction worth keeping is not how
many admit but what KIND of admission each is: the conflicting arm is an
adjudication between observed rivals, while the two sole-lineage arms admit
only a CONFIRMING selection -- the declaration must name the very file
observed, and any other id is rejected. That is why they do not route through
the adjudication fold.

Same class as the previous commit and as 97882b0: prose asserting
something the declarations do not say (DESIGN §4c).

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@briansrls
briansrls added this pull request to the merge queue Sep 21, 2026

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

SOURCE APPROVE / LAND — exact head afd3c62f764e29e69d2d80d8a1f5ad57c8c41680.

I re-read the moved-head delta from the previously approved 5a792d21c2.

The only branch-authored changes to the reviewed authority are the two annotation repairs:

  1. The legacy-only declared-ID route now says the truth about its effect: formatting is a Sheets batchUpdate write to the selected file. That write is admitted because this arm is reached only through a positive, self-proving legacy find and the operator confirms that exact observed ID; the load-bearing containment is that the converge never creates a second sheet beside it.
  2. The selection annotation now names all three admitting standings and distinguishes them correctly: conflicting lineages admit an adjudication among observed rivals; the two sole-lineage arms admit only a confirming declaration naming the sole observed file.

Neither changes a constructor, judgment, network route, admission, or claim. The merge from main did not alter the review-sheet semantic surface; it brought unrelated v2/roadmap work and the generated linked-partition state.

The prior unresolved-legacy repair remains intact: LegacyExtentUnsettled has no route to SelectionStandsForAdjudication, while settled-empty and positive-found extents admit only observed IDs.

All four exact-head checks (compiler, clippy, floor, witnesses) are terminal-success, the PR is mergeable, and I found no new source blocker.

This approval is SHA-specific. Freeze this head and merge/queue it unchanged.

Merged via the queue into main with commit d41c94e Sep 21, 2026
4 checks passed
@briansrls
briansrls deleted the session/calm-koi-99 branch September 21, 2026 19:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant