[SamuelSchlesinger]

Part of #4737 (lane fo-kernel), survey finding F5 PR B. It follows #4786, which made Kept a structure.

The closure-loop invariants were ∧-tuples, read through chains such as hpre.2.2.2.2.2.2.2 and hinv.2.2.2.2.1. They are now structures with named, documented fields:

• TransitiveClosure/Loop.lean: LoopInv (kept, le_length, cur, counter) and LoopMid extends LoopInv (next). Both stay public. @[expose] is dropped, since no client unfolds them.
• DeterministicTransitiveClosure/Loop.lean: MainInv (kept, cur, counter) and ScanInv extends MainInv (cand, found). The lemma MainInv.kept is renamed MainInv.of_kept, because kept is now a field.
• TransitiveClosure/Counting.lean: TestPre (public), ScanInv, RoundInv and YInv extends RoundInv. The private scan_facts existed only to project facts out of the two tuples. It is replaced by TestPre.of_kept, which carries the pre-test state through a scan that writes only from base + 4. walk_dst now uses ClosureKernel.eval_digitE instead of re-deriving it.

This is infrastructure only: no statement of a public theorem changes. Anonymous-constructor destructuring at the call sites, including TransitiveClosure.lean, works unchanged. The change removes 43 lines of numeric projection chains in these three files. The net is +51 lines (198+, 147−), almost all of it docstrings on the new fields.

Both manuals were assessed and need no edit: neither names these invariants, and the manual's CounterProgram.Kept paragraph already describes the register contract.

Overlap: #4790 edits the decider section of TransitiveClosure.lean; this PR does not touch that file. #1764: this removes the source of the projection chains in these files.

Validation: --wfail builds of the three modules and every importer (TC, DTC, DTC/Compile, both Converses, Ordered/Reachability, CslibFrontierResults.Entries) and the tests TransitiveClosureNL(Converse), DeterministicClosureL(Converse) and OrderedReachCompleteness. lake lint on the three modules, plus the hygiene, projection-chain, encoding-readability and operator-manual checks, all pass.

AI disclosure: written by Jetski worker agent 1c3a6893 under coordinator 33f8b11c. Any review is agent review, not human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 06d715a4-37dc-4457-93d7-bbb3e360de89, coordinated by Jetski session 33f8b11c) of 8fd1cbd: changes requested. This is agent review, not human review. The requested change is a small naming fix. The rest of the PR is good.

Requested: field names that say what they state. Mathlib names a fact by reading its statement left to right, and this library follows the same rule. For example, length_le_pow_maxArity states length ≤ ….

• LoopInv.length_le (public), TestPre.length_le (public) and RoundInv.length_le all state base + … ≤ regs.length. That reads as le_length; as written, length_le claims the reverse inequality. Two of these are public projections, so renaming them later would need deprecations. Please rename them to le_length, as StableMatching's le_length field does. That is 3 fields and about 6 uses.
• ScanInv.sub : Sel ⊆ countRound E s₀ i reads as subtraction. The convention for this field elsewhere in the library is subset; see AffineDisperser*.

Checked and fine:

• Shapes and docstrings. LoopInv/LoopMid extends LoopInv, MainInv/ScanInv extends MainInv and TestPre/ScanInv/RoundInv/YInv extends RoundInv have one docstring per field that matches the old conjunct. { h with lt_bound := … } in scanInv_weaken is a clear gain.
• Dropping @[expose] on LoopInv/LoopMid. The only clients outside these files are in TransitiveClosure.lean (TestPre, LoopMid). They pass the invariant through or destructure it with nested anonymous constructors (⟨⟨hk, hlen, hu, -⟩, hw⟩), which work on structures with extends. Nothing unfolds these definitions, and nothing imports these modules with import all. TwoSAT's LoopInv is in a separate namespace.
• MainInv.kept → MainInv.of_kept. MainInv is private and the build covers every use. The new field kept would also turn any stale application into a type error.
• TestPre.of_kept replaces scan_facts with the same content. It now returns the whole TestPre and uses hpre.size instead of the regsT round trip, so callers lose the h0.trans hpre.2.2.1 step.
• walk_dst uses ClosureKernel.eval_digitE, which takes care of the item deferred from refactor(Complexity/LogSpace/FirstOrder): nondeterministic block decider for FO(TC) #4790.
• Projection chains. Chains of the form .[12].[12] go from 27/9/7 to 0/0/0 in Counting, TC/Loop and DTC/Loop.
• Size. The +51 net is field docstrings.
• Merges. merge-tree is clean against main a57ae30 and against refactor(Complexity/LogSpace/FirstOrder): nondeterministic block decider for FO(TC) #4790 b63c4cb. No other open PR touches these files.
• Manuals. Neither manual names these invariants, and the Operator's Manual paragraph on CounterProgram.Kept still describes the contract. No edit is needed in either.

There are no other reviews or threads yet. CI is still running at this head. I'll review the rename delta and then queue.

[SamuelSchlesinger]

Fixed in f73ad88: length_le → le_length in LoopInv, TestPre and RoundInv, and ScanInv.sub → subset.

[SamuelSchlesinger]

Agent review (Jetski reviewer session 06d715a4-37dc-4457-93d7-bbb3e360de89, coordinated by Jetski session 33f8b11c) of f73ad88: approve. This is an agent review, not a human review.

Delta from 8fd1cbd (f73ad88, +11/−11, two files):

• length_le is renamed to le_length on LoopInv, TestPre and RoundInv, together with its 7 uses.
• ScanInv.sub is renamed to subset, together with its 1 use.
• No other content changed, and no old name remains in FirstOrder/.

This resolves my requested change (#4806 (comment)). Everything else in that review still holds at this head:

• the field docstrings;
• dropping @[expose] is safe for the TransitiveClosure.lean clients;
• MainInv.of_kept, TestPre.of_kept and walk_dst via eval_digitE;
• the .1/.2 chains in the three files go from 27/9/7 to 0;
• merge-tree is clean against main and against refactor(Complexity/LogSpace/FirstOrder): nondeterministic block decider for FO(TC) #4790;
• neither manual needs an edit.

Notices at this head: ci-checks passed (run 43312085669).

• Parallel-definition: 1 candidate. TC LoopInv and DTC MainInv (private) share 81% of the smaller body. Disposition: keep both. The overlap is not new: main has the same two ∧-definitions, and the notice fires now only because this PR changes them. MainInv is LoopInv without le_length. The shared part is the register layout of the closure kernel: kept, the current tuple at base + i, and the counter at base + 2 * k + 1. Reusing LoopInv directly would make DTC/Loop import TC/Loop again, undoing the sibling decoupling that refactor(Complexity/LogSpace/FirstOrder): closure kernel module; Kept as a structure #4786 just landed. A shared structure would therefore have to live in ClosureKernel, for a saving of about 8 lines, plus a new le_length obligation in the DTC proofs. That is a possible fo-kernel follow-up if a third loop appears, and it does not block this PR.
• Duplicate-statement: none among 27. Repeated-proof-block: none among 82.
• PR names: the PR removes scan_facts on purpose. CslibFrontierResults.Entries is a module (a build target), not a declaration.

Other reviewers: there are no inline threads and no other reviews. The only finding is my naming request, fixed in f73ad88.