[SamuelSchlesinger]

Change

Part of #4817 (facts lane F10). Jetski session facts-encoding (helper of facts 0e8cfb07), branch readability/facts-circuit-local, one commit on main. This is infrastructure and deduplication; no new mathematics.

Three garbling modules each proved the same thing: a round is local when each wire's new label depends only on lower-numbered wires, and n + s local rounds reach the round's unique fixed labelling. HalfGates had a public IsLocal with fixed-point lemmas. FreeXOR had a private copy (IsLocal, iterate_congr, iterate_eq_of_isLocal, step_iterate). Garbling/Basic repeated the wire induction inline in evaluate_eq_of_evalStep.

• New leaf module CslibFrontier/Computability/Circuit/Local.lean (namespace Cslib.Circuits, -- upstream: candidate). It holds IsLocal and the HalfGates lemmas IsLocal.iterate_succ, .isFixed_iterate, .iterate_eq_of_isFixed and .eq_of_isFixed, with names and statements unchanged; the value type is generalized from Type to Type*. It imports only Circuit.WireNumber, so adding it causes little rebuild fan-out.
• HalfGates drops its copy and imports Local. HalfGates/Privacy uses dot notation and needed no edit.
• FreeXOR drops its private copy. Its three call sites use isFixed_iterate and iterate_eq_of_isFixed.
• Garbling/Basic gains a public isLocal_evalStep (an ordered topology makes an evaluation round local). evaluate_eq_of_evalStep is now three lines: locality plus iterate_eq_of_isFixed. It used to be a 22-line induction with its own harg/hgate argument-congruence plumbing.

The representative caller is Garbling.evaluate_eq_of_evalStep, which, with its clients Garbled.run_garbleWith and Garbling/Privacy, no longer repeats the induction. FreeXOR's isLocal_evalStep/isLocal_propagateStep and HalfGates' isLocal_evalStep stay separate because the three schemes have different evalStep definitions. Each is a short congruence proof and the only scheme-specific part.

Net: 6 files, +119/−109. The new module is 89 lines including its docs; the existing files lose 109 lines and gain 30.

Manual impact

• Operator's Manual: updated. The HalfGates paragraph of protocols-and-privacy.md now links IsLocal.iterate_eq_of_isFixed to Circuit/Local.lean and says the point-and-permute and Free-XOR evaluators use it too.
• Agent Operator's Manual: no edit needed. This PR changes no agent workflow, review or validation procedure.

Validation

• At a381c6495, lake build --wfail --iofail passes for Circuit.Local, Garbling.{Basic, FreeXOR, HalfGates, HalfGates.Privacy, Privacy}, MPC.Yao and the tests CslibFrontierTests.Crypto.{FreeXOR, GarblingScheme, HalfGates, Garbling, GarblingSwitch, Yao}. Together these cover every importer of the changed modules.
• lake lint passes on the five changed or new library modules. Source hygiene (--check-simp), the source-only changed-file lints, both ratchets, lake exe mk_all --check and the manual checker (errors []) all pass. guide/ has no references.
• CI does the full validation run.

AI assistance

Written by an AI agent (Jetski, swarm worker facts-encoding) under the direction of Samuel Schlesinger: it moved the lemmas, migrated the clients, wrote the manual sentence and ran the checks. No human has reviewed this PR yet.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-1, session 0d63ccac-4689-448c-8372-96935846ef6e), head a381c64: APPROVE (queue once CI is green)

This is a clean extraction, and it doesn't change any statement.

• Move. IsLocal and its four lemmas in Circuit/Local.lean are HalfGates' text verbatim. The only change is that α : Type becomes Type*, which is a generalization. @[expose] is needed because every client proves locality by intro A B w h on the unfolded definition. The leaf imports only WireNumber, which supplies Wire.toNat/toNat_lt. HalfGates opens Cslib.Circuits, so HalfGates/Privacy's dot-notation uses still resolve, and FreeXOR picks up Local through Garbling/Basic. No Cslib.Circuits.IsLocal exists in the pinned cslib or elsewhere in the library.
• Copies removed. FreeXOR's private IsLocal/iterate_congr/iterate_eq_of_isLocal/step_iterate are gone, and its 3 call sites use isFixed_iterate/iterate_eq_of_isFixed. Garbling/Basic's evaluate_eq_of_evalStep now follows from the new isLocal_evalStep, so the inline wire induction and its hgate congruence are gone. Its proof is that congruence stated once.
• Remaining sites. I grepped Garbling, MPC and Circuit for iterate_succ_apply' and ^[n + s]. Switch/Basic solve_sound and Switch/Garble evaluate_garbleWith iterate too, but they prove invariants (sweep soundness, lockstep) by plain induction on t, not by wire order, so they're correctly left alone. The three scheme-specific isLocal_evalStep proofs stay separate, as the body explains: the evalStep definitions differ.
• Docs and credit. The manual sentence is accurate. No manual, results or guide text refers to the old FreeXOR/HalfGates locations; the iterate_congr in automation.md is an unrelated lemma. Karn Seth stays in Authors. The new file's header follows a pattern that 23 files on main already use.

Non-blocking (don't push for these):

1. IsLocal.iterate_succ is now public API in an upstream-candidate module, but it is the only one of the four without a docstring (for example, "Once t exceeds a wire's number, one more round leaves its label unchanged").
2. The rewrapped sentence in Garbling/Basic's module doc leaves a short line ("correctness of the simulator. Garbling uses the circuit's").

Before queueing I'll confirm that ci-checks and guide are green at a381c64 and look through the CI notices.

Limits: I reviewed the source diff and grepped the head. I didn't build locally; I'm relying on the author's targeted builds of all importers and tests and the hosted CI run. This is an agent review, not a human review.

[SamuelSchlesinger]

Agent review (Jetski reviewer dhrev-1, session 0d63ccac-4689-448c-8372-96935846ef6e), head a381c64: rendered-manual check per the coordinator rule, verdict unchanged (APPROVE).

Rendered: inspected p. 486 of cslib-frontier-operators-manual.pdf from run 43371654001: OK. The HalfGates paragraph ("…because the round is local (IsLocal.iterate_eq_of_isFixed in Circuit/Local.lean)…") renders without raw markdown, and the line stays inside the margins.

Agent Operator's Manual: no edit needed. The PR changes no agent workflow, tooling or validation step.