3. Explore-Then-Commit

Plain-English statement. The canonical Rat ETC commit oracle selects the least encoded arm among all arms tying its maximal score.

Intuition

The strict-update fold scans arms in canonical order: a strictly better score replaces the current arm, while an equal score leaves the earlier arm in place.

Why it is needed

The generated ETC policy needs deterministic, explicit tie behavior; maximality alone does not identify which maximizing action is selected.

Place in the proof

This deterministic leaf closes the tie-semantics edge between the concrete Rat commit oracle and the canonical measurable generated ETC route.

Proof idea

Identify the fold with Mathlib's first-occurrence List.argmax, compare the selected arm's list index with any tying maximizer using index_of_argmax, and rewrite finRange indices as encodings.

Lean reading notes

The only substantive assumptions are finite Rat scores and 0<K. No measure, independence, MGF, or unique-maximum assumption is introduced.

Teaching dependencies

BanditRLProof.ETC.argmaxCommitOracle

theorem argmaxCommitOracle_encode_le_of_score_le {K : Nat} (hK : 0 < K) (scores : Fin K -> Rat) (a : Fin K) (hscore : scores ((ETC.argmaxCommitOracle hK).choose scores) <= scores a) : Encodable.encode ((ETC.argmaxCommitOracle hK).choose scores) <= Encodable.encode a

Plain-English statement. For the generated Explore-Then-Commit policy under finite-arm sub-Gaussian reward laws, expected Real pseudo-regret is bounded by the canonical per-arm exploration-plus-commit expression.

Intuition

Exploration pays a deterministic cost; exploitation pays only when empirical noise makes the commit oracle choose the wrong arm.

Why it is needed

This is a concrete end-to-end local ETC theorem rather than only a tail lemma or theorem card.

Place in the proof

Together with the generated-law, round-robin, least-tie, and named wrong-commit declarations in the public canary, it closes the scoped local ETC chapter; direct imported-LML identity remains separate.

Proof idea

Prove empirical-mean measurability, reduce a wrong commit to a pairwise deviation event, apply the sub-Gaussian tail contract, and integrate the deterministic regret split.

Lean reading notes

The Real integral is explicit. The bound and every arm-law regularity hypothesis are visible in the Lean statement; no LML theorem card is used as a proof term.

Teaching dependencies

BanditRLProof.pseudoRegret_eq_finset_sum_gap_mul_pullCount

theorem integral_real_pseudoRegret_explorationArgmaxGeneratedAction_le_canonicalSubGaussianArmPerArmIntegralRegretBoundReal {K : Nat} {Context : Type} [MeasurableSpace Context] (spec : ETC.Spec K) (model : FiniteBanditModel K) (armLaw : Fin K -> Measure Rat) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (sigma2 : NNReal) (hmean : forall arm, integral (armLaw arm) (fun reward : Rat => (((reward : Rat) : Real))) = (((model.mean arm : Rat) : Real))) (hsubG : forall arm, ProbabilityTheory.HasSubgaussianMGF (fun reward : Rat => ((reward : Rat) : Real) - (((model.mean arm : Rat) : Real))) sigma2 (armLaw arm)) (context : (n : Nat) -> ((j : Finset.Iic n) -> Rat) -> Context) (hcontext : forall n : Nat, Measurable (context n)) (hexplorationPulls_pos : 0 < spec.explorationPulls) (r : Nat) : let defaultAction := ETC.exploreArm spec 0 let rewardKernel := RewardKernel.contextIndependentOfActionLaws (Context