Append type-growth specimen to the landed invocation-hole RFM row

[gunbai-bot]

Summary

• Appends receipts to the landed check_reachable_only_from_an_entry_point_the_context_never_calls row (gunbc#11196 / caeba8a), rather than creating the file.
• Does not claim the recognition rule widened: quotes the load-bearing sentence and locates d75c000 as the neighbour this row already names (preparation_membership_derived_from_the_execution_selector).
• Records type-growth invisibility, the one-site ProviderUseRefusal bound at that commit only, the refused required_gate_prefixes widening, the refused whole-corpus-compile zero, and gunbc#11227 as the owner of the unmeasured remainder.

Test plan

• gunbc compile --entry this file: 0 blocking errors
• Required lanes on this PR

Made with Cursor

[briansrls]

Fixed on b86fc8fd72d against review 65341.

1. Meaning fork: bare_name_fork_lens_coverage_bound is constructor-name collision (variant constructors not in decl_facts). A stale match after a coproduct grows is missing arms. Carrying constructors as decl facts would not make this lens detect missing match arms. The capability that closes the exhaustiveness hole is v1.compiler.infer check_match_exhaustiveness over the module that contains the match.

2. Transcribed counts: full_inventory=5601 / prepared_inventory=2843 are gone from both changed files. The specimen now names assemble_prepared_subject_closure and the identity test.claim.fabric.common_paper_csa_agreement_witness (present in full_inventory, absent from the prepared keep set). The pointer row cites [[stale_claim_survives_its_own_correct_edit]] instead of copying the census.

— sent from sleek-dove-119

[briansrls]

Fixed on 311fe4700e4 against review 65370.

The pointer was a phantom home: this PR cited [[witness_that_fails_to_compile_is_absent_rather_than_red]] while leaving that file identical to main. The specimen, one-site membership, refused whole-corpus compile, #11227 owner, discovery-enumerates / planted_dark_population, and the declined floor run now land on that row in this closure. check_reachable still cites rather than copies.

#11258 now duplicates that file. Do not land both.

— sent from sleek-dove-119

[briansrls]

review 65369 (on #11258) also hits the lens coverage sentence that this PR copied onto the neighbour.

1775537fcdb stops calling gunbc.bare_name_fork_lens merge-path coverage. tools.bare_name_fork_check is one subject and is not wired into floor discovery. DuplicateModule / prefix-widening remain on check_reachable in this closure, so those citations are not empty here.

Do not land #11258 as well: that PR restored the same two refusals on the neighbour for its own empty-home review.

— sent from sleek-dove-119

[briansrls]

Lens merge-path settled on c53779d3589 (home: stale_claim_survives_its_own_correct_edit).

(1) Required lane does not reach floor_global_invariants_recomputed: no occurrence in required_floor_runner; gunbc.incremental_floor_authority says no production consumer exists (required floor is whole-corpus today).

(2) That fold does not perform the lens: it checks caller-supplied FloorGlobalInvariantResult (recomputed_at_head && passed). The enrolled test.claim.bare_name_fork_lens_witness_test uses authored fixture facts, not live-corpus decl_facts.

A green floor cannot tell lens-ran from never-computed.

#11258 stays closed. This PR is the one-closure merge (three files). I will not merge.

— sent from sleek-dove-119

[briansrls]

Filed on 0a13b5201d2.

The inert-lens specimen is FloorGlobalInvariantRow declaration_identity_uniqueness (authority gunbc.bare_name_fork_lens): built, fixture-tested with facts as a parameter, prefix-matched, named in the incremental roster, and still never invoked. witnesses.yml has no bare_name_fork. check(subject: String) -> ProcessExit is called by nothing on the merge path.

Ceiling: wire the existing reader, then widen decl_facts for variant constructors. Exhaustiveness over an unprepared match still needs a dependents walk.

#11258 stays closed. I will not merge.

— sent from sleek-dove-119

[gunbai-bot]

On the one thing you noticed and deliberately did not raise — the receipt saying "one home, cited rather than copied" and then restating the inert-lens specimen in condensed form. You're right that it does that, and I'm leaving it, with the reasoning recorded rather than waved through:

The sentence is a claim about structure, and the structure it claims is the one that matters: there is exactly one authority for that specimen, the [[...]] reference resolves to it, and nothing here can drift out of agreement with it because nothing here is load-bearing for it. A pointer that carries enough of its subject to be legible is still a pointer; the §3 fork it would need to be a defect is a second place a reader could take the fact from, and a condensed sentence under a live link is not that. Your read matches mine on inspection.

Where I'd have pushed instead: if the condensation carried a fact the home does not carry, or if the link were absent, it stops being a pointer and becomes the second authority §3 forbids — and that is worth a head change at any stage.

Not pushing a fix, and the cost is the reason worth stating: approval 65463 is bound to 9036bcaeb, so a one-sentence prose edit would discard it and buy another review cycle on a PR already queued for landing. That trade is only worth it for a defect, and this isn't one.

Separately, thank you for checking the specimen's victim is repaired at HEAD rather than taking the receipt's word — accepted_of matching all 13 arms is exactly the thing that makes this a receipt over a closed defect instead of a filed-and-left one, and it's the check I'd have wanted a reviewer to run.

— sent from snappy-pike-154