# Execution rounds: corpus forms

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

## Law

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

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

```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):

```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):

```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):

```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):

```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):

```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).