NF weak partition development: NFStandard.StratificationNormalize.

The Hailperin construction first raises every variable to a common type. For a nonempty finite context, typeCeiling ty is the largest assigned integer type and typeOffset ty i is the number of singleton applications needed to raise variable i to that ceiling.

def NFChoice.Foundation.Formula.typeCeiling {n : ℕ} (ty : Fin (n + 1) → ℤ) : ℤ

The largest type in a nonempty intrinsic context.

Equations

• NFChoice.Foundation.Formula.typeCeiling ty = Finset.univ.sup' ⋯ ty

theorem NFChoice.Foundation.Formula.le_typeCeiling {n : ℕ} (ty : Fin (n + 1) → ℤ) (i : Fin (n + 1)) : ty i ≤ typeCeiling ty

Every assigned type lies below the chosen ceiling.

def NFChoice.Foundation.Formula.typeOffset {n : ℕ} (ty : Fin (n + 1) → ℤ) (i : Fin (n + 1)) : ℕ

Number of singleton raises taking variable i to the common ceiling.

Equations

• NFChoice.Foundation.Formula.typeOffset ty i = (NFChoice.Foundation.Formula.typeCeiling ty - ty i).toNat

theorem NFChoice.Foundation.Formula.typeOffset_cast {n : ℕ} (ty : Fin (n + 1) → ℤ) (i : Fin (n + 1)) : ↑(typeOffset ty i) = typeCeiling ty - ty i

theorem NFChoice.Foundation.Formula.typeOffset_eq_of_eq {n : ℕ} {ty : Fin (n + 1) → ℤ} {i j : Fin (n + 1)} (h : ty i = ty j) : typeOffset ty i = typeOffset ty j

Equal-typed variables need the same number of singleton raises.

theorem NFChoice.Foundation.Formula.typeOffset_mem {n : ℕ} {ty : Fin (n + 1) → ℤ} {i j : Fin (n + 1)} (h : ty j = ty i + 1) : typeOffset ty i = typeOffset ty j + 1

A membership source needs exactly one more raise than its target.