IndisputableMonolith.CrossDomain.AttentionSpace

   1import Mathlib
   2
   3/-!
   4# C5: Attention Space — 5 × 8 = 40, + 5 = gap45 — Wave 62 Cross-Domain
   5
   6Structural claim: attentional state space factors as
   7
   8  AttentionNetwork × TickPhase  =  5 × 8  =  40
   9
  10and the complexity ceiling gap45 = 45 leaves exactly 5 overflow slots:
  11  45 − 40 = 5.
  12
  13The overflow slots are the five attention-network singletons under
  14saturation. Prediction: attentional-blink experiments should show 40 stable
  15plateaus plus 5 transient ones, matching the five singletons.
  16
  17Lean status: 0 sorry, 0 axiom.
  18-/
  19
  20namespace IndisputableMonolith.CrossDomain.AttentionSpace
  21
  22inductive AttentionNetwork where
  23  | alerting | orienting | executive | defaultMode | salience
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26inductive TickPhase where
  27  | t0 | t1 | t2 | t3 | t4 | t5 | t6 | t7
  28  deriving DecidableEq, Repr, BEq, Fintype
  29
  30theorem networkCount : Fintype.card AttentionNetwork = 5 := by decide
  31theorem tickCount : Fintype.card TickPhase = 8 := by decide
  32theorem tick_eq_twoPowD : Fintype.card TickPhase = 2 ^ 3 := by decide
  33
  34abbrev AttentionState : Type := AttentionNetwork × TickPhase
  35
  36theorem attentionStateCount : Fintype.card AttentionState = 40 := by
  37  simp only [AttentionState, Fintype.card_prod, networkCount, tickCount]
  38
  39/-- The complexity ceiling gap45 leaves exactly 5 overflow slots. -/
  40def gap45 : ℕ := 45
  41theorem overflow_eq_D : gap45 - Fintype.card AttentionState = 5 := by
  42  rw [attentionStateCount]; decide
  43
  44theorem attention_fits_under_gap : Fintype.card AttentionState < gap45 := by
  45  rw [attentionStateCount]; decide
  46
  47theorem attention_plus_overflow_eq_gap :
  48    Fintype.card AttentionState + 5 = gap45 := by
  49  rw [attentionStateCount]; decide
  50
  51theorem network_surj :
  52    Function.Surjective (fun s : AttentionState => s.1) := by
  53  intro x; exact ⟨(x, TickPhase.t0), rfl⟩
  54
  55theorem tick_surj :
  56    Function.Surjective (fun s : AttentionState => s.2) := by
  57  intro x; exact ⟨(AttentionNetwork.alerting, x), rfl⟩
  58
  59structure AttentionSpaceCert where
  60  state_count : Fintype.card AttentionState = 40
  61  overflow_D : gap45 - Fintype.card AttentionState = 5
  62  sum_is_gap : Fintype.card AttentionState + 5 = gap45
  63  tick_2cube : Fintype.card TickPhase = 2 ^ 3
  64  network_surj : Function.Surjective (fun s : AttentionState => s.1)
  65  tick_surj : Function.Surjective (fun s : AttentionState => s.2)
  66
  67def attentionSpaceCert : AttentionSpaceCert where
  68  state_count := attentionStateCount
  69  overflow_D := overflow_eq_D
  70  sum_is_gap := attention_plus_overflow_eq_gap
  71  tick_2cube := tick_eq_twoPowD
  72  network_surj := network_surj
  73  tick_surj := tick_surj
  74
  75end IndisputableMonolith.CrossDomain.AttentionSpace
  76