The honest admissible fragment (issue #18)

A purely syntactic wrapper: an ordinary Fragment, closed upward under exactly the conjunctions and disjunctions named by certified coded families.

Deliberately absent:

• no height — whether it belongs to the presentation or is derived is unsettled, and a field here would permit a fragment whose height disagreed with its presentation's;
• no compactness data — compactness is a theorem with hypotheses, proved externally. That is what makes "a theorem named Barwise compactness merely projects a field" structurally impossible rather than merely observed.

This does not wrap the legacy AdmissibleFragmentCore, which an honest HF fragment provably cannot instantiate: its closed_iInf/closed_iSup are upward over arbitrary external ℕ-families.

structure FirstOrder.Language.AdmissibleFragment {L : Language} (P : L.FamilyPresentation) extends L.Fragment : Type (max u v)

An admissible fragment: an ordinary Fragment, closed upward under the conjunctions and disjunctions named by certified coded families — and under nothing else.

Parameterized by the family view. This file imports only Admissible/Family.lean, so the syntax interface cannot mention theory decoding or Sigma1: the separation is by import, not by convention. A richer presentation is used here through its toFamilyPresentation projection.

• toSet : Set ((n : ℕ) × L.BoundedFormulaω Empty n)
• imp_left_mem {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : ⟨n, φ.imp ψ⟩ ∈ self.toSet → ⟨n, φ⟩ ∈ self.toSet
• imp_right_mem {n : ℕ} {φ ψ : L.BoundedFormulaω Empty n} : ⟨n, φ.imp ψ⟩ ∈ self.toSet → ⟨n, ψ⟩ ∈ self.toSet
• all_mem {n : ℕ} {φ : L.BoundedFormulaω Empty (n + 1)} : ⟨n, φ.all⟩ ∈ self.toSet → ⟨n + 1, φ⟩ ∈ self.toSet
• iInf_mem {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} : ⟨n, BoundedFormulaω.iInf φs⟩ ∈ self.toSet → ∀ (k : ℕ), ⟨n, φs k⟩ ∈ self.toSet
• iSup_mem {n : ℕ} {φs : ℕ → L.BoundedFormulaω Empty n} : ⟨n, BoundedFormulaω.iSup φs⟩ ∈ self.toSet → ∀ (k : ℕ), ⟨n, φs k⟩ ∈ self.toSet
• iInf_coded_mem {n : ℕ} (F : CodedFamily P n) : (∀ (i : P.Index F.code), ⟨n, F.decode i⟩ ∈ self.toSet) → ⟨n, codedIInf F⟩ ∈ self.toSet
• iSup_coded_mem {n : ℕ} (F : CodedFamily P n) : (∀ (i : P.Index F.code), ⟨n, F.decode i⟩ ∈ self.toSet) → ⟨n, codedISup F⟩ ∈ self.toSet