Bar-recursive choice theorem boundary

The classical source is $\mathrm{WE}\text{-}{\mathsf{PA}}^{\omega }+\mathsf{QF}\text{-}\mathsf{AC}+{\mathsf{AC}}_{\mathbb{N}}$. The verifying target is $\mathrm{WE}\text{-}{\mathsf{HA}}^{\omega }+\mathsf{SBR}$. Chapter 66’s first-order Dialectica proof gives the clause schema but is not misreported as this higher-type soundness theorem.

The applied binary product, finite product equations, finite DNS matrix, complete finite-choice instance, exact finite type levels, prefix factorization, controlled-product equations, adjusted selectors for $R\times \mathbb{N}$, Spector’s condition, and the BI totality argument.

Simple eps defines dependent EPS in System T, and EPS defines SBR in the weak finite-type base. Powell proves dependent EPS and SBR primitive-recursively equivalent. Returning all the way to the simple eps used for the controlled equations instead factors through BR, EPQ, epq, and eps; that comparison assumes ${\mathrm{BI}}_{\mathrm{rel}}$ twice and SPEC on the BR-to-EPQ edge.

Restricted SBR realizes ${\mathsf{DNS}}_{\mathbb{N}}$ and therefore ${\mathsf{cAC}}_{\mathbb{N}}$, the negative translation of countable choice. It is not claimed to realize an un-translated classical choice axiom inside an intuitionistic target.

Totality holds in the total continuous functionals under the displayed ${\mathrm{BI}}_{\mathrm{dec}}$ principle. The result is not a System T definability theorem or strong normalization of unrestricted bar-recursive rewrite equations.

The Kappa corpus checks binary and three-selection products plus one fuel-bounded control case. The archived Agda project carries a dependent finite-pigeon specification but was not freshly typechecked under its historical toolchain. Neither artifact proves semantic totality.