Deterministic Policy Section Count

Abstract

Distinct public states with at least two legal actions force exponentially many deterministic sections.

Theorem 1.1 (Legal deterministic sections have an exponential lower bound).

$$\begin{gathered} \forall Q,A,k:\mathrm{Type}, \\ legal:Q\to \mathrm{Set}(A),selected:\mathrm{Fin}\left(k\right)\to Q, \\ \mathrm{Finite}\left(Q\right)\wedge \mathrm{Finite}\left(A\right)\wedge \forall q\in Q,\mathrm{Nonempty}\left(legal(q)\right)\wedge \mathrm{Injective}\left(selected\right)\wedge \forall i\in \mathrm{Fin}\left(k\right),2\le \mathrm{card}(\{a\mid a\in legal(selected(i))\})\Rightarrow 2^k\le \mathrm{card}(\forall q\in Q,\{a\mid a\in legal(q)\}). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Policy/DeterministicPolicySectionCount.deterministic_policy_sections_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

The legal-action relation is the source primitive: every public state has a finite nonempty legal-action fiber. A deterministic section is the dependent product that assigns one subtype element to every public state.

An injectively selected family of k public states has at least two choices in each corresponding fiber. The finite product cardinality theorem therefore gives the lower bound 2^k, while the remaining nonempty fibers can only increase the full section-space cardinality.

The proof uses the exact finite-cardinality and product-order lemmas from pinned Mathlib; no Boolean-only or target-shaped section object is introduced.

References

• Truth anchor: D5/S3/ConceptDynamics/Policy/DeterministicPolicySectionCount.deterministic_policy_sections_lower_bound