no_surj_small

formal source

  38  simp [Pattern, Fintype.card_fin] at*
  39
  40/-- No surjection to all d-bit patterns if T < 2^d. -/
  41lemma no_surj_small (T d : Nat) (hT : T < 2 ^ d) :
  42  ¬ ∃ f : Fin T → Pattern d, Function.Surjective f := by
  43  classical
  44  intro h; rcases h with ⟨f, hf⟩
  45  obtain ⟨g, hg⟩ := hf.hasRightInverse
  46  have hginj : Injective g := by
  47    intro y₁ y₂ hgy
  48    have : f (g y₁) = f (g y₂) := by simp [hgy]
  49    simpa [RightInverse, hg y₁, hg y₂] using this
  50  have hcard : Fintype.card (Pattern d) ≤ Fintype.card (Fin T) :=
  51    Fintype.card_le_of_injective _ hginj
  52  have : 2 ^ d ≤ T := by
  53    simpa [Fintype.card_fin, card_pattern d] using hcard
  54  exact (lt_of_le_of_lt this hT).false
  55
  56/-- Minimal ticks lower bound for a complete cover. -/
  57lemma min_ticks_cover {d T : Nat}
  58  (pass : Fin T → Pattern d) (covers : Function.Surjective pass) : 2 ^ d ≤ T := by
  59  classical
  60  by_contra h
  61  exact (no_surj_small T d (lt_of_not_ge h)) ⟨pass, covers⟩
  62
  63/-- For 3-bit patterns, any complete pass has length at least 8. -/
  64lemma eight_tick_min {T : Nat}
  65  (pass : Fin T → Pattern 3) (covers : Function.Surjective pass) : 8 ≤ T := by
  66  simpa using (min_ticks_cover (d := 3) (T := T) pass covers)
  67
  68/-- Nyquist-style obstruction: if T < 2^D, no surjection to D-bit patterns. -/
  69theorem T7_nyquist_obstruction {T D : Nat}
  70  (hT : T < 2 ^ D) : ¬ ∃ f : Fin T → Pattern D, Function.Surjective f :=
  71  no_surj_small T D hT