[prevostad]

This PR defines the transductive best-answer task of linear identification, transductiveTask ν z, and proves the closure of its alternatives as a finite union of half-spaces. This is the Identification roadmap's Layer 9.1 (Linear tasks): "For a finite set 𝒵 of answers in E, define the transductive best-answer task argmax_{z∈𝒵}⟨z,θ⟩ [FJJR19]; best arm identification is the case 𝒵=φ(α)."

Generalised baiTask (Identification/Task/Classical.lean): baiTask ν mean now takes mean : Θ → ι → ℝ with an arbitrary answer type ι (previously ι = α). Its API (correct_baiTask, subsingleton_correct_baiTask, correct_baiTask_eq_singleton_iff, isSingleAnswer_baiTask) and the MeanFunctional material of Identification/Task/BestArm/Basic.lean (mem_alt_baiTask_iff, mem_answerSet_baiTask_iff, charTime_baiTask_eq_inv_answerValue, …) hold at this generality unchanged. Every existing use is the case ι = α and needs no change.

Openness (Identification/Task/BestArm/Basic.lean): new isOpen_answerSet_baiTask_of_continuous: for finitely many answers and a mean functional continuous in the model, the answer sets of baiTask ν mean are open. isOpen_answerSet_baiTask (the case mean = id) is now derived from it.

New file LMLExplore/Identification/Task/Transductive.lean, in LMLExplore.Identification:

• transductiveTask ν z : IdentTask α E ι 𝓨 is the abbrev baiTask ν (fun θ i ↦ ⟪z i, θ⟫): models θ in a real inner product space E, answers a family z : ι → E (a finite set 𝒵 ⊆ E is the case (↑) : 𝒵 → E), correct answer the i with the largest ⟪z i, θ⟫, admissible models those with a unique best answer. Its single-answer property, alternatives, answer sets (open by isOpen_answerSet_baiTask_of_continuous) and characteristic time T*(θ) = D(θ, ¬i)⁻¹ are those of baiTask. Linear best arm identification is transductiveTask ν φ = baiTask ν (fun θ a ↦ ⟪φ a, θ⟫), the roadmap's "best arm identification is the case 𝒵 = φ(α)"; as Layer 9.1 asks, the linear tasks get no separate definitions.
• closure_alt_transductiveTask: for finitely many distinct answers, closure (alt i) = ⋃ j : {j // j ≠ i}, {λ | ⟪z i - z j, λ⟫ ≤ 0}, and mem_closure_alt_transductiveTask proves the hard inclusion. Starting from a point where some j ≠ i scores at least as much as i, take, among the best answers other than i, the one farthest from z i, and move along the direction from z i to it. This gives a unique best answer other than i. The injectivity hypothesis is needed: with z i = z j for some j ≠ i, the answer i is never correct, and the right-hand side is all of E while the alternatives need not be dense.
• altCost_transductiveTask_eq_iInf: for a transportation cost continuous on these half-spaces, D(θ, w, ¬i) = min_{j ≠ i} inf {cost_θ(w, λ) | ⟪z i - z j, λ⟫ ≤ 0}. This follows from IdentTask.altCost_eq_biInf_of_subset_closure.

Consumer: Layer 9.2 (Characteristic time) states T*(θ)⁻¹ = max_w min_{z ≠ z*} ⟨θ, z* - z⟩² / (2 ‖z* - z‖²_{V_w⁻¹}) "as the case of the half-spaces {λ : ⟨z* - z, λ⟩ ≤ 0} of Layer 3.6". closure_alt_transductiveTask has exactly the shape of the two closure hypotheses (h_alt, h_closure, with y j = z i - z j and c j = 0) of IdentTask.altCost_gaussianReal_inner and IdentTask.answerValue_gaussianReal_inner in the open PR #362, which is independent of this one. With charTime_baiTask_eq_inv_answerValue, these two give 9.2. Nothing here depends on #362.

Layer 9.1 is complete after this PR. Layer 9 still needs 9.2 (once #362 lands), the RAGE elimination algorithm of 9.3 (which also needs the phased-elimination constructor of Layer 0.5) and the GLRT and asymptotic optimality results of 9.4.

Mathematical source: T. Fiez, L. Jain, K. Jamieson and L. Ratliff, Sequential experimental design for transductive linear bandits, NeurIPS 2019, Section 2 and Theorem 1, cited in the file. The API and the closure statement follow the existing baiTask material in Identification/Task/Classical.lean and Identification/Task/BestArm/Basic.lean. No Mathlib material is vendored. Nothing is renamed or removed.

Roadmap: Identification

🤖 Generated with Claude Code

[prevostad]

🟡 reuse — request_changes claude/claude-opus-5-5

The earlier copies of the baiTask API are gone: transductiveTask is now an abbrev of the generalised baiTask, and the closure and altCost results are new. isOpen_answerSet_transductiveTask still repeats the proof of isOpen_answerSet_baiTask, and one general lemma for a continuous mean would cover both.

• LMLExplore/Identification/Task/Transductive.lean:81 — isOpen_answerSet_transductiveTask copies the proof of isOpen_answerSet_baiTask (BestArm/Basic.lean:238-245): the same mem_answerSet_baiTask_iff/simp rewrite into ⋂ j ∈ {i}ᶜ, {mean · j < mean · i}, then isOpen_biInter and isOpen_lt, with different continuity terms. This PR already widens baiTask to mean : Θ → ι → ℝ, so one lemma can serve both. Fix: Generalise isOpen_answerSet_baiTask to [TopologicalSpace Θ] [Finite ι] (hmean : ∀ b, Continuous fun θ ↦ mean θ b) (a : ι) : IsOpen ((baiTask ν mean).answerSet a), proved with isOpen_lt (hmean b) (hmean a). Get the id case from continuous_apply and update isOpen_answerSet_baiTask_restrict. Get the transductive case as isOpen_answerSet_baiTask ν (fun j ↦ continuous_const.inner continuous_id) i, or delete the transductive copy.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 23s · 88.1k in (54.6k cache read, 33.5k cache write) / 2.4k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[prevostad]

🟡 generality — request_changes claude/claude-opus-5-5

The earlier duplication is fixed: baiTask now takes an answer type ι and transductiveTask is an abbrev for it. One special-case proof remains: isOpen_answerSet_transductiveTask repeats the proof of isOpen_answerSet_baiTask, and both should come from one openness lemma for a continuous mean functional.

• LMLExplore/Identification/Task/Transductive.lean:82 — isOpen_answerSet_transductiveTask repeats the proof of isOpen_answerSet_baiTask (BestArm/Basic.lean:238-245), changing only the continuity witness from continuous_apply to continuous_const.inner continuous_id. Both are special cases of one statement about a continuous mean functional. Fix: In the MeanFunctional section of BestArm/Basic.lean, add lemma isOpen_answerSet_baiTask_of_continuous [TopologicalSpace Θ] [Finite ι] (hmean : ∀ a, Continuous fun θ ↦ mean θ a) (a : ι) : IsOpen ((baiTask ν mean).answerSet a). Derive isOpen_answerSet_baiTask from it with continuous_apply, and derive the transductive lemma from it with fun j ↦ continuous_const.inner continuous_id, or drop the transductive lemma.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 19s · 77.6k in (51.6k cache read, 25.9k cache write) / 1.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[prevostad]

AI review — changes requested

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
♻️	correctness	stale (re-run pending)	claude/claude-opus-5-5	The transductive task, its correct-answer set and the closure of its alternatives as a union of half-spaces faithfully formalize FJJR19's argmax_{z∈𝒵}⟨z,θ⟩ task under a necessary and natural injectivity hypothesis. The cost and characteristic-time statements are correct instances of the existing IdentTask API with no hidden content in their hypotheses.
🟡	reuse	changes requested	claude/claude-opus-5-5	The earlier copies of the baiTask API are gone: transductiveTask is now an abbrev of the generalised baiTask, and the closure and altCost results are new. isOpen_answerSet_transductiveTask still repeats the proof of isOpen_answerSet_baiTask, and one general lemma for a continuous mean would cover both.
♻️	scope	stale (re-run pending)	claude/claude-opus-5-5	New material directly implements Identification README Layer 9.1 (transductive best-answer task, BAI as the case z = φ, no separate linear task definitions), and the closure/altCost/charTime results supply the half-space form Layer 9.2 explicitly calls for. Single coherent topic with no bundled refactor.
♻️	attribution	stale (re-run pending)	claude/claude-opus-5-5	The file cites the informal source [FJJR19] (Fiez, Jain, Jamieson, Ratliff, NeurIPS 2019) in its module docstring, definition and cost theorem, and links the in-repo baiTask material it follows; no Mathlib material is vendored. The closure proof is not lifted from the existing closure_alt_baiTask proof, and the roadmap is credited only in the PR description.
♻️	api-design	stale (re-run pending)	claude/claude-opus-5-5	The surface mirrors the established baiTask API (field simp lemmas proved by (rfl), uniqueness, single-answer, mem_alt/mem_answerSet, openness, closure, altCost and charTime) with no exposed body, no compatibility leftovers and no hidden general infrastructure. The characterizing API is complete for this layer and annotated consistently with baiTask.
🟡	generality	changes requested	claude/claude-opus-5-5	The earlier duplication is fixed: baiTask now takes an answer type ι and transductiveTask is an abbrev for it. One special-case proof remains: isOpen_answerSet_transductiveTask repeats the proof of isOpen_answerSet_baiTask, and both should come from one openness lemma for a continuous mean functional.
♻️	placement	stale (re-run pending)	claude/claude-opus-5-5	The new transductive-task file sits in the existing Identification/Task directory, next to the other task definitions, and every declaration is specific to that task. Its three imports (Classical for baiTask, TransportationCost for the altCost/charTime lemmas, InnerProductSpace.Basic) are each used and none is overly broad.
♻️	naming	stale (re-run pending)	claude/claude-opus-5-5	Every new name mirrors the existing baiTask API (correct_/subsingleton_/isSingleAnswer_/mem_alt_…iff/closure_alt/altCost_…eq_iInf/charTime…_eq_inv_answerValue), and no name claims more than its statement proves. Declarations sit in LMLExplore.Identification and no notation is introduced.
♻️	documentation	stale (re-run pending)	claude/claude-opus-5-5	The module docstring and every public declaration's docstring accurately describe the transductive task, its API, the closure of the alternatives and the cost identity, without overclaiming or process narrative.
✅	proof-quality	approved	claude/claude-opus-5-5	The closure argument now lives in a commented private helper lemma (eventually_forall_inner_lt_inner_add_smul) about 37 lines long, which resolves the earlier length and buried-reasoning finding. The remaining proofs are short, use only local rewrites and linear arithmetic, and do not rely on undocumented definitional equality.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 898f4d8. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.92.}

[RemyDegenne]

🟡 documentation — request_changes claude/claude-opus-5-5

The new transductive file and its public declarations are documented accurately. The generalised baiTask docstring still gives the old type mean : Θ → α → ℝ, which no longer matches its signature.

• LMLExplore/Identification/Task/Classical.lean:113 — The baiTask docstring opens with "the mean functional mean : Θ → α → ℝ", but the variable is now mean : Θ → ι → ℝ (line 111). The docstring was not updated when the definition was generalised, so it contradicts the signature. Fix: Rewrite the first sentence with mean : Θ → ι → ℝ and answers ι, and say that classical best arm identification is the case ι = α. Merge this with the 'More generally' paragraph instead of keeping both.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 22s · 45.7k in (39.2k cache read, 6.5k cache write) / 2k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	transductiveTask is faithfully baiTask on the values ⟪z i, θ⟫, matching FJJR19's best-answer task. The closure-of-alternatives statement is the correct half-space union, its injectivity hypothesis is necessary, and the edge cases are consistent.
✅	reuse	approved	claude/claude-opus-5-5	The transductive closure result is new material with no existing counterpart: the closure_alt_baiTask lemmas only cover baiTask ν id on α → ℝ, and Task/HalfSpace.lean has no closure lemma. The PR reuses baiTask, IdentTask.altCost_eq_biInf_of_subset_closure and Mathlib's eq_of_norm_le_re_inner_eq_norm_sq, and now derives isOpen_answerSet_baiTask from the new general openness lemma instead of repeating its proof.
✅	scope	approved	claude/claude-opus-5-5	The PR delivers roadmap Identification Layer 9.1 (the transductive best-answer task [FJJR19]), plus the half-space closure that leads directly to Layer 9.2. The generalisation of baiTask to an answer type ι and the openness lemma are modest generalisations of merged code that the new definition needs, so the PR is one coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The new transductive file credits its central informal source, FJJR19 (Section 2 and Theorem 1), in its References and in the relevant docstrings. The closure proof and the generalisation of baiTask are routine or rework the project's own code, with no uncredited outside source.
✅	api-design	approved	claude/claude-opus-5-5	The public surface is minimal: transductiveTask is a deliberate abbrev of the widened baiTask, so the existing baiTask lemmas apply to it directly, and the new closure and cost theorems are exported for Layer 9.2. The only private lemma depends on how this proof picks its answer, and nothing is kept around only for compatibility.
✅	generality	approved	claude/claude-opus-5-5	Generalising baiTask to an arbitrary answer type ι and deriving isOpen_answerSet_baiTask from the new continuous-mean openness lemma put the material at the natural level, and the transductive task reuses that API instead of duplicating it. Every hypothesis in Transductive.lean (Finite ι, injectivity of z, Fintype α, the real inner product space) is used in an essential way.
✅	placement	approved	claude/claude-opus-5-5	The new transductive task file sits in the existing Identification/Task/ directory next to the other task files, the baiTask generalisation and its openness lemma stay in their existing homes, and the imports are specific and used.
✅	naming	approved	claude/claude-opus-5-5	New names (transductiveTask, closure_alt_transductiveTask, mem_closure_alt_transductiveTask, altCost_transductiveTask_eq_iInf, isOpen_answerSet_baiTask_of_continuous) describe their conclusions and match the adjacent baiTask names such as altCost_baiTask_restrict_eq_iInf, and the PR adds no notation.
✅	documentation	approved	claude/claude-opus-5-5	The new module docstring and every new or generalised public declaration are documented accurately, without process narrative or overclaiming. The baiTask generalisation to an answer type ι is reflected in its docstring, the Classical module summary, and the BestArm/Basic statement index.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are robust, use no change/show or hidden defeq, and the one substantial argument is split into a commented private lemma; the openness proof is generalised and reused instead of duplicated.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 6a7acb6. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.05.}