Execution rounds: corpus forms

Analysis of real fragments: package identifier, act name, the key fragment, form rating (exemplary / debatable / wrong-form choice) and why.

OverviewBoundariesCorpus formsPitfalls

Law

1. Maine ranked choice — full counting round (exemplary, inspected)

Package us.me.ranked_choice — Maine ranked-choice voting (United States):

Arxo Law

stage CountingRounds {
    index r: Integer from 1 to 32;
    bind round_of_the_count index 2;
    bind continuing_candidate index 3;
    bind not_continuing_at index 3;
    bind highest_continuing_ranking_is index 4;
    ...
    bind tied_for_last_place index 3;
}

Nineteen binds — everything defined “in this round”. The step forward — then round_of_the_count(c, r + 1) (the ANewRoundBegins rule from supported(removed_from_consideration(c, cand, r))). Exemplary: domain 1…32 named as a formalization boundary, not a statute one (package comment: no more rounds than candidates minus two; otherwise a loud STAGE_INDEX_OUTSIDE_DOMAIN, not silence).

2. Nauru electoral act — deduction rounds (exemplary, inspected)

Package nr.electoral_act_2016 — Nauru Electoral Act 2016 (Nauru):

Arxo Law

stage DeductionRounds {
    index depth: Integer from 1 to 32;
    bind deduction_round_required index 2;
    bind remaining_value index 3;
    bind remaining_value_seen index 2;
    bind distinct_remaining_values index 2;
    bind higher_remaining_value index 2;
    bind equal_remaining_value index 2;
}

The index is the deduction depth, not a round number: the round scale is set by subject meaning. Six bound relations whose subject is one round. Exemplary: the package comment pins the bind (“six relations bound whose subject is one round”) and the neighbourhood with judgment (lot_excludes — the Commission’s lot, not executed in rounds).

Works regulation

3. Finishing schedule — coat rounds without procedures (exemplary, inspected)

Package renovation.schedule — renovation finishing schedule (works regulation):

Arxo Law

stage CoatingTours {
    index round: Integer from 1 to 5;
    bind coat_cured index 1;
}

One bind, domain 1…5 (screed + two primer and paint coats each). Exemplary twice: the package comment names the LDC-E4126 boundary and keeps the hidden-works-act procedure in the neighbouring renovation.hidden_works package (bridge — renovation.plan), while the unmodellable (screed strength gain, not set by the work plan) is named as the SCHED_SCOPE boundary, not silenced.

Science and algorithms

4. Heaps — round as a trace step (exemplary, inspected)

Package algo.heaps — heap algorithms (teaching formalization):

Arxo Law

stage HeapTour {
    index k: Integer from 0 to 15;
    bind heap_size index 3;
    bind heap_cell index 4;
    bind heap_inverted index 4;
    bind heap_sift_swap index 4;
    bind heap_sift_swapped index 2;
    bind heap_sift_redundant index 3;
}

The index is the trace step number from the initial state, the domain starts at 0 (from 0 to 15 — the default ascending direction allows it). Step rules are k -> k + 1 over empirical intentions (HeapSizeInit writes round 0, operations write k + 1). Exemplary: state and round sift intermediaries bound, while intention markers, results and errors are not (comment: a bind names the relation and the index-argument position; intermediaries are needed for the visible descent over rounds).

5. Navier–Stokes — second disjoint stage (exemplary, inspected)

Package arxo.navier_stokes — Navier–Stokes regularity (research formalization):

Arxo Law

stage RegularityTours {
    index step: Integer from 1 to 3;
    bind ns_regularity_tour_closed index 2;
}

Three rounds of parallel stepwise checking; the package comment pins the disjointness: ProofTours from poincare binds proof_ground_closed, this one its own predicate, no overlaps. Exemplary as a new-norm specimen: bind disjointness written in words where the compiler checks it (LDC-E4124).

6. Poincaré — grounds by rounds (exemplary)

Package arxo.poincare — Poincaré conjecture grounds (research formalization):

Arxo Law

stage ProofTours {
    index step: Integer from 1 to 4;
    bind proof_ground_closed index 1;
}

Four grounds (Hamilton, entropy, surgery, extinction), the next transition applicable only after prev closes. A pair to item 5 under the disjointness rule.

7. Sequences, DSU, trees, hash tables — a family of small rounds (exemplary)

Packages algo.sequences (SeqTour), algo.disjoint_sets (DsuTour), algo.trees (TreeTour), algo.hash_tables (HashTour), algo.range_queries (RqTour) — algorithm teaching formalizations. Same-type short domains (trace steps with margin: “scenarios need no more than ten steps, the rest is margin” — see item 4 for the formula).

Form boundary

8. Empty body absent from the corpus (form boundary)

A search for empty stage <Name> {} bodies across the act corpus gave no hits: nobody keeps the reserve “for the future”. Rating: not a choice mistake but an unused form — the corpus bypassed missing rounds by feeding rounds as facts (an explicit round number in case facts instead of the index), and recent packages write executable bodies. Reserve behaviour verified by a scratch run during this research: check OK, evaluation — a loud NON_EXECUTABLE_STAGE before any conclusion (see README.md, section 4).