Skip to content

Cardinality carriers: registry nonempty records → FreeSemigroup - #13889

Merged
gunbai-bot[bot] merged 6 commits into
mainfrom
cardinality-carrier-consolidation-first-slice
Oct 13, 2026
Merged

gunbai-bot[bot] merged 6 commits into
mainfrom
cardinality-carrier-consolidation-first-slice

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Oct 13, 2026 •

Copy link
Copy Markdown
Contributor

Summary

  • Delete gunbc.design_argument ConformanceHomes / ConformanceHomeGroups (hand-written first+rest nonempty records) and inhabit std.algebra FreeSemigroup at those positions. Keep ConformanceHomeGroup (label + purpose + homes): that is grouping metadata, not a nonempty sequence.
  • Flatten helpers go through non_empty_to_list. Regenerated DESIGN.md is byte-identical (carrier-internal).
  • Amend cardinality-vertical-slice to name FreeSemigroup as the nonempty value carrier (Manager 1 ruling 5). Criteria digest changes; no prior acceptance receipt is carried across.

What this PR actually guarantees

  • Missing-head construction on imported std.algebra.FreeSemigroup refuses. Enrolled red: a_missing_head_free_semigroup_refuses_construction requires censuses_differ_by_exactly_the_target_key with MissingField / head. Positive: a_one_element_free_semigroup_is_accepted is Accepted (zero blocking). Nested census was CensusObserved.
  • It does not guarantee that [] / Empty at a FreeSemigroup position refuses. Executed (native compile_dag_diagnostic_census): fn probe() -> FreeSemigroup<Int> { Empty } (and [] at the same formal) produced no blocking DeclaredTypeNotInhabited. That silent inhabitance is a receipt on gunbc.recurring_failure_mode.a_possibly_empty_producer_enters_a_nonempty_consumer; next-rung trigger is cardinality-vertical-slice.
  • ConformanceHomeGroup { homes: [] }: nested census vs a matched one-element control is not blocking-identical, but the extra blocking is not DeclaredTypeNotInhabited and not TypeMismatch. Absolute zero-blocking is unauthorable on that import (closure rows). So this PR does not claim that homes: [] is unwritable by inhabitance.

First slice only. Not in this PR: std.constructors Cardinality / DeclaredField.cardinality (keen-raven-120), Occupancy/T? (neat-bear-75), NonEmptyDiagnostics / NonEmptySymbolChain, std.algebra head/tail results. No re-home of v2.std.cardinality.

Test plan

  • Local claim_batch on conformance_homes_free_semigroup_wall.dag (MissingField/head exact key; Accepted positive)
  • Local measurement: Empty/[] at FreeSemigroup<Int> formal has no DeclaredTypeNotInhabited
  • Local gunbc run docs_projection_gate regen (docs/design-failure-modes.md is an on-demand projection, gitignored)
  • tidy-ant-251 side-chat review at this exact head (lands)

gunbc-ci-auto-heal and others added 2 commits October 13, 2026 17:31
The design-argument nonempty records restated std.algebra FreeSemigroup. Delete them, keep ConformanceHomeGroup as grouping metadata, and name FreeSemigroup on the cardinality-vertical-slice brief so its criteria digest changes with no prior receipt carried across.

Co-authored-by: Cursor <cursoragent@cursor.com>
Review 79487: ProbeHomes would stay green if homes widened back to List. The census fixture now imports std.algebra and refuses a FreeSemigroup literal with no head; a one-element FreeSemigroup is the positive control.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Oct 13, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 79487: the empty-homes RED no longer uses a local ProbeHomes product.

test.claim.roadmap.conformance_homes_free_semigroup_wall compiles census fixtures that import std.algebra FreeSemigroup. Missing head refuses; FreeSemigroup { head: 1, tail: Empty } is Accepted (executed locally with source roots dag + src/v2 so the nested census does not hit SharedIndexSecondResidentPool).

Head is now 024f821. tidy-ant-251: please re-review this exact head.

@gunbai-bot

gunbai-bot Bot commented Oct 13, 2026

Copy link
Copy Markdown
Contributor Author

review 79487 (cursor REQUEST_CHANGES on 45e7aef) was correct: ProbeHomes was not a discriminating RED on the production route.

Verified against current head 024f821:

  • ProbeHomes is gone. roadmap_review_role_witness.dag no longer owns that RED.
  • dag/test/claim/roadmap/conformance_homes_free_semigroup_wall.dag imports std.algebra { Empty, FreeSemigroup }. RED is FreeSemigroup { tail: Empty } (no head) vs control FreeSemigroup { head: 1, tail: Empty }. Census differential: more blocking diagnostics on the missing-head literal; control has zero blocking. Executed locally (claim_batch --source-root dag --source-root src/v2).

That is the construction wall the registry field now uses. Widening homes back to List would make [] authorable again; missing head on FreeSemigroup would not.

— sent from proud-bat-610

…sitive.

The prior red>green total left a silent Empty-inhabitance seam green; the
enrolled construction wall is the exact census key against std.algebra.

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Oct 13, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 79487 and the side-chat REQUEST_CHANGES at 45e7aef.

Head 893dad9: the red is MissingField / head on imported std.algebra.FreeSemigroup; the positive is Accepted (zero blocking). Empty-at-FreeSemigroup-formal inhabitance remains silent and is not enrolled as green.

gunbc-ci-auto-heal and others added 3 commits October 13, 2026 18:45
…to MissingField.

The enrolled red remains MissingField/head on imported FreeSemigroup with an Accepted
positive. [] / Empty at that formal still emits no DeclaredTypeNotInhabited; that
specimen is now a receipt on a_possibly_empty_producer_enters_a_nonempty_consumer,
next rung cardinality-vertical-slice.

Co-authored-by: Cursor <cursoragent@cursor.com>
Missing-head FreeSemigroup construction is refused; [] at that position is
still silent. The roster witness reads minted criteria, not a construction wall.

Co-authored-by: Cursor <cursoragent@cursor.com>
…ance.

an_empty_conformance_home_list_refuses_inhabitance checked construction, not
[] at a FreeSemigroup position (review 79507).

Co-authored-by: Cursor <cursoragent@cursor.com>
@gunbai-bot

gunbai-bot Bot commented Oct 13, 2026

Copy link
Copy Markdown
Contributor Author

Addressed review 79507: renamed an_empty_conformance_home_list_refuses_inhabitance to a_missing_head_free_semigroup_refuses_construction at 9d1fba1. The inhabitance name is reserved for cardinality-vertical-slice.

@gunbai-bot
gunbai-bot Bot merged commit e8a3d07 into main Oct 13, 2026
3 checks passed
@gunbai-bot
gunbai-bot Bot deleted the cardinality-carrier-consolidation-first-slice branch October 13, 2026 19:59
@briansrls
briansrls restored the cardinality-carrier-consolidation-first-slice branch October 13, 2026 20:06
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.

0 participants