Repository navigation
fix(frontier): prevent infinite branching-program resources from counting as zero #1717
Description
The same independent semantic review forwarded by Samuel Schlesinger found two uses of natural cardinality on unrestricted sets in ReadOnceNBP: size sums Set.ncard of edge layers, and SmallSides compares Set.ncard of the past/future sides. Set.ncard is zero for infinite sets. See the reviewed definitions.
Checked report examples: a one-step Boolean-input program with states ℕ and all edges accepts every input unambiguously but reports size0; adding those infinite edges to the two useful self-loop edges reduces reported size2→0. With one coordinate over alphabet ℕ, one state and all inputs accepted, infinite sides satisfy SmallSides 1 because their natural cardinalities are zero. Existing finite-domain lower-bound theorems exclude these examples; they are not refuted.
Repair size and small-side cardinality together after the higher-priority commitment contract. Preserve finite programs in infinite ambient state types where possible: an explicit finite-edge requirement or extended cardinality can do this. Infinite side cardinalities must compare correctly. Reuse the existing finite-edge API work and FrontierFiniteEdges regressions rather than introducing a parallel resource model.
Completion criteria: the two-edge program on ℕ states remains valid with cost2; an infinite edge layer cannot obtain finite size0; an infinite past/future side cannot witness a fewer-than-one condition. Migrate all actual consumers/affected abstracts without weakening finite frontier lower bounds, run required checks, and obtain independent outside-author-fleet API/correctness review. Attribute the report and keep its scope limits explicit.
Activity
SamuelSchlesinger commentedon Oct 30, 2026
Worker preflight —
codex-readonce-ncard-preflight-1717-20261030claims read-only analysis of both reported cardinality defects, using current main311e9841in an independent source repository. I will inspect the definitions, actual consumers/abstracts and existing finite-cardinality APIs, then recommend one repair with regression cases and migration scope.No source edits, dependency materialization, MCP elaboration or builds are included yet. #1716 remains first and root retains the only local build slot. Any eventual public-definition change will need outside-author-fleet API/correctness review.
SamuelSchlesinger commentedon Oct 30, 2026
Preflight complete; active source-only implementation — worker
codex-readonce-finite-resources-1717-20261030, branchwork/readonce-finite-resources-1717-codex-20261030, worktree/tmp/complexitylib-readonce-finite-1717-codex-20261030, from main311e9841in an independent Git repository.The repair will keep natural
sizebut require existingFiniteinstances on the used edge carriers, rather than globally restricting states or adding another resource model.SmallSideswill compareencard, matching the existingRectangleFreecontract and reusing the finite-cardinality bridges. Existing finite numerical frontier statements stay intact. Direct proof migration is in BranchingProgram/Sweep; Network's finite hypotheses already provide finite carriers. The source import graph has 22 downstream library modules and five test importers, with no selected abstract/bridge importer.Regressions will cover infinite all-edge ℕ states, the positive two-edge ℕ-state program of cost 2, and the infinite-alphabet one-state program failing SmallSides 1 while satisfying SmallSides 2. This reconstructs the forwarded report; it is not a full semantic audit. No local bootstrap, elaboration or build will run here; root's existing warm checkout will validate serialized checkpoints. Outside-author-fleet review remains required for the public definition/API change.
SamuelSchlesinger commentedon Oct 30, 2026
Awaiting review — worker
codex-readonce-finite-resources-1717-20261030: #1719 is published at6a4ef4a2. The PR owns the final definition changes, reconstructed counterexamples/positive clients, exact validation record and no-impact abstract assessment. All six gates pass in the coordinator's serialized warm checkout; no local dependency/build tree was created here.Outside-author-fleet correctness/API review is requested from edemaine. Fresh hosted CI and independent review remain required; this issue stays open until integration.
SamuelSchlesinger commentedon Oct 30, 2026
Non-author coordinator
review_logsq_savitch_1671takes integration of #1719 at6a4ef4a24ac963316f5fbb185f014095596e8f51, using the explicit outside coordinator approval and passing current-head hosted validation. The verdict uses the project's review-comment fallback; I am not adding an approval from the authoring fleet. I will preserve the queue prefix with a guarded tail enqueue, then verify the exact candidate, required queue CI, landing and main/cache handoff. The PR will own the final integration evidence.SamuelSchlesinger commentedon Oct 30, 2026
Completed in #1719. Non-author coordinator
review_logsq_savitch_1671verified actual landing and the usable latest-main/cache handoff; the final integration record owns the evidence. This completes the reported finite-resource contract repair, not a full semantic audit of the frontier development.