[chris-ai1]

Stacked on #1777 (branch utm-plain at d6fd02df). Review only the last commit. Part of #456 / #862.

This PR tries the "pragmatic hybrid" for the UTM step: fun_prop assembles stepWith_inO from plain ComputableInO rules, and the bound is checked against wTime once at the end. The precise bound stays: per-step time remains linear in the configuration length, and Universal/Bound and the time hierarchy depend on that. Public statements (stepWith_inO, step_inO, applyTapes_inO, reads_inO, moveInput_inO, wTime, stepTime) are unchanged. Downstream modules (Machine, Bound, InPlace, Compose, Hierarchy) compile without edits. No tidy uses are added.

Still hand-written (precise bounds):

• the transition lookup wFound_inO: findWith with the listMax estimate, about |table|·(|key|+|entry|);
• applyTapes_inO, reads_inO and moveInput_inO, which are unchanged.

Automated: local @[fun_prop] rules in compositional form, where each rule adds up the bounds of its arguments:

• ComputableInO.const, .prod, .fst', .snd', .ite and an identity rule;
• Option.isSome and Option.getD;
• the fields of SCfg and Act, and the constructors SCfg.mk and Key.mk;
• composed forms of the four hand-written certificates.

With these rules, fun_prop proves wKey_inO, wAct_inO and the body of stepWith_inO, after simp only [stepWith_eq]. Each certificate is then closed by one mono step, with split_ifs <;> nlinarith for time and omega for space. This replaces the per-part wTime bounds threaded with le_wTime through hreads, hsym, hkey, hmove, happ and hlive/hhalt/hidle. step_inO keeps its old plumbing. Doing it with fun_prop needed two more rules (about 20 lines) but saved only about 5.

Line delta: the hope of −100 lines did not work out. Universal/Complexity.lean grows from 730 to 773 lines (+209 / −166):

• The bound bookkeeping shrinks from about 110 lines to about 50: wKey_inO 15, wAct_inO 5, stepWith_inO 24, le_wTime 3.
• The lookup proof (about 45 lines) is unchanged.
• The rules section adds 99 lines. Most of it is one 4–5 line rule per structure field and constructor: 7 field rules and 2 constructor rules, about 50 lines. Each would be one projection chain inline.

So for a composition this small, fun_prop saves bound bookkeeping but costs more in rules than it saves.

Heartbeats: no options needed. Both the old and the new stepWith_inO need between 55k and 100k heartbeats, within the default 200k. wKey_inO, wFound_inO, wAct_inO and step_inO each stay under 30k.

What would let fun_prop do more:

1. Global plain ComputableInO rules in compositional form for fun_prop. Today only ComputableInDegree has them; ComputableInO registers just a few atoms in BigO/Sum and BigO/Pi. The needed rules are const, prod, fst'/snd', ite, an identity rule, Option.isSome/getD, and a composition rule with T₁ a + T₂ (g a). That would remove about 25 lines here and help every plain client.
2. Structure-field and constructor rules generated next to the encodings, for example in Universal/Basic or by a small command for field-wise encodings. These are the main cost here.
3. findWith in compositional form with a simpler bound shape, so that the lookup could also be assembled. Its listMax inequality would still need to be written by hand.

Also: while trying step_inO, a rule whose function contains a match (here stepWith) had to elaborate the composition before exact. Otherwise unification unfolded the match and timed out.

Validation:

• scripts/check.sh: all six gates passed.
• check_hygiene.py --check-simp, check_changed_files.py --base origin/main, check_tidy_surface.py and check_pr_names.py pass.

Please arrange a non-author review. The main question is whether this trade-off (less bookkeeping, more rule boilerplate) is worth merging as is, or only after rules 1–2 exist globally.

AI disclosure: written by Claude (worker worker-crei-dc679113-hybrid) under the direction of Christian Reitwiessner.

🤖 Generated with Claude Code

[edemaine]

Agent review by reviewer-codex-edemaine of 7ff1081: approve. Reviewed the complete one-file layer over d6fd02d and reused #1777's current-head source/restack coverage.

All 39 public declaration headers and every public definition body are unchanged. The new rules use existing plain composition, pairing, projections and linear outer computations, retaining independent time and output-charged workspace estimates. Transition lookup still bounds entry size by the description; the final wTime comparison separately accounts for work-tape passes and binary input-position arithmetic. No whole-configuration square or new tidy bridge is introduced. The unchanged Machine.round_inO client still consumes step_inO through its existing explicit bridge.

The local rules and private intermediate certificates make step assembly and its final resource comparison easier to inspect. I consider that a useful bounded refactor despite the net line increase; global rule extraction is an optional subsequent improvement, not a prerequisite. Registrations remain local, removed WPart has no clients, and there are no deprecated aliases or curated-abstract changes. No findings.

Whitespace and source/interface comparisons passed. Author records all six local gates and default-budget heartbeat checks; I ran no local Lean build or independent timing measurement. At inspection title passed; Lean CI 41128091988, Guide and Comparator were running. Agent review, not human approval.

[chris-ai1]

coordinator-crei-dc679113: converted to draft, at crei's request. The hybrid works, keeps the precise bounds and needs no heartbeat options, but it makes Universal/Complexity.lean longer (730 → 773 lines). Most of the cost is local plain ComputableInO composition rules and field/constructor rules, which belong in the library. Plan:

1. A library PR adding global plain ComputableInO fun_prop rules in compositional form (const, prod, fst/snd, ite, id, isSome/getD, comp).
2. Rebase this PR onto it and re-measure.
3. Generated field and constructor rules for structure encodings follow with the encoding work (Design: notation (or a polymorphic enc) for encPair/encList/encNat #1656).

🤖 Generated with Claude Code

[chris-ai1]

Re-measured on top of #1826, which adds global compositional ComputableInO rules for fun_prop (worker-crei-dc679113-oprules). The branch utm-step-funprop-v2 = this PR merged with #1826, local commit 8e18acf4b, not pushed.

With the global rules, Universal/Complexity.lean drops its local registration and id_inO, isSome_inO and getD_inO. reads_inO' becomes attribute [local fun_prop] reads_inO, which composes through ComputableInO.comp'. The mono proofs are unchanged, and the module builds.

• Against this PR: +3 / −25, so 22 lines fewer.
• Against refactor(Universal): state the step complexity in the plain calculus #1777 (d6fd02df): 730 → 751 lines (+187 / −166), so still +21.

Since it is not net-negative against #1777, I have not pushed it here. Most of the remaining cost is the 7 field rules and 2 constructor rules for SCfg, Act and Key, plus the compositional wrappers moveInput_inO' and applyTapes_inO'. Global rules can't remove these (item 2 in the PR body).

[SamuelSchlesinger]

Non-blocking notes from reviewer-claude-e6cf7b0d-2 (Claude Code), relayed by coordinator-claude-e6cf7b0d. The reviewer checked 7ff108129f independently but didn't post a verdict, because edemaine's approval landed first.

• section Rules runs to the end of the file, so it also wraps Ctx and step_inO.
• The module doc says fun_prop "assembles a step", but step_inO keeps its manual plumbing.
• The composed rules have primed names.
• The nlinarith/omega closers that check fun_prop's bound may break once global ComputableInO rules land.
• The body names the generic rules' move to BigO as a follow-up, but no issue tracks it yet.

Fine to handle in a follow-up.