1. Access Structure🔗

Definition of Access Structure. Suppose there are n participants, represented by the term 0, 1,..., n-1 in Fin n. Denote the set of all participants by \mathcal{P}.

A secret sharing scheme distributes a secret s among the participants in \mathcal{P} such that only specific subsets of participants can reconstruct s. The collection of these qualified subsets is formally defined as an access structure.

An access structure consists of a set \Gamma of subsets of \mathcal{P} and a proof that this set of sets is satisfies the monotone property.

An access structure \Gamma is said to be monotone if for all A \in \Gamma and B \subseteq \mathcal{P},

A \subseteq B \implies B \in \Gamma.

import Mathlib.Tactic

noncomputable section AccessStructure

structure AccessStructure (n : ℕ) where
  auth : Set (Set (Fin n))
  h_monotone : ∀ {A B}, A ∈ auth → A ⊆ B → B ∈ auth

Open namespace AccessStructure.

namespace AccessStructure

A subset of participants not in \Gamma are unauthorized.

def unauthorized {n : ℕ} (Γ : AccessStructure n)
  : Set (Set (Fin n)) :=
  {A | A ∉ Γ.auth}

While an access structure \Gamma can be large, it is uniquely determined by its minimal elements. This representation is often more compact and convenient for both theoretical analysis and implementation.

A minimal authorized set is an authorized set A, such that all proper subsets of A are not authorized.

/--
A set `A` is a minimal authorized set if it is authorized
and no proper subset of `A` is authorized.
-/
def isMinimalAuthorized {n : ℕ} (Γ : AccessStructure n)
    (A : Set (Fin n)) : Prop :=
  A ∈ Γ.auth ∧ ∀ B : Set (Fin n), B ⊂ A → B ∉ Γ.auth

We define the set of minimal authorized sets by \Gamma_0.

def minimalAuthorized {n : ℕ} (Γ : AccessStructure n)
    : Set (Set (Fin n)) :=
  {A | isMinimalAuthorized Γ A}

Specifying the minimal authorized set is sufficient to fully characterize any monotone access structure \Gamma.

The next theorem show that every authorized set contains a minimum authorized subset.

/--
Every authorized set contains a minimal authorized subset.
-/
theorem auth_contains_minimal_auth {n : ℕ}
  (Γ : AccessStructure n) :
  ∀ B ∈ Γ.auth, ∃ A ∈ Γ.auth,
  isMinimalAuthorized Γ A ∧ A ⊆ B := byn:ℕΓ:AccessStructure n⊢ ∀ B ∈ Γ.auth, ∃ A ∈ Γ.auth, Γ.isMinimalAuthorized A ∧ A ⊆ B
    intro B hBn:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.auth⊢ ∃ A ∈ Γ.auth, Γ.isMinimalAuthorized A ∧ A ⊆ B;
    -- Apply the well-ordering principle to
    -- the set of authorized subsets of `B`.
    obtain ⟨A, hA⟩ :
      ∃ A ∈ {C : Set (Fin n) | C ∈ Γ.auth ∧ C ⊆ B},
      ∀ C ∈ {C : Set (Fin n) | C ∈ Γ.auth ∧ C ⊆ B},
      A.ncard ≤ C.ncard := byn:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.auth⊢ ∃ A ∈ {C | C ∈ Γ.auth ∧ C ⊆ B}, ∀ C ∈ {C | C ∈ Γ.auth ∧ C ⊆ B}, A.ncard ≤ C.ncard
      apply_rules [ Set.exists_min_image ]h1n:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.auth⊢ {C | C ∈ Γ.auth ∧ C ⊆ B}.Finitean:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.auth⊢ {C | C ∈ Γ.auth ∧ C ⊆ B}.Nonempty;
      ·h1n:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.auth⊢ {C | C ∈ Γ.auth ∧ C ⊆ B}.Finite exact Set.toFinite _All goals completed! 🐙;
      ·an:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.auth⊢ {C | C ∈ Γ.auth ∧ C ⊆ B}.Nonempty exact ⟨ B, hB, Set.Subset.refl _ ⟩All goals completed! 🐙;
    use Ahn:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.authA:Set (Fin n)hA:A ∈ {C | C ∈ Γ.auth ∧ C ⊆ B} ∧ ∀ C ∈ {C | C ∈ Γ.auth ∧ C ⊆ B}, A.ncard ≤ C.ncard⊢ A ∈ Γ.auth ∧ Γ.isMinimalAuthorized A ∧ A ⊆ B;
    simp_all  [ isMinimalAuthorized ]hn:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.authA:Set (Fin n)hA:(A ∈ Γ.auth ∧ A ⊆ B) ∧ ∀ C ∈ Γ.auth, C ⊆ B → A.ncard ≤ C.ncard⊢ ∀ B ⊂ A, B ∉ Γ.auth;
    intro C hChn:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.authA:Set (Fin n)hA:(A ∈ Γ.auth ∧ A ⊆ B) ∧ ∀ C ∈ Γ.auth, C ⊆ B → A.ncard ≤ C.ncardC:Set (Fin n)hC:C ⊂ A⊢ C ∉ Γ.auth hC'hn:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.authA:Set (Fin n)hA:(A ∈ Γ.auth ∧ A ⊆ B) ∧ ∀ C ∈ Γ.auth, C ⊆ B → A.ncard ≤ C.ncardC:Set (Fin n)hC:C ⊂ AhC':C ∈ Γ.auth⊢ False;
    have := hA.2 C hC' ( hC.1.trans hA.1.2 )hn:ℕΓ:AccessStructure nB:Set (Fin n)hB:B ∈ Γ.authA:Set (Fin n)hA:(A ∈ Γ.auth ∧ A ⊆ B) ∧ ∀ C ∈ Γ.auth, C ⊆ B → A.ncard ≤ C.ncardC:Set (Fin n)hC:C ⊂ AhC':C ∈ Γ.auththis:A.ncard ≤ C.ncard⊢ False;
    exact this.not_gt ( Set.ncard_lt_ncard hC )All goals completed! 🐙

A set is said to be maximally unauthorized if it is unauthorized and any proper super set is authorized.

/--
A set `A` is a maximally unauthorized set if it is
unauthorized and any proper superset of `A` is authorized.
-/
def isMaximallyUnauthorized {n : ℕ} (Γ : AccessStructure n)
    (A : Set (Fin n)) : Prop :=
  A ∉ Γ.auth ∧ ∀ B : Set (Fin n), A ⊂ B → B ∈ Γ.auth

Define the collection of maximally unauthorized sets.

/--
The family of maximally unauthorized sets.
-/
def maximallyUnauthorized {n : ℕ} (Γ : AccessStructure n)
    : Set (Set (Fin n)) :=
  {A | isMaximallyUnauthorized Γ A}

We can generate an access structure by taking the upper closure of an arbitrary collection S.

def generatedAccessStructure {n : ℕ} (S : Set (Set (Fin n)))
   : Set (Set (Fin n)) :=
  upperClosure S

A set A is in the upper closure of a collection S if and only if there exists a set B in S such that B is a subset of A.

/--
An explicit statement of what `upper close` means.
-/
theorem mem_generatedAccessStructure_iff {n : ℕ}
  (S : Set (Set (Fin n))) (A : Set (Fin n)) :
    A ∈ generatedAccessStructure S ↔ ∃ B ∈ S, B ⊆ A := byn:ℕS:Set (Set (Fin n))A:Set (Fin n)⊢ A ∈ generatedAccessStructure S ↔ ∃ B ∈ S, B ⊆ A
  simp [generatedAccessStructure, mem_upperClosure]All goals completed! 🐙

The access structure generated by S is the smallest monotone collection that contains S as a sub-colleciton.

theorem generatedAccessStructure_extensive {n : ℕ}
  (S : Set (Set (Fin n))) :
    S ⊆ generatedAccessStructure S := byn:ℕS:Set (Set (Fin n))⊢ S ⊆ generatedAccessStructure S
  exact fun x hx => ⟨ x, hx, le_rfl ⟩All goals completed! 🐙

If S is a subcollection of T, then the access structure generated by T contains the access structure generated by S.

/--
If S ⊆ T, then the access structure generated
by `T` contains the subsets in the access structure
generated by `S`.
-/
theorem generatedAccessStructure_mono {n : ℕ}
  {S T : Set (Set (Fin n))} (h : S ⊆ T) :
    generatedAccessStructure S
    ⊆ generatedAccessStructure T := byn:ℕS:Set (Set (Fin n))T:Set (Set (Fin n))h:S ⊆ T⊢ generatedAccessStructure S ⊆ generatedAccessStructure T
  intros A hAn:ℕS:Set (Set (Fin n))T:Set (Set (Fin n))h:S ⊆ TA:Set (Fin n)hA:A ∈ generatedAccessStructure S⊢ A ∈ generatedAccessStructure T
  obtain ⟨B, hB₁, hB₂⟩ := mem_upperClosure.mp hAn:ℕS:Set (Set (Fin n))T:Set (Set (Fin n))h:S ⊆ TA:Set (Fin n)hA:A ∈ generatedAccessStructure SB:Set (Fin n)hB₁:B ∈ ShB₂:B ≤ A⊢ A ∈ generatedAccessStructure T
  have hB₃ : B ∈ T := h hB₁n:ℕS:Set (Set (Fin n))T:Set (Set (Fin n))h:S ⊆ TA:Set (Fin n)hA:A ∈ generatedAccessStructure SB:Set (Fin n)hB₁:B ∈ ShB₂:B ≤ AhB₃:B ∈ T⊢ A ∈ generatedAccessStructure T
  exact mem_upperClosure.mpr ⟨B, hB₃, hB₂⟩All goals completed! 🐙

If S an access structure generated by some other collection, then the access structure generated by S is the same as S.

/--
The generated access structure operation is idempotent.
-/
theorem generatedAccessStructure_idempotent {n : ℕ}
  (S : Set (Set (Fin n))) :
    generatedAccessStructure (generatedAccessStructure S)
      = generatedAccessStructure S := byn:ℕS:Set (Set (Fin n))⊢ generatedAccessStructure (generatedAccessStructure S) = generatedAccessStructure S
  simp_all [generatedAccessStructure ]All goals completed! 🐙

In terms of lattice theory, the operation of generating an access structure from an arbitrary collection of sets is an example of closure operator. In general, a mapping C from a lattice to itself is called a closure operator if

S \prec C(S) for all S.
S \prec T implies C(S) \prec C(T).
C (C (S)) = C (S).

/--
The generated access structure operation is a
closure operator.
-/
def generatedAccessStructureClosure (n : ℕ)
  : ClosureOperator (Set (Set (Fin n))) where
  toFun := generatedAccessStructure
  monotone' := fun _ _ h => generatedAccessStructure_mono h
  le_closure' := generatedAccessStructure_extensive
  idempotent' := generatedAccessStructure_idempotent

The threshold access structure is a basic example of access structure. All sets with cardinality larger than or equal to a threshold t are authorized, but sets with cardinality less than t are not authorized.

This access structure is generated by sets of size t. We define this access structure as thresholdAccessStructure n t.

def thresholdAccessStructure (n t : ℕ)
  : AccessStructure n where
  auth := generatedAccessStructure {A | A.ncard = t}
  h_monotone := byn:ℕt:ℕ⊢ ∀ {A B : Set (Fin n)},
  A ∈ generatedAccessStructure {A | A.ncard = t} → A ⊆ B → B ∈ generatedAccessStructure {A | A.ncard = t}
    unfold generatedAccessStructuren:ℕt:ℕ⊢ ∀ {A B : Set (Fin n)}, A ∈ ↑(upperClosure {A | A.ncard = t}) → A ⊆ B → B ∈ ↑(upperClosure {A | A.ncard = t});
    simp [ upperClosure ]n:ℕt:ℕ⊢ ∀ {A B : Set (Fin n)} (x : Set (Fin n)), x.ncard = t → x ⊆ A → A ⊆ B → ∃ a, a.ncard = t ∧ a ⊆ B;
    exact fun { A B } x hx hx' hx''
      => ⟨ x, hx, hx'.trans hx'' ⟩All goals completed! 🐙

We verify that a set in thresholdAccessStructure n t is authorized if and only if the cardinality is larger than or equal to t.

theorem threshold_auth_iff (n t : ℕ) (A : Set (Fin n)) :
  A ∈ (thresholdAccessStructure n t).auth
  ↔ t ≤ A.ncard := byn:ℕt:ℕA:Set (Fin n)⊢ A ∈ (thresholdAccessStructure n t).auth ↔ t ≤ A.ncard
    constructormpn:ℕt:ℕA:Set (Fin n)⊢ A ∈ (thresholdAccessStructure n t).auth → t ≤ A.ncardmprn:ℕt:ℕA:Set (Fin n)⊢ t ≤ A.ncard → A ∈ (thresholdAccessStructure n t).auth;
    ·mpn:ℕt:ℕA:Set (Fin n)⊢ A ∈ (thresholdAccessStructure n t).auth → t ≤ A.ncard intro hAmpn:ℕt:ℕA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).auth⊢ t ≤ A.ncard;
      -- Since `A` is in the upper closure of the
      -- set of subsets with cardinality `t`, there exists
      -- some `B` with `|B| = t` such that `B \subseteq A`.
      obtain ⟨B, hB_card, hB_subset⟩ :
        ∃ B : Set (Fin n), B.ncard = t ∧ B ⊆ A := byn:ℕt:ℕA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).auth⊢ ∃ B, B.ncard = t ∧ B ⊆ A
        exact hAAll goals completed! 🐙;
      exact hB_card ▸ Set.ncard_le_ncard hB_subsetAll goals completed! 🐙;
    ·mprn:ℕt:ℕA:Set (Fin n)⊢ t ≤ A.ncard → A ∈ (thresholdAccessStructure n t).auth intro htmprn:ℕt:ℕA:Set (Fin n)ht:t ≤ A.ncard⊢ A ∈ (thresholdAccessStructure n t).auth
      obtain ⟨B, hB⟩
       : ∃ B : Set (Fin n), B ⊆ A ∧ B.ncard = t := byn:ℕt:ℕA:Set (Fin n)ht:t ≤ A.ncard⊢ ∃ B ⊆ A, B.ncard = t
        exact Set.exists_subset_card_eq htAll goals completed! 🐙;
      exact ⟨ B, hB.2, hB.1 ⟩All goals completed! 🐙

All subsets of size t-1 are maximally unauthorized sets.

theorem threshold_maximalUnauthorized_eq (n t : ℕ)
  (h_t : t > 0) (h_t_le_n : t ≤ n) :
  (thresholdAccessStructure n t).maximallyUnauthorized
  = {A | A.ncard = t - 1} := byn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ n⊢ (thresholdAccessStructure n t).maximallyUnauthorized = {A | A.ncard = t - 1}
    ext Ahn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)⊢ A ∈ (thresholdAccessStructure n t).maximallyUnauthorized ↔ A ∈ {A | A.ncard = t - 1};
    constructorh.mpn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)⊢ A ∈ (thresholdAccessStructure n t).maximallyUnauthorized → A ∈ {A | A.ncard = t - 1}h.mprn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)⊢ A ∈ {A | A.ncard = t - 1} → A ∈ (thresholdAccessStructure n t).maximallyUnauthorized <;>h.mpn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)⊢ A ∈ (thresholdAccessStructure n t).maximallyUnauthorized → A ∈ {A | A.ncard = t - 1}h.mprn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)⊢ A ∈ {A | A.ncard = t - 1} → A ∈ (thresholdAccessStructure n t).maximallyUnauthorized intro hAh.mprn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}⊢ A ∈ (thresholdAccessStructure n t).maximallyUnauthorized;
    ·h.mpn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorized⊢ A ∈ {A | A.ncard = t - 1} have h_card : A.ncard < t := byn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ n⊢ (thresholdAccessStructure n t).maximallyUnauthorized = {A | A.ncard = t - 1}
        exact lt_of_not_ge fun h => hA.1
        <| byn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh:t ≤ A.ncard⊢ A ∈ (thresholdAccessStructure n t).auth exact ( threshold_auth_iff n t A ) |>.2 hAll goals completed! 🐙;
      have h_card :
        ∀ B : Set (Fin n), A ⊂ B → t ≤ B.ncard := byn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ n⊢ (thresholdAccessStructure n t).maximallyUnauthorized = {A | A.ncard = t - 1}
        exact fun B hB => byn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card:A.ncard < tB:Set (Fin n)hB:A ⊂ B⊢ t ≤ B.ncard
          have := hA.2 B hBn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card:A.ncard < tB:Set (Fin n)hB:A ⊂ Bthis:B ∈ (thresholdAccessStructure n t).auth⊢ t ≤ B.ncard;
          exact (threshold_auth_iff n t B).mp thisAll goals completed! 🐙;
      contrapose! h_cardh.mpn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}⊢ ∃ B, A ⊂ B ∧ B.ncard < t;
      -- Since $A$ is not maximal unauthorized,
      -- there exists an element
      -- `x \in \{0, 1, ..., n-1\} \setminus A`.
      obtain ⟨x, hx⟩ : ∃ x : Fin n, x ∉ A := byn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}⊢ ∃ x, x ∉ A
        by_cases hA_univ : A = Set.univposn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}hA_univ:A = Set.univ⊢ ∃ x, x ∉ Anegn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}hA_univ:¬A = Set.univ⊢ ∃ x, x ∉ A;
        ·posn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}hA_univ:A = Set.univ⊢ ∃ x, x ∉ A simp_all  [ Set.ncard_univ ]posn:ℕt:ℕA:Set (Fin n)h_t:0 < th_t_le_n:t ≤ nhA:Set.univ ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:n < th_card:¬n = t - 1hA_univ:A = Set.univ⊢ False;
          linarithAll goals completed! 🐙;
        ·negn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}hA_univ:¬A = Set.univ⊢ ∃ x, x ∉ A exact Set.nonempty_compl.2 hA_univAll goals completed! 🐙;
      refine' ⟨ Insert.insert x A, _, _ ⟩h.mp.refine'_1n:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}x:Fin nhx:x ∉ A⊢ A ⊂ insert x Ah.mp.refine'_2n:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}x:Fin nhx:x ∉ A⊢ (insert x A).ncard < t <;>h.mp.refine'_1n:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}x:Fin nhx:x ∉ A⊢ A ⊂ insert x Ah.mp.refine'_2n:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A ∈ {A | A.ncard = t - 1}x:Fin nhx:x ∉ A⊢ (insert x A).ncard < t simp_allh.mp.refine'_2n:ℕt:ℕA:Set (Fin n)x:Fin nh_t:0 < th_t_le_n:t ≤ nhA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A.ncard = t - 1hx:x ∉ A⊢ (insert x A).ncard < t ;
      ·h.mp.refine'_1n:ℕt:ℕA:Set (Fin n)x:Fin nh_t:0 < th_t_le_n:t ≤ nhA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A.ncard = t - 1hx:x ∉ A⊢ A ⊂ insert x A exact ⟨ Set.subset_insert _ _, fun h
          => hx <| h <| Set.mem_insert _ _ ⟩All goals completed! 🐙;
      ·h.mp.refine'_2n:ℕt:ℕA:Set (Fin n)x:Fin nh_t:0 < th_t_le_n:t ≤ nhA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A.ncard = t - 1hx:x ∉ A⊢ (insert x A).ncard < t rw [ Set.ncard_insert_of_notMem hx ]h.mp.refine'_2n:ℕt:ℕA:Set (Fin n)x:Fin nh_t:0 < th_t_le_n:t ≤ nhA:A ∈ (thresholdAccessStructure n t).maximallyUnauthorizedh_card✝:A.ncard < th_card:¬A.ncard = t - 1hx:x ∉ A⊢ A.ncard + 1 < t ;
        omegaAll goals completed! 🐙;
    ·h.mprn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}⊢ A ∈ (thresholdAccessStructure n t).maximallyUnauthorized constructorh.mpr.leftn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}⊢ A ∉ (thresholdAccessStructure n t).authh.mpr.rightn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}⊢ ∀ (B : Set (Fin n)), A ⊂ B → B ∈ (thresholdAccessStructure n t).auth;
      ·h.mpr.leftn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}⊢ A ∉ (thresholdAccessStructure n t).auth exact fun h => byn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}h:A ∈ (thresholdAccessStructure n t).auth⊢ False
          have := threshold_auth_iff n t A |>.1 hn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}h:A ∈ (thresholdAccessStructure n t).auththis:t ≤ A.ncard⊢ False;
              linarith [ hA.symm, Nat.sub_add_cancel h_t ]All goals completed! 🐙 ;
      ·h.mpr.rightn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}⊢ ∀ (B : Set (Fin n)), A ⊂ B → B ∈ (thresholdAccessStructure n t).auth intro B hBh.mpr.rightn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}B:Set (Fin n)hB:A ⊂ B⊢ B ∈ (thresholdAccessStructure n t).auth
        have hB_card : B.ncard ≥ t := byn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ n⊢ (thresholdAccessStructure n t).maximallyUnauthorized = {A | A.ncard = t - 1}
          have := Set.ncard_lt_ncard hBn:ℕt:ℕh_t:t > 0h_t_le_n:t ≤ nA:Set (Fin n)hA:A ∈ {A | A.ncard = t - 1}B:Set (Fin n)hB:A ⊂ Bthis:A.ncard < B.ncard⊢ B.ncard ≥ t;
          grindAll goals completed! 🐙;
        exact threshold_auth_iff n t B |>.2 hB_cardAll goals completed! 🐙

The minimal authorized sets of the threshold access structure are precisely the sets of size t.

theorem threshold_minimalAuthorized_eq (n t : ℕ) :
  (thresholdAccessStructure n t).minimalAuthorized
   = {A | A.ncard = t} := byn:ℕt:ℕ⊢ (thresholdAccessStructure n t).minimalAuthorized = {A | A.ncard = t}
    -- To prove equality of sets,
    -- we show each set is a subset of the other.
    apply Set.exthn:ℕt:ℕ⊢ ∀ (x : Set (Fin n)), x ∈ (thresholdAccessStructure n t).minimalAuthorized ↔ x ∈ {A | A.ncard = t}
    intro Ahn:ℕt:ℕA:Set (Fin n)⊢ A ∈ (thresholdAccessStructure n t).minimalAuthorized ↔ A ∈ {A | A.ncard = t}
    simp [minimalAuthorized, thresholdAccessStructure]hn:ℕt:ℕA:Set (Fin n)⊢ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.isMinimalAuthorized A ↔ A.ncard = t;
    constructorh.mpn:ℕt:ℕA:Set (Fin n)⊢ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.isMinimalAuthorized A → A.ncard = th.mprn:ℕt:ℕA:Set (Fin n)⊢ A.ncard = t → { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.isMinimalAuthorized A;
    ·h.mpn:ℕt:ℕA:Set (Fin n)⊢ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.isMinimalAuthorized A → A.ncard = t rintro ⟨ hA₁, hA₂ ⟩h.mpn:ℕt:ℕA:Set (Fin n)hA₁:A ∈ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.authhA₂:∀ B ⊂ A, B ∉ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.auth⊢ A.ncard = t;
      obtain ⟨ B, hB₁, hB₂ ⟩ := hA₁h.mpn:ℕt:ℕA:Set (Fin n)hA₂:∀ B ⊂ A, B ∉ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.authB:Set (Fin n)hB₁:B ∈ {A | A.ncard = t}hB₂:B ≤ A⊢ A.ncard = t;
      contrapose! hA₂h.mpn:ℕt:ℕA:Set (Fin n)B:Set (Fin n)hB₁:B ∈ {A | A.ncard = t}hB₂:B ≤ AhA₂:A.ncard ≠ t⊢ ∃ B ⊂ A, B ∈ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.auth;
      refine' ⟨ B, _, _ ⟩h.mp.refine'_1n:ℕt:ℕA:Set (Fin n)B:Set (Fin n)hB₁:B ∈ {A | A.ncard = t}hB₂:B ≤ AhA₂:A.ncard ≠ t⊢ B ⊂ Ah.mp.refine'_2n:ℕt:ℕA:Set (Fin n)B:Set (Fin n)hB₁:B ∈ {A | A.ncard = t}hB₂:B ≤ AhA₂:A.ncard ≠ t⊢ B ∈ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.auth;
      ·h.mp.refine'_1n:ℕt:ℕA:Set (Fin n)B:Set (Fin n)hB₁:B ∈ {A | A.ncard = t}hB₂:B ≤ AhA₂:A.ncard ≠ t⊢ B ⊂ A exact lt_of_le_of_ne hB₂ fun h => hA₂ <| h ▸ hB₁All goals completed! 🐙;
      ·h.mp.refine'_2n:ℕt:ℕA:Set (Fin n)B:Set (Fin n)hB₁:B ∈ {A | A.ncard = t}hB₂:B ≤ AhA₂:A.ncard ≠ t⊢ B ∈ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.auth exact ⟨ B, hB₁, Set.Subset.refl _ ⟩All goals completed! 🐙;
    ·h.mprn:ℕt:ℕA:Set (Fin n)⊢ A.ncard = t → { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.isMinimalAuthorized A intro hAh.mprn:ℕt:ℕA:Set (Fin n)hA:A.ncard = t⊢ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.isMinimalAuthorized A
      constructorh.mpr.leftn:ℕt:ℕA:Set (Fin n)hA:A.ncard = t⊢ A ∈ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.authh.mpr.rightn:ℕt:ℕA:Set (Fin n)hA:A.ncard = t⊢ ∀ B ⊂ A, B ∉ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.auth
      ·h.mpr.leftn:ℕt:ℕA:Set (Fin n)hA:A.ncard = t⊢ A ∈ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.auth exact (byn:ℕt:ℕA:Set (Fin n)hA:A.ncard = t⊢ A ∈ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.auth
        exact ⟨ A, hA, Set.Subset.refl _ ⟩All goals completed! 🐙)
      ·h.mpr.rightn:ℕt:ℕA:Set (Fin n)hA:A.ncard = t⊢ ∀ B ⊂ A, B ∉ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.auth -- If `B` is a proper subset of `A`,
        -- then its cardinality is strictly less than `t`.
        intro B hBh.mpr.rightn:ℕt:ℕA:Set (Fin n)hA:A.ncard = tB:Set (Fin n)hB:B ⊂ A⊢ B ∉ { auth := generatedAccessStructure {A | A.ncard = t}, h_monotone := ⋯ }.auth
        have hB_card : B.ncard < t := byn:ℕt:ℕ⊢ (thresholdAccessStructure n t).minimalAuthorized = {A | A.ncard = t}
          exact hA ▸ Set.ncard_lt_ncard hBAll goals completed! 🐙;
        simp [generatedAccessStructure]h.mpr.rightn:ℕt:ℕA:Set (Fin n)hA:A.ncard = tB:Set (Fin n)hB:B ⊂ AhB_card:B.ncard < t⊢ ∀ (x : Set (Fin n)), x.ncard = t → ¬x ⊆ B;
        exact fun x hx hx' => hB_card.not_ge
        <| hx ▸ Set.ncard_le_ncard hx'All goals completed! 🐙

end AccessStructure  -- namespace

end AccessStructure  -- section