BanditRLProof.Algorithms.ETCTraceCountLemmas

On any prefix contained inside the configured exploration horizon, the fixed-commit ETC trace has the same pull counts as the pure round-robin exploration trace. This is the `ETC-ACTION-WITH-COMMIT-EXPLORE-PREFIX-PULLCOUNT` project-local trace/count transfer leaf.

theorem ETC.pullCount_actionWithCommit_eq_pullCount_exploreArm_of_le {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (n : Nat) (hn : n <= spec.explorationPulls * K) : pullCount (ETC.actionWithCommit spec commitArm) a n = pullCount (ETC.exploreArm spec) a n

At the configured exploration horizon, the fixed-commit ETC trace has pulled each arm exactly `spec.explorationPulls` times. This is the `ETC-ACTION-WITH-COMMIT-EXPLORATION-HORIZON-COUNT` project-local trace/count adapter.

theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_eq {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) : pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K) = spec.explorationPulls

At the configured exploration horizon, every arm in the fixed-commit ETC trace has a positive pull count whenever the configured number of exploration pulls is positive. This is the first denominator-positivity leaf for future empirical-mean construction. It stays purely deterministic and Nat-valued.

theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_pos {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (hexplorationPulls_pos : 0 < spec.explorationPulls) : 0 < pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K)

Rat-cast form of the fixed-commit ETC exploration pull-count positivity leaf. This is the first denominator adapter for future Rat-valued empirical means. It only transports the compiled Nat positivity theorem across the Nat-to-Rat cast.

theorem ETC.ratCast_pullCount_actionWithCommit_explorationPulls_mul_K_pos {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (hexplorationPulls_pos : 0 < spec.explorationPulls) : (0 : Rat) < (pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K) : Rat)

Nonzero Rat-denominator form of the fixed-commit ETC exploration pull-count positivity leaf. This is still only a deterministic denominator adapter. It does not define empirical means or introduce probability assumptions.

theorem ETC.ratCast_pullCount_actionWithCommit_explorationPulls_mul_K_ne_zero {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (hexplorationPulls_pos : 0 < spec.explorationPulls) : Not ((pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K) : Rat) = 0)

After the configured exploration horizon, one step of the fixed-commit ETC trace updates pull counts according to whether the queried arm is the commit arm. This is the `ETC-ACTION-WITH-COMMIT-POST-COMMIT-SUCC-COUNT` project-local trace/count update leaf.

theorem ETC.pullCount_actionWithCommit_succ_eq_add_if_commitArm_of_ge {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) {t : Nat} (ht : spec.explorationPulls * K <= t) : pullCount (ETC.actionWithCommit spec commitArm) a (Nat.succ t) = pullCount (ETC.actionWithCommit spec commitArm) a t + if commitArm = a then 1 else 0

After the configured exploration horizon, the fixed-commit ETC trace has a closed-form pull count: the commit arm receives every suffix pull, while all other arms keep their exploration-horizon count. This is the `ETC-ACTION-WITH-COMMIT-SUFFIX-COUNT` project-local trace/count closed-form leaf.

theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq {K : Nat} (spec : ETC.Spec K) (commitArm a : Fin K) (r : Nat) : pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K + r) = spec.explorationPulls + (if commitArm = a then r else 0)

After the configured exploration horizon, every non-commit arm keeps its exploration-horizon pull count. This is the `ETC-ACTION-WITH-COMMIT-NONCOMMIT-SUFFIX-COUNT` project-local trace/count corollary.

theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq_of_ne {K : Nat} (spec : ETC.Spec K) {commitArm a : Fin K} (hne : commitArm ≠ a) (r : Nat) : pullCount (ETC.actionWithCommit spec commitArm) a (spec.explorationPulls * K + r) = spec.explorationPulls

After the configured exploration horizon, the commit arm has the exploration count plus every suffix pull. This is the `ETC-ACTION-WITH-COMMIT-COMMITARM-SUFFIX-COUNT` project-local trace/count corollary.

theorem ETC.pullCount_actionWithCommit_explorationPulls_mul_K_add_eq_commitArm {K : Nat} (spec : ETC.Spec K) (commitArm : Fin K) (r : Nat) : pullCount (ETC.actionWithCommit spec commitArm) commitArm (spec.explorationPulls * K + r) = spec.explorationPulls + r