igneum/docs/spec/finality-guarantees.md

Igneum protocol specification: finality guarantees and the long-partition boundary (rule v4)

Spec version 0.1, 8 October 2026, the finality boundary lane (branch finality-boundary). Status: Designed. Simulated at the checkpoint level (sim/finality_v2.py scenario N, rules v3, v4 pause, v4 recovery; the tables in sim/results_v2.md, "Rule v4"). Not implemented: the node change is one function and one switch (section 6.7). Not externally reviewed: this document is the answer to the external review the founder accepted on 8 October 2026 at 16:1x UK, whose finding is quoted in 6.1. Section 3 of the specification (docs/spec/03-finality.md) stays the rule; where this document and section 3 differ, this document is the statement and section 3 carries a pointer (Q5, 3.7 item 9, 3.11.2, 3.11.3). Labels as in the rest of the specification: measured (a simulator table or a network run, cited by scenario), derived (arithmetic shown in place), designed (a rule with no measurement yet).

One paragraph for a reader with a minute. A checkpoint is final when two thirds of all 30-day mining weight has signed it, counted twice: against the sliding table at the checkpoint and against the table anchored at the last certified checkpoint. When too much of that weight is missing, finality pauses and the chain keeps running on proof of work; nothing ever reverses a certified checkpoint. The pause does not end on a timer, because a timer cannot tell a node whether the missing miners are gone or on the other side of a partition. It ends when the missing weight returns, when it hands itself over, when it is stripped, or, after a full window with no certificate, when signers holding more than half of the last certified table certify the chain through it: the majority-continuity recovery, a proof any node checks from the chain. Program rotation never waits for finality: every seed is drawn from a chain block, certified or not.

1. Scope

This document states, in one place and in the form an external reviewer can check line by line: the assumptions (section 2), the two-thirds rule exactly as the node tests it (3), the safety and liveness statements with their arguments (4, 5), the long-partition rule chosen and defended with the fault it closes (6), what is not guaranteed (7), the single answer to program rotation during a pause (8), and the four words every interface uses for a transaction's state (9). The test table (10) ties each claim to a scenario, known-failed first. Section 11 lists what is owed.

"The rule" means W1 to W6, C1 to C5, Q1 to Q5 of section 3 with the change of 6.2 here, S1, F1 to F5, 3.6 and 3.11.4.

2. Assumptions

2.1 Weight and the eligible signer set

• Weight is blocks: a key's weight at checkpoint C is the number of blue blocks in the trailing 30-day window of C's past that name the key (W2; the simulator counts DAA time, the node counts DAA score along the selected chain's mergesets, the rule of 3 October 2026 denominates in past-median time). Nothing but blocks changes it: no stake, no bond, no coins.
• The sliding table T(i) at index i is the weight of every key above dust (100 blue blocks in the window, W3) and not stripped, computed at C_i from its own past. The anchored table T_f is the sliding table at C_f, the highest certified checkpoint whose block lies on the selected chain of C_i (Q5's "frozen table", renamed here because under this document it does not expire). Both are functions of the chain, so every node with C_i's past computes the same tables, and a certificate carries enough (index, block, bitmap over the canonical voter list) for anyone to verify it against them.
• How the eligible set changes, and over what window. A key enters when its window count reaches 100 blue blocks (about 9 to 10 days for the smallest honest key, 20 days for every key of a 1,000-key Pareto network from zero history, measured in sim/results_v2.md A). A key leaves the sliding table by ageing out (every block leaves the window 30 days after it was mined, whoever holds the key), by dust, by the equivocation strip (3.6: zero weight from the first block in C's past that carries the evidence, for one window), by succession (W5: its weight moves once to a successor that both keys signed for, a function of the chain, carried in any block) and by the leave item where that rule is active (finality_leave_activation_daa; Devnet 3 from DAA 93,600, about 20:01 UK on 8 October 2026). The anchored table changes in exactly two ways: it is replaced when a certificate passes it (then T_f becomes the table at the new certificate), and it is reduced by a strip or moved by a succession, both functions of the chain (the node applies "the bans known now" to T_f, section 3's Q5 row). It is never changed by time. The window over which the set can turn over completely is therefore one weight window, 30 days, and only while certificates keep forming; while no certificate forms, the anchored table holds the set as it was at the last certified checkpoint.
• Keys are free (W6): every rule draws by weight, never per key.

2.2 The adversary

Controls keys holding a fraction a of the anchored table and of every sliding table at the indices in question (a the largest such fraction). May equivocate, withhold, drop votes and certificates from its blocks, aggregate as it likes, buy or steal old keys with their history, delay its own messages, mine privately. May not forge BLS signatures or produce blocks without hashrate. Its share of a view's active weight is not bounded by a alone, which is why the floor binds on total weight (3.3.2).

2.3 Delay

Partial synchrony: after an unknown global stabilisation time (GST) every message between honest nodes arrives within a one-way bound Delta; before GST messages may be delayed arbitrarily. A partition or an eclipse is a period before GST for the nodes involved. The simulator ran Delta = 2 s between regions (0.5 and 5 s swept). No rule in this document reads a wall clock: every interval is blue score, DAA score or past-median time, and the only duration the rule names, one weight window, is the window itself. "A full window with no certificate" is daa(C_i) >= daa(C_f) + 2,592,000, a fact of the chain.

2.4 Honest hashrate

A majority of hashrate follows GHOSTDAG honestly (section 2). Finality adds a bound in weight, not hashrate.

2.5 The model's limits

The simulator has no DAG (a side's checkpoint is "the block at blue score 30 i in that view"; conflicts are index collisions), its honest keys are in outage 2.2 percent of the time, participation is the cert reading (a subset of the node's block reading, which is never lower), and a partition side counts only the blocks it has seen (+local, the real node's window). Each side retargets at once (+daa), the worst case for every clock the rule has. These are the assumptions of every table cited below.

3. The rule as the code has it

The node (consensus/src/processes/finality.rs, lock_test; the constants in consensus/core/src/finality.rs, FinalityParams, 2/3 since 4 October 2026 on the devnet-v4 line and every node line since; quorum_met, floor_met and locks are pure functions with the unit test floor_is_two_thirds_of_total_and_inclusive) locks a certificate for index i over block C_i when, with signed the weight of its signers at the table of C_i:

3 x signed x P  >=  2 x active_num          Q3, the active test   (active_num = sum over voters of weight x participation count, P the presence window)
3 x signed      >=  2 x total               Q3, the floor          (total = the sliding table T(i))
3 x signed_f    >=  2 x total_f             Q5, the anchored table (signed_f = the signers' weight AT THE WEIGHTS OF T_f; total_f = T_f)

All three inclusive: exactly two thirds locks. The floor implies the active test (active weight never exceeds total), so in plain words a checkpoint locks when two thirds of all 30-day weight at the checkpoint, and two thirds of all 30-day weight at the last certified checkpoint, has signed it. The active test and participation (Q2) stay as the liveness-side report of who is present.

What the node does today with the third line that this document changes (the Q5 row of 3.10): frozen_table finds the highest locked index below i whose block is an ancestor of C_i, takes voters_at of that block with the bans known now, and drops it when daa(C_i) >= daa(C_f) + weight_window, after which the first two lines alone decide. That drop is the timeout of 6.1. Rule v3 is behind finality_v3_activation_daa; rule v4 (6.2) is the same function without the drop plus the recovery test, behind finality_v4_activation_daa (6.7).

4. Safety

S. As long as the adversary holds less than one third of the anchored table and less than one third of the sliding table in every view, honest nodes never hold two certificates at one index naming different blocks, and never hold a certificate whose checkpoint block is off the chain of a lower certified checkpoint. S holds before and after GST, under a partition of any length and an eclipse of any length, and does not depend on the presence window.

The argument (derived). Two certificates at index i on different blocks each carry signatures of at least 2/3 T_f by the anchored table (Q5), so the weight that signed both is at least 4/3 T_f - T_f = T_f / 3; an honest key signs one block per index, so that weight is equivocating, and a >= 1/3. The same arithmetic on the sliding table gives the same bound in every view. Under rule v3 the Q5 line vanished one window after C_f, and from that point each side of a partition tested only against a sliding table it had filled with its own blocks (s + (1 - s) t / 30 of it on day t, two thirds of it by day 30 (2/3 - s) / (1 - s), 3.7 item 9), so two honest sides with a = 0 both passed at day 30: the measured fault of 6.1. Under rule v4 the anchored line never vanishes, so the bound has no time term. The recovery test of 6.2 is the one place where a certificate can lock with less than two thirds of the anchored table; its own bound is stated in 6.5 and counted in 7, and it never applies before a full window without a certificate.

The second clause (chain of a lower certified checkpoint) follows from F1 and C3 as in 3.11.2: a node that holds a certificate for C_i never selects or signs a chain that misses it, and a recovery certificate must lie on the chain through C_f by construction (6.2 item 3).

Measured: 0 conflicting locks in every honest partition of every tested length (E, I, L4, M1, M2), in every eclipse (L3), with equivocators up to 33 percent across a 50/50 split for 360 minutes (H at the 2/3 floor); 2 to 54 conflicts at 34 percent (the bound, H); the N1 rows of this document at 31 days.

5. Liveness

L. After GST, if honest voters holding at least two thirds of the sliding table at C_i AND at least two thirds of the anchored table T_f are mutually connected within Delta and signing the chain through C_f, a new checkpoint certifies within T = I + d + G + Delta = 107 s (I = 30 s, d = 60 s, G = 15 s, Delta = 2 s; simulated lock latency after the checkpoint block median 2.5 s, p99 4.6 s, A; the test network median 0.80 s). Below that there is no bound: finality pauses, the chain continues on proof of work, and the node reports finality_active false with the reason.

The argument (derived). The floor and the anchored test need the stated fractions and nothing the rest of the network does can raise or lower them (silence leaves both tables unchanged; equivocation lowers both; buying keys moves weight between holders). The active test is implied. I + d is the wait for the next determination, G + Delta the vote round trip. Withholding changes nothing above; dropping votes from a block delays a vote's entry into the DAG by one honest block; aggregating dishonestly costs nothing because anyone MAY aggregate.

How long a pause lasts, by cause (the honest statement a reviewer asked for; each row measured in the scenario named, under rule v4 with the recovery of 6.2, and the same under the pause-only variant where it differs):

Cause of the pause	Lasts until	v4 recovery	v4 pause only (6.5)
A set of a third or more is silent but keeps mining (J, N3)	it signs again; first lock 0 minutes after, 0 conflicts	at day 30 of silence the signing majority (more than half of T_f) recovers (N3)	for as long as it is silent
A set leaves gradually while locks continue (M4's gradual case)	nothing: every certificate re-anchors the table and the leavers age out of both tables	same	same
A set of a third or more stops mining and signing at once (M4, N6)	the survivors hold more than half of T_f: day 30 after the last certificate (N6, 35 percent); exactly half or more gone: never by rule (N6, 50 percent), only by succession, a strip or an operator's certificate (7)	day 30 (35 percent); never (50 percent)	never
An honest partition (N1, N2)	the heal: first lock 0 minutes after, 0 conflicts; or, at day 30, on the side that holds more than half of T_f (the 60 of 60/40), the other side never, 0 conflicts	day 30 on one side at most	the heal only
Keys worth a third or more bought or stolen and withholding (K, N4)	day 30, the honest majority of T_f recovering; a stolen key's owner can strip it by self-equivocation the same day (N4)	day 30	never for a purchase; the same day for a strip
The first month (3.8)	the window is full (min_daa)	same	same

6. The long-partition rule: the anchored table and the majority-continuity recovery

6.1 The fault this closes

The documented case (sim/results_v2.md M3, 4 October 2026, measured): a 31-day honest partition under rule v3. For 30 days neither side locks (each holds half of the frozen table). At day 30.00 the frozen table expires, each side tests against the sliding table it filled with its own blocks, and both sides lock alone: 2,679 to 2,701 conflicting locks in the 50/50 split, 2,822 to 2,870 in the 60/40 split, the first at day 30.00 to 30.06, with no attacker. The heal cannot undo them (3.11.4: no lock is ever reversed), so finality stays forked until an operator acts. A set that departs at once shows the other face of the same clause: M4's survivors lock at day 30.00 whether the departed weight is gone or on the other side of a partition.

The review's finding, which the founder accepted on 8 October 2026 at 16:1x UK: the long-partition boundary must be explicit. When enough historical voting weight disappears, the network either preserves safety and pauses, or resumes under a disclosed, verifiable continuity or recovery rule; a timeout alone cannot tell a node whether missing miners are gone or on the other side of a partition. Acceptance: a new authority set cannot override the last certified history without a clearly specified, verifiable continuity rule.

The expiry clause of Q5 is exactly a timeout alone. Rule v4 removes it and adds the one recovery that is not a timeout.

6.2 The rule (designed)

Rule v4 replaces Q5's expiry with the following, active for checkpoints at or above finality_v4_activation_daa:

1. The anchored table never expires by time. T_f is the sliding table at C_f, the highest certified checkpoint on the selected chain of C_i, with the strips and successions known at C_i applied. It stands until a certificate that passes it replaces it. A certificate for i locks only if its signers hold at least two thirds of T_f at T_f's weights, in addition to Q3, for as long as daa(C_i) < daa(C_f) + 2,592,000 (one weight window, as under v3), and
2. The majority-continuity recovery. Once daa(C_i) >= daa(C_f) + 2,592,000 with no certificate formed between C_f and C_i on this chain, a certificate for i locks when its signers hold at least two thirds of the sliding table T(i) (Q3, both tests) AND strictly more than half of T_f at T_f's weights (2 x signed_f > total_f), AND
3. C_f is an ancestor of C_i on the selected chain (the certificate names a chain through the last certified history; a certificate for a chain that misses any lock the node holds is a conflict under 3.11.4, as before).
4. A lock under item 2 is a recovery lock: it re-anchors T_f at C_i (so the next certificate needs two thirds again), it is carried, verified and followed exactly like any other certificate (C3, C4, F1, the certificate-driven reorg of 3.5), and the node reports finality_reason recovered with the index and the signed share of the old T_f for one window after it, then active.
5. Before the first certificate of the chain there is no anchored table and Q3 alone decides (3.8's first-month rule applies).

In one sentence: the last certified table is the authority until a new certificate carries the consent of two thirds of it, or, after a full window of silence, of more than half of it; nothing else, and no clock, can replace it.

6.3 Why a pause, and why this recovery and not a timeout

A node inside a partition sees exactly what a node after a departure sees: the same chain, the same missing votes, the same elapsed window. No local rule can tell the two apart, which is the review's point, and any rule that resumes on elapsed time alone resumes on both sides of a partition and forks (6.1). The anchored table is therefore the default: when enough weight is missing, finality pauses and stays paused. The chain does not stop (5).

The majority test is the one resumption that is safe without knowing which case it is in, because it is asymmetric by construction: two certificates at one index each carrying more than half of T_f need more than T_f in total, so some key signed both (derived). Under a partition with no equivocator, at most one side can hold more than half of the last certified table, whatever each side mined since; the 50/50 split holds exactly half on each side and stays paused until the heal (N1, measured: never in 31 days). After a departure, the survivors recover exactly when they are the majority of the table the chain last agreed on (N6: 35 percent gone, day 30; 50 percent gone, never). Bought or stolen keys that withhold lose their veto at day 30 to the honest majority (N4), where the pause-only variant hands one purchase a permanent veto.

6.4 The continuity proof, and who can verify it

A recovery certificate is verifiable by anyone holding the chain, with no operator, no committee and no out-of-band input: (i) T_f from C_f's past (W2 at C_f, bans and successions as the chain carries them at C_i), (ii) T(i) from C_i's past, (iii) C_f an ancestor of C_i (reachability), (iv) daa(C_i) - daa(C_f) >= 2,592,000 and no certificate between (the node's own locks on this chain), (v) the bitmap over the canonical voter list at C_i and the aggregate signature. A light client that holds C_f's certificate and the header chain checks the same five facts (section 10's receipt already carries the voter table with weights). This is the "disclosed, verifiable continuity rule" of the acceptance line: the new authority set, the signers of T(i), cannot certify anything unless a majority of the old authority set, T_f, signed with them, and never on a chain that misses C_f.

6.5 The cost, stated, and the one-line alternative

The recovery certificate's safety bound is weaker than one third. Two conflicting recovery locks need a partition that has lasted a full window with no certificate on either side AND equivocating keys whose share of T_f exceeds the split's imbalance: each side of an s / (1 - s) split with an equivocator at a holds (1 - a) / 2 + a of T_f in the 50/50 case, more than half for any a > 0; in a 60/40 split the 40 side needs a > 0.2 to reach half. Measured (N1b, N2): at 31 days a 50/50 split with a 10 or 20 percent equivocator conflicts under v4 recovery and never under v4 pause; the 40/40 split with a 20 percent equivocator reaching both sides (60/60 of T_f) the same. In every such case the equivocator is stripped at the heal (3.6), the history through C_f is untouched (item 3), and the pair is handled as 3.11.4 says. The one-third bound of section 4 is intact for every certificate formed within a window of the last one, which is every certificate of a connected network.

The alternative the founder can choose by deleting item 2 is the indefinite pause (v4 pause in the simulator, P.recovery = False; in the node, the recovery test left out). Its guarantees are strictly stronger: no certificate ever forms with less than two thirds of the last certified table, so the one-third bound holds for every certificate for ever. Its costs, measured: one purchase of keys worth a third of a window is a permanent veto on finality (N4: never in 31 days, against day 30 with the recovery), a sudden honest loss of a third of weight (a pool folding with its keys) pauses finality permanently absent succession or an operator's trusted certificate (N6: never, against day 30), and a 60/40 partition that outlasts a window pauses the 60 side until the heal instead of recovering at day 30 (N1).

This document recommends the recovery (items 1 to 5 as written), because its failure needs an attacker, a month-long partition and equivocation that the chain then punishes, while the pause's failure needs no attacker and has no exit inside the protocol; and because the recovery never touches certified history, which is what the acceptance line protects. The founder chose "the pause over the fork" on 4 October 2026 (ledger F21) against a fork that needed no attacker; this recommendation keeps that choice (the honest 31-day partition never forks under either variant) and adds a bounded, disclosed exit. The decision is the founder's at the 18:00 UK report; the simulator and the node carry both as one switch.

6.6 How it composes with the rest of the rule

• No certified checkpoint is ever reversed (3.11.4) stands unchanged: a recovery lock adds a certificate, it never withdraws one; a node holding two valid certificates at one index keeps the first, reports conflict, and the protocol does not pick.
• The certificate-driven reorg (3.5, ledger C4) carries recovery certificates: a node on the other side of a healed 60/40 partition, holding no lock since C_f, verifies the 60 side's recovery certificate against T_f and T(i) from the block's own past and moves to it. Measured: every pre-heal lock kept, first lock after the heal 0 minutes, 0 post-heal stalls (N1).
• Succession (W5) and the strip (3.6) are the two in-protocol ways the anchored table changes without a certificate, both functions of the chain: a miner that retires hands its weight to a successor (which then counts in T_f at the old key's weight), and the owner of a compromised key equivocates with it once to remove it from every table (N4: finality resumes the day the evidence is carried).
• The trusted certificate (F5) is the operator's exit for the cases no rule covers (half or more of T_f gone for good). It gains one check: a configured trusted certificate MUST lie on the chain through every lock the node holds, else it is refused; an operator cannot be handed a certificate that overrides certified history.
• The exchange guidance (3.9) gains one row: finality_reason recovered means a lock formed under 6.2 item 2 within the last window; an operator who prefers the pause-only reading treats it as paused for that window. The pause row itself is unchanged: a pause is proof of work, the reorg bound is the finality depth in median time.
• Layer 4 of class rotation (the emergency miner vote, docs/design/class-rotation-four-layers.md): no flip vote counts while finality is paused, and a recovery lock counts as a lock; the schedule stands throughout (8).

6.7 The node change

One function and one switch, for the node lane; nothing here lands on any network until the founder sets the height. frozen_table (the Q5 row of 3.10) keeps its reference and loses its drop; evaluate and ingest_off_chain test floor_met(frozen_signed, frozen.total) while daa(C_i) < daa(C_f) + weight_window and continuity_met(frozen_signed, frozen.total) (2 x signed > total, a pure function with its own inclusive-boundary unit test) after, provided no lock exists between; a lock that passed by continuity_met is stamped recovered in the record and getFinalityCheckpoints reports finality_reason recovered with anchored_index and anchored_signed_share for one window. Switch finality_v4_activation_daa (never on every network until set; the digest arm entered only when set, so a binary carrying the field peers with one that does not, the rule of every switch since 0.3.20). Unit tests, known-failed first: the M3 shape (A at 60 percent and B at 40 percent lock together, B leaves, A alone must not lock under v4 pause ever and must lock under v4 recovery only once the last lock is one window old; under v3 it locks at the window, the known-failed line); and a 50/50 shape that never locks under either v4. The fast-time harness row is tools/finality-attacks/v3.mjs split50 extended past the window (SPLIT above 120 DAA at 60x), where v3 must conflict and v4 must not.

7. What is NOT guaranteed

1. At or above one third of equivocating weight two valid certificates can exist at one index; the rule reports and does not resolve (3.11.4).
2. A recovery lock is bounded as 6.5 states, not by one third: a month-long partition plus an equivocator outweighing the split's imbalance can produce two recovery locks after C_f. The history through C_f is never touched.
3. A loss of half or more of the last certified table at once has no in-protocol exit: finality pauses until the weight returns, hands over or is stripped, or an operator configures a trusted certificate on the chain through the last lock (F5 with 6.6's check). The chain runs on proof of work meanwhile.
4. An exactly even partition (each side exactly half of T_f) pauses until the heal. Half is not more than half.
5. The first month (3.8): no certificate until the window is full; proof of work guidance applies.
6. Body availability and execution correctness: a certificate is a statement about a header chain by voters who validated it; availability and pruning are F3 and section 2, execution is section 7's proofs. The "proven" word of section 9 is a different claim from "finalised".
7. Everything the model excludes (2.5): no DAG, the 2.2 percent outage guess, the cert reading, no VRF noise, no cost of keys. The young-window form of the sliding bound (W / R of a side's DAA time) is a devnet fact, not a mainnet one.
8. Participation credited for any vote at the index (O-3.19), the block-reading re-run (O-3.18), the launch-month simulation (O-3.1), the forced double certificate on a network (O-3.17) remain open as section 6 of the specification lists them.
9. Clock. Nothing here reads wall-clock time, so nothing here is guaranteed in wall-clock terms: "30 days" is 2,592,000 DAA seconds of the chain, which a retarget lag can stretch or shrink in real time by the amount section 2's controller allows.

8. Program rotation when finality is unavailable: the single answer

Mining and validation continue, and every seed is drawn from a chain block, never from a certificate. This is one rule for all four layers of class rotation and for both VDFs, and it closes O-4.3 for the epoch as the era VDF lane closed it for the era:

• The hourly program's seed source is the reference block of the epoch: the last selected-chain block below the boundary less the lead, walking down from the header's own selected parent (HeaderProcessor::epoch_seed today keys the devnet's epoch on the header's own past, lead 600; class v5's C_w is the same block for the hour; 4.3 step 1 names the checkpoint block at that score, certified or not, by the decision of 3 October 2026, 3.11.6). The era's cut block is the same shape at lead 7,200 (EraVdfManager::cut_block, class_signal::seed_below, 4.4 step 1). The week's and the family epoch's reference blocks in docs/design/class-rotation-four-layers.md section 2 are the same shape at their leads. Every one is a function of the header's own past, so two nodes validating one header derive one program, and a header on a chain that reorged across the reference names another block and is validated under that block's seed.
• A finality pause therefore changes nothing for rotation: through a pause of any length, including the first month and the 31-day partition of N1, the program changes every hour, the parameter era every week, the family set every 180 days, on both sides of a partition, each side under the block its own chain names. A later certificate confirms the seed the certified chain used or discards a branch F1 already discarded; it never changes the program of any block on the certified chain (3.11.6).
• The one thing that stops during a pause is layer 4's emergency vote (no flip vote counts while finality is paused, by that document's own rule); the scheduled family epoch is a height, not a vote, and stands.
• The certified binding (the design document's wording, the era record's section 4 alternative) is rejected for both VDFs: it couples the seed to finality liveness (a month-long pause would hand every epoch the same stale checkpoint), it needs a second rule for a certificate that lands late, and the grinding defence does not need it, since the delay makes any candidate's draw unknowable whichever block is the cut.

Consistent with docs/spec/04-seeds-and-vdf.md 4.3 step 1 and 4.4 step 1 and with docs/analysis/era-vdf-2026-10-07.md section 4. O-4.3 closes with this document; the devnet row "seeds during a pause" of 3.11.7 is still owed as a harness run (11).

9. The four interface words

Defined once, for every interface (the wallet, the explorer, the live page, the receipt and light pages, the miner app, the node's status word), from the weakest claim to the strongest. Each word is a claim about one transaction; a stronger word implies every weaker one; no interface may show a word stronger than the chain's own (the wallet's ledger P17 rule, kept).

Word	Claim	Source of truth	Can it be withdrawn
included	a block in the DAG carries the transaction	the including block (includingBlock in the receipt's igneum section)	yes: the block can be red or the chain can move; until executed it is an announcement, not a result
executed	the EVM ran it in a chain block with a number; the receipt (status, gas, the fee split) exists	the chain block of that number (t.number, the receipt)	yes: a reorg above the last lock can change the chain block of a number; the receipt then changes with it
proven	the chain block's execution has been proved: every shard verified or paid (section 7)	the proof records of the chain block (shards verified or paid)	yes, for the same reason as executed: a proof is of a block, and the block can leave the chain; it adds "the result was checked", not "the result is permanent"
finalised	the chain block is at or under the latest locked checkpoint's blue score (a chain block under the lock, or merged by one), in the past of last_certified	the lock (a certificate verified against the tables, 3 and 6.4)	no (3.11.4): no node ever reports as not final a block it reported as final; a conflict is reported as conflict, never as a withdrawal

Two surrounding states: pending (no block carries it) and failed (executed, the execution reverted, the fee still paid), and the network state word finality paused (the chain is running on proof of work; applies only to blocks ABOVE the last lock). A block under a locked checkpoint is finalised whether or not finality is active afterwards; "finality not active" is a statement about the network, never about a block that is already under a lock.

Where each interface shows them today (read from the worktree at box master 5cd69d3d), and where it does not, for the UI lanes:

Interface	Shows	Does not, or differs
Wallet, History page (app/igneum-wallet/ui/app.js 131 to 147, stateWord; view.test.mjs 117)	all four, plus pending and failed, one word per row, the wallet's own verified "finalised" winning over the node's word	shows finality not active for a transaction "under a locked checkpoint; finality is paused on the network" (line 144): by this section that transaction is finalised and the pause is a network state; the wallet lane should move the pause to the status strip (line 98 already shows "paused" there) and keep the row's word
Node transaction status (node_status.state from the app's GET /api/tx/<hash>, the words the wallet switches on)	included, executed, proven, finalised, finality not active	the same "finality not active" word for a block under a lock; the node should report finalised for the block and paused for the network, in two fields
Explorer, transaction page (site/tx.html 370 to 400)	"Status" = the receipt's success or failure; "Lock state" final or not final with the reason; "Proof" x of y shards paid; "Including block ... executed under chain block N"	none of the four words as the row's state; final where this section says finalised; no single state word for the transaction (the reader assembles it from three rows)
Explorer, block page (site/block.html 386 to 420)	"N transactions executed" chip; "Lock state" final or not final; "Proof" shards	final for finalised; "included" is not said of the carried transactions (the page says "carried")
Explorer API (site/api/explorer.mjs, lockState)	final: true/false with a reason; shard states	no words; a consumer maps final to finalised itself
Live page (site/live.html 423 to 651)	included, excluded, pending (the block's colour), proven, "locked checkpoint", "selected chain"	executed and finalised are absent: a block under the lock reads "locked checkpoint" only when it is the checkpoint itself; blocks under it have no word
Receipt and light pages (site/receipt.html, site/light.html, site/lc/app.js)	"proven" in the verifier's sense ("a receipt proven against the finality certificate", "Proven balance"); "final" through the certificate check	proven here means "verified by this page against the certificate", which is this section's finalised plus a local check; the word collides with the proof-of-execution sense; the reference-apps lane should say "verified final" (or "finalised, verified here", the wallet's phrase) and keep "proven" for execution proofs
Miner app (app/igneum-app/ui/app.js 505 to 509, 1398)	"proven" for shard pieces and segments ("0 assigned, 0 proven, 0 paid")	no transaction states, correctly: the app has no transactions; the word is the proving sense
Site copy ("Mined by GPUs. Proven by fire.", every page's footer and image alt)	the brand line	not a state word; unchanged

Rule for the lanes: one vocabulary, four words plus pending and failed, the network state shown separately as finality active, paused or recovered; final in the explorer becomes finalised; the live page gains executed and finalised for blocks under the lock; the receipt pages keep proven for execution proofs only.

10. Test table

Each claim, the scenario, the known-failed line first where there is one, and the result. Simulator rows are sim/finality_v2.py --scenarios N --seeds 7,11 at the 2/3 floor, each side retargeting and counting only its own blocks, run on build-3 under the lease tool; the tables are in sim/results_v2.md, "Rule v4". Where a row says "pending" the run had not landed when this version was written; the 20:00 UK version carries the numbers.

Claim	Scenario	Known-failed line	Result
(a) The 31-day partition at the window: no conflicting locks under the chosen rule	N1: 50/50, 60/40, 55/45 for 31 days, v3 against v4 pause and v4 recovery	v3: both sides lock alone at day 30.00, 2,679 to 2,870 conflicts (M3, re-run in N1)	pending
(a) The recovery bound	N1b: 50/50 for 31 days with a 10, 20, 34 percent equivocator	34 percent: conflicts from minute 0 under every rule (the one-third bound)	pending
(b) 40/40/20 under the active-set rules	N2: honest three-way for 150 minutes and 31 days; 40/40 with a 20 percent equivocator reaching both for 31 days	the 60/60 case under v4 recovery at day 30 (6.5)	pending
(c) Signing stops while mining continues	N3: 34, 40, 45 percent for 24 h under v4 recovery; 34 percent for 31 days under both v4	none expected (as J)	pending
(d) Old keys compromised against fresh hashrate	N4: keys worth 40 percent withhold, holder at 30 percent of hashrate, 31 days, v2, v3, v4 pause, v4 recovery; the self-strip on day 1	v4 pause: never (the permanent veto, 6.5)	pending
(e) Finality paused across an epoch boundary: seeds advance, mining continues, certified history intact	derived from N1 and N3: blocks and checkpoints continue through the pause (every stalled checkpoint in the tables is a block the chain mined), 744 hourly boundaries in a 31-day pause, each seeded by its reference block (8); the fast-time harness row (11)	none	derived; harness run owed
(f) The heal: a deterministic path that never reverses a lock	N1, N2: every pre-heal lock kept, first lock after the heal, post-heal stalls; the certificate-driven reorg (3.11.7, c4.mjs)	none	pending
The epoch 20 template fault (today's fault 6)	the node lane's fast-time gate: every epoch boundary a template test; the release-rules record	a header refused for missing state counted as a PoW strike	node lane's regression, outside this lane's harness time (11)
The cold-start deadlock (today's fault 7)	the node lane's kept-datadir gate on a chain paused over ten minutes	the sink-age guard on a node holding the chain	node lane's regression (11)

11. Owed

1. The fast-time harness rows on a box: tools/finality-attacks/v3.mjs split50 past the window under v4 (the N1 shape on real nodes, three nodes, the 60x file), a pause across an epoch boundary reading the program id on both sides (row (e)), and the two regressions of 8 October on a node pair carrying the hotfix (/srv/artefacts/0326-f8da7515 on build-1), each under lease pool on build-2 or build-3; queued behind the sweeps at the time of writing.
2. The node change of 6.7 on the node line, behind finality_v4_activation_daa, with the two unit tests and the known-failed v3 line.
3. The 720-index tally of layer 4 against the simulator (that document's section 11), under the pause and the recovery.
4. The interface changes of 9 by the wallet, explorer, live and reference-apps lanes.
5. Section 3 of the specification: Q5's expiry clause, 3.7 item 9's last sentence ("a partition longer than a window still forks"), 3.11.2's "beyond a window the frozen table is empty" and 3.11.3's departure row to point here (O-3.20).