[chris-ai1]

This adds enc_structure and uses it for 14 hand-written structure encodings in 9 files, as the "structure encodings are boilerplate" row of #2209. It's refactoring and infrastructure, with no mathematical progress.

This is a draft and needs a design decision before review. It is the generated-encoding request from #1656. crei asked Samuel on #2184 what he thinks of it, and no answer is recorded yet.

This replaces Boosting's State.encoding, its injectivity proof, and its hand-written field and constructor rules:

/-- Reuse the standard Boolean, unary, and list encodings. -/
global enc_structure encoding : State where
  stopped : encBool, threshold : encUnary, predictors : (encList encBits)

Lines. Clients are net −396 (+135, −531). The tool is 206 lines and its tests 120, plus one line in Complexity.lean, so the repository is net −69.

Migrated: Encoded.Edge and Encoded.Graph (PCP), Boosting State and Parameters, SavedPrediction.Description, the TQBF Frame and State, the Savitch Frame and State, LocalCfg and IntervalData, the inductive-counting Runtime, the RAM FiniteState, and MINKT.Instance.

Changes to the command from #2184, each needed by a client here. #2184 should take this version when rebased.

• It also generates eS_f_polyTime and eS_mk_polyTime. Most clients wrote these by hand; the ComputableInDegree and ComputableInO rules alone would have replaced almost nothing.
• It accepts parametric structures (Edge C) and binders. Explicit binders stay explicit on eS and become implicit in rules with hypotheses.
• noncomputable enc_structure covers encodings built on encFinite.
• global enc_structure gives ordinary fun_prop rules. PCP and Boosting clients use these rules across many files, and one of those files is in an open PR, so open scoped everywhere was worse.
• _apply is no longer @[simp]. As simp it unfolded Description.encoding before decode_encoding could fire, which broke SavedPrediction. Universal/Complexity.lean already passes eCfg_apply explicitly in its one use I checked, but refactor(Universal): assemble the step complexity with fun_prop #2184 must recheck the rest. MINKT and the RAM FiniteState keep the attribute with one attribute [simp] line each.

Public changes. Encoded words are unchanged, so no bound or curated abstract statement changes, and no abstract source mentions these encodings. The definitions are now @[expose] and built with .trans.

• Renamed with clients updated and no aliases: State.isPolyTime_{mk,stopped,threshold,predictors}, Parameters.isPolyTime_{mk,confidence,densityNumerator,densityBound,rateBound,codeBound}, Edge.isPolyTime_{mk,src,dst,constraint} and Graph.isPolyTime_{mk,vertices,edges} become encoding_mk_polyTime and encoding_<field>_polyTime. IntervalData.computableInPolyTime_mk becomes encIntervalData_mk_polyTime.
• Removed: Frame.fields and State.fields in TQBF, Frame.fields in Savitch, LocalCfg.equivProd, IntervalData.equivProd.
• The hypothesis of a generated field rule is now named h, and its function g, in place of names such as hedge and edge.
• MINKT.enc_apply and FiniteState.encoding_apply keep their names; they now state encFields, which is a reducible abbreviation of the old encPair term.

Left as they are:

• TM2/Encoding encCfg: its rules are in TM2/Simulation.lean, changed by refactor(resources): replace plain linear computability with degree 1/1 #2177.
• Files in open PRs: QueryReplaySpace and TreeEval/Ary/IterativeEncoding (feat(ExactTriangle): bound initialized native ET by natural subcubic time #2154), ReplacementDesignBuilder, StepMachineComp and ChildCursor (refactor(BigO): assemble computability proofs with fun_prop #2215), MPC/PolyTime (refactor(Crypto): replace projection chains across MPC, GMW, and SigmaProtocol modules (#1764) #2011).
• DescribedNetwork.encDescribed: DirectContraction.lean, in refactor(BigO): assemble computability proofs with fun_prop #2215, uses its equivProd.
• MINcKT.enc and PacketCtx.enc: their tuples nest differently, and matching them would change the encoded words.
• TreeEval/Reader Frame: part of its tuple goes through encFinEnum.
• The private ComputableInSpace field rules in InductiveCounting/Callbacks.lean remain. Replacing them needs a space-level rule in the command.

Universal/ is untouched (#2184), and sum types are #2217.

Validation. At bec86df63, based on 62ca5c214: scripts/check.sh passed all six gates (lake build --wfail --iofail, mk_all --check, lake test --wfail --iofail, lake lint, lint-style, checkInitImports). scripts/check_hygiene.py --check-simp, scripts/check_tidy_surface.py and scripts/check_changed_files.py --base origin/main passed on the same build. No maxHeartbeats changed. Hosted CI should cover the merge with the latest main.

Tracks #2209. Related: #1656, #2184.

AI assistance: Claude Code (Opus 5.5) extended the command, migrated the clients and wrote this description. The original command is crei's, from #2184. This needs independent non-author review once the design is decided.

🤖 Generated with Claude Code