P34 Host-capacity aliasing

Declarations: P34_capacity_below_entropy_aliasing

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P34_capacity_below_entropy_aliasing
    {nAttack nSignal : Nat}
    (hcard : nSignal < nAttack) :
    ¬ ∃ detect : Fin nAttack → Fin nSignal, Function.Injective detect :=
  not_exists_injective_of_fin_card_lt hcard