proof

P34 Host-capacity aliasing

Host-capacity aliasing (pigeonhole)

Spine theorem: AlignmentProofSpine.P34_capacity_below_entropy_aliasing

Lean spine source

Declarations: P34_capacity_below_entropy_aliasing

From the machine-checked spine in formal/ (Mathlib + spine imports). 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

Axiom footprint (headline check)

Classical.choice
Quot.sound
propext