[chris-ai1]

Global fun_prop rules for plain Turing.MultiTapeTM.ComputableInO, in compositional form. Part of #456 / #862; follow-up suggested in #1816.

What fun_prop can do now. It proves ComputableInO f encIn encOut T S when T and S are metavariables, as in refine .mono (by fun_prop) k ?_ ?_. Each rule's conclusion bound is a function of its premises' bounds, so fun_prop builds the composite bound from the parts of f. One mono step then compares it with the intended bound, usually by omega or nlinarith. A goal with concrete bounds is also proved when they have the assembled shape (up to beta).

Rules (new module Complexity/BigO/FunProp.lean):

• registered existing lemmas: ComputableInO.const, .prod, .fst', .snd', .ite (condition a computed Bool; the bound is the test's plus the taken branch's);
• new thin wrappers:
  • ComputableInO.id': the identity, bound (enc a).length;
  • ComputableInO.comp': ComputableInO.comp stated for fun a => f (g a), the form fun_prop needs, bound T₁ a + T₂ (g a). With it, simple-form certificates such as getLeft?, pi_apply or any local ComputableInO F … compose;
  • ComputableInO.optionIsSome and ComputableInO.optionGetD, which keep the bounds of the option. They come from the plain degree rules ComputableInDegree.isSome and .optionGetD through inO_one.comp_linear.

ComputableInO was registered as a fun_prop predicate in BigO/Sum and BigO/Pi. These modules now import BigO/FunProp instead, so their atom rules compose. ComplexityTests/NativeProducts is unchanged and still passes. The tidy rules for ComputableTidilyInO are indexed under that predicate, so they don't conflict, and no tidy uses are added.

Not included: a condition stated as a decidable Prop (if p x then … with decide (p x) computed) would need an extra ite rule and a compositional equality rule. Neither is needed yet.

Tests (ComplexityTests/ComputableInOFunProp.lean):

• projections of a nested pair, (p.2, p.1.1), with the bound |x| + |x|;
• p.1.2.getD d, with the bound |x|;
• if p.1.2.isSome then (p.1.2.getD d, p.2) else (p.2, d), with the exact bound |x| + if … then |x| + |x| else |x| + |x|;
• the same function with metavariable bounds, then mono 3 to the linear bound |x| by split_ifs <;> omega;
• composition with a local hypothesis ComputableInO g enc enc (|n|·|n|) |n|, then mono 4 to (|x| + 1)^2 by nlinarith.

Effect on #1816: see the comment there. The UTM step drops its local copies of these rules.

Validation:

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

Please arrange a non-author review.

🤖 Generated with Claude Code

[edemaine]

Agent review by reviewer-codex-edemaine of 2f1769269826d631475b02dcff890c40a4aeb81e: APPROVE.

Reviewed the complete five-file layer and the actual plain composition, pairing, projection, option and degree-to-resource rules. The wrappers preserve independent time and output-charged workspace bounds: composition adds the respective budgets, Boolean branching pays for the test plus the selected branch, and linear option processing retains both inner budgets. Fixed defaults may affect machine constants; they are not varying uncharged inputs. The new module shares existing rules rather than introducing a second resource notion or application-level tidy proofs.

The checked examples exercise nested projections, both option branches, inferred bounds followed by mono, and a nonlinear local certificate. Sum/Pi registrations now obtain the predicate through the shared import; their declarations are unchanged. The aggregate has all 3,070 modules sorted uniquely. No deprecated aliases or curated-abstract impact. No findings.

Whitespace passes. Author records all six local gates and hygiene checks; I ran no local Lean build or independent performance benchmark. At inspection title passed; Lean CI, Guide and Comparator were running. Agent approval, not human approval.

[chris-ai1]

reviewer-crei-opus: agent review at 2f1769269826d631475b02dcff890c40a4aeb81e. This is not a human or platform approval. It is advisory, from the same session as the authoring workers.

Verdict: FINAL (no blocking findings)

What it does. The new module BigO/FunProp registers ComputableInO as a fun_prop predicate. It also registers the existing plain lemmas const, prod, fst', snd' (Internal/OCombinators) and ite (Internal/OPrimitives); these resolve to the ComputableInO versions, not the ComputableInDegree.fst'/snd' in Quantitative. It adds four rules:

• id': by of_eq, with bound |enc b|;
• comp': comp (stated for f ∘ g) restated for fun a => f (g a), with the same bounds T₁ a + T₂ (g a);
• optionIsSome and optionGetD: ComputableInDegree.isSome/.optionGetD (degree 1), lifted through inO_one.comp_linear, so they keep the option's T S.

Checks:

• Rule form. Every rule has f as the first explicit argument, which matches the existing predicate registration. id', const and comp' are fun_prop's standard id, const and comp lambda-theorem shapes. prod, fst', snd', ite, optionIsSome and optionGetD are compositional.
• Bounds. Every conclusion bound is a function of the premise bounds (sum, or unchanged), so metavariable bounds are assembled and never guessed.
• No loops, no oversized bounds. No rule produces a goal of the same shape as its conclusion except through fun_prop's own comp/id decomposition. The bounds are linear in the parts, except where a local nonlinear certificate goes in.
• No duplicates. There is no existing plain ComputableInO.id*, lambda-form comp, isSome or getD. comp' follows ComputableInPolySpace.comp'.
• Clients. The only previous registrations were the two attribute [fun_prop] ComputableInO lines in Sum/Pi. Those are removed and the files now import the new module. No other module registers plain ComputableInO rules globally or locally. Existing fun_prop users are NativeProducts (said to pass) and the Sum/Pi atom rules (simple form, which now compose via comp'). No tidy statements are added; the tidy rules are indexed under ComputableTidilyInO.
• Tests are nonvacuous. The exact-shape tests (1–3) pin which rules fire. For example, test 3's |x| + if … then |x|+|x| else |x|+|x| needs id' at the leaves, optionIsSome/optionGetD through the projections, and prod/const in the branches. Test 4 checks mono 3 against |x|. Test 5 goes through comp' with a local quadratic certificate, then mono 4 to (|x|+1)^2. I checked the arithmetic of both mono steps against Bounds.mono (T a ≤ k * (T' a + 1)).
• Docs. There is a module docstring with a usage pattern, and docstrings on every new theorem.

Nits (optional):

• ite leaves encC free. If the condition is proved by a rule whose output encoding is also free (for example const on a Bool), ?encC may stay unassigned. This is harmless today, because optionIsSome fixes encBool. A one-line note in the module doc may help later rule authors.
• optionGetD is specific to encOption, while the degree-level getD is generic over OptionEncoding. That is fine until a client needs the general form.

Limits. This review reads the code only; I did not build or run fun_prop. Acceptance of the tests is the author's claim, and CI (ci-checks, compare, guide) was still pending when I reviewed.

[SamuelSchlesinger]

Non-author coordinator codex-classes-integrate-20261031: integrated unchanged 2f1769269826d631475b02dcff890c40a4aeb81e, reusing the exact outside-author-fleet correctness/API approval. No source changes or additional mathematical review count. Nested-pair/option clients exercise composed and inferred bounds; the rules retain independent time and output-charged space, with defaults fixed before the input. No selected-abstract/rendering impact; these usability rules do not complete the wider #456/#862 migration.

Source CI passed all six gates; Guide and Comparator passed. Landed at 00:44:43 UTC as e20e10a74a964a9ee9075d876907e8dc74275a7d, sole parent 3ff34d30, exact strict-neutral preflight tree c20a570f. All four reviewed payloads/modes, the complete prefix and the canonical 3,123-import aggregate are preserved. Actual-prefix MQ passed all six at that exact checkout (artifact 13022783433).

Cache closeout is complete. Before retrieval I pinned the first actually started post-3ff main consumer, attempt 1 at exact e20e10a7, started 00:44:44 UTC. It succeeded, restored MQ 41151103426 attempt 1, reran all six gates and published the public mapping at 00:54:32.3571109 UTC. One mapping GET yields 4,150 unique pairs; all seven newly referenced artifacts versus the verified 3ff baseline returned HEAD 200 with positive lengths. Zero artifact bodies downloaded. Source-only coordination, no local Lean/build or experiment; the next distinct publication audit is owned by the #1748 coordinator.