The HF fragment (issue #18)

L_HF = L_ωω: the first-order image inside Lω₁ω, as an honest admissible fragment, plus its compactness theorem derived from Mathlib.

This is the regression oracle for the interface. Any proposed change to AdmissibleFragment must keep all four conditions:

1. the underlying formulas are exactly the toLω-image (sentence_slice_hfFragment);
2. coded families reduce to finite ones — here, to none at all;
3. the compactness theorem is finitaryFragment_compact;
4. no adapter widens it back to all of Lω₁ω.

Where the emptiness lives. hfFamily.IsFamilyCode is False. Not the index type's cardinality, and not einf's ⊤-padding, which is legitimate for a real infinitary code. The forbidden move is granting the certificate to a finite code and using padding to manufacture a primitive iInf.

Universes. The syntax layer and finitaryFragment_compactIn are universe-general; the latter returns Mathlib's canonical model in Type (max u v). The compatibility theorem finitaryFragment_compact retains its published universe-zero result type.

Not built on the legacy structures. AdmissibleFragmentCore.hf := Set.univ is a quarantined placeholder; nothing here uses it, and nothing here may be proved from it.

def FirstOrder.Language.hfFragment (L : Language) : L.Fragment

The HF fragment. Each field is now one appeal to the first-order-image API: three structural equations and the two negative facts. Compare the five hand-rolled constructor inversions this replaces.

Equations

• L.hfFragment = { toSet := FirstOrder.Language.hfSet✝ L, imp_left_mem := ⋯, imp_right_mem := ⋯, all_mem := ⋯, iInf_mem := ⋯, iSup_mem := ⋯ }

def FirstOrder.Language.finitaryFragment (L : Language) : Set L.Sentenceω

The finitary fragment: the image of first-order syntax in Lω₁ω. This is L_HF = L_ωω.

Equations

• L.finitaryFragment = Set.range FirstOrder.Language.Sentence.toLω

theorem FirstOrder.Language.finitaryFragment_compact {L : Language} {T : L.Theoryω} (hT : T ⊆ L.finitaryFragment) (hfin : T.IsFinitelySatisfiable) : T.IsSatisfiable

Universe-zero compatibility endpoint. This retains the published result type while the underlying first-order argument is universe-general; use finitaryFragment_compactIn when the language or resulting carrier lives above universe zero.

Gate 4 — the HF oracle

For HF the certificate is empty, so CodedFamily is uninhabited and the upward-closure fields of any AdmissibleFragment over it are vacuous. Note where the emptiness lives: in IsFamilyCode, not in the index type's cardinality and not in einf's padding.

Step 4 — the honest HF instance

Essentially a structure literal: the base is hfFragment, and both upward fields are closed by certificate absurdity. That it is nearly definitional is the signal that the signature is right.

def FirstOrder.Language.hfAdmissibleFragment (L : Language) : AdmissibleFragment L.hfFamily

The HF admissible fragment. No adapter, no widening.

Equations

• L.hfAdmissibleFragment = { toFragment := L.hfFragment, iInf_coded_mem := ⋯, iSup_coded_mem := ⋯ }

The universe boundary

The structures are language-indexed and universe-polymorphic: FamilyPresentation L for L : Language.{u, v}, so FamilyPresentation L[[J]] is well-formed for an arbitrary parameter type J. The probes below record that, at the signature level only — nothing here claims a presentation for L lifts to one for L[[J]].

The low-level semantic boundary is now explicit: Theoryω.IsSatisfiableIn selects the carrier universe, and finitaryFragment_compactIn works for any language. The ambient presentation API still concludes the published universe-zero Theoryω.IsSatisfiable; that remaining boundary is enforced separately by scripts/check_admissible_universes.lean.

Write the probe results as Type _, not Type: bare Type means Type 0, and that constraint propagates backward onto the presentation argument.