NF weak partition development: SemanticCore.PartialLowering.

def NFChoice.SemanticCore.PartialLowering.liftRhoOption {n : ℕ} (rho : Var → Option (Fin n)) : Var → Option (Fin (n + 1))

Shift every mapped variable under a new de Bruijn binder.

Equations

• NFChoice.SemanticCore.PartialLowering.liftRhoOption rho x = Option.map Fin.succ (rho x)

def NFChoice.SemanticCore.PartialLowering.bindRhoOption {n : ℕ} (rho : Var → Option (Fin n)) (x : Var) : Var → Option (Fin (n + 1))

Shift the old mappings and bind x at de Bruijn index zero.

Equations

• NFChoice.SemanticCore.PartialLowering.bindRhoOption rho x = Function.update (NFChoice.SemanticCore.PartialLowering.liftRhoOption rho) x (some 0)

def NFChoice.SemanticCore.PartialLowering.lowerClassPredOption {n : ℕ} (rho : Var → Option (Fin n)) (candidate : Fin n) : Class → Option (Foundation.Formula n)

Partial class-predicate lowering; failure means an unmapped free name.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.SemanticCore.PartialLowering.lowerClassPredOption rho candidate (NFChoice.SemanticCore.Class.cv x_1) = do let i ← rho x_1 pure (NFChoice.Foundation.Formula.mem candidate i)

def NFChoice.SemanticCore.PartialLowering.lowerWffOption {n : ℕ} (rho : Var → Option (Fin n)) : Wff → Option (Foundation.Formula n)

Partial nominal lowering, usable at depth zero with the empty environment.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.SemanticCore.PartialLowering.lowerWffOption rho NFChoice.SemanticCore.Wff.falsum = some NFChoice.Foundation.Formula.falsum
• NFChoice.SemanticCore.PartialLowering.lowerWffOption rho (NFChoice.SemanticCore.Wff.objEq x_1 y) = do let x' ← rho x_1 let y' ← rho y pure (NFChoice.Foundation.Formula.equal x' y')
• NFChoice.SemanticCore.PartialLowering.lowerWffOption rho (NFChoice.SemanticCore.Wff.objMem x_1 y) = do let x' ← rho x_1 let y' ← rho y pure (NFChoice.Foundation.Formula.mem x' y')

def NFChoice.SemanticCore.PartialLowering.MappedAgreement {S : Type u_1} {n : ℕ} (rho : Var → Option (Fin n)) (xs : DVec S n) (v : Var → S) (support : Finset Var) : Prop

The partial environment supplies the values of all names in support.

Equations

• NFChoice.SemanticCore.PartialLowering.MappedAgreement rho xs v support = ∀ x ∈ support, ∃ (i : Fin n), rho x = some i ∧ NFChoice.SemanticCore.Lowering.lookup xs i = v x

def NFChoice.SemanticCore.PartialLowering.emptyRho : Var → Option (Fin 0)

An empty partial environment, available even at de Bruijn depth zero.

Equations

• NFChoice.SemanticCore.PartialLowering.emptyRho x✝ = none

def NFChoice.SemanticCore.PartialLowering.lowerClosed (p : Wff) : Option Foundation.Sentence

Lower a closed nominal wff directly to a sentence.

Equations

• NFChoice.SemanticCore.PartialLowering.lowerClosed p = NFChoice.SemanticCore.PartialLowering.lowerWffOption NFChoice.SemanticCore.PartialLowering.emptyRho p

def NFChoice.SemanticCore.PartialLowering.closeNames : List Var → Wff → Wff

Universally close the listed nominal names, in list order.

Equations

• NFChoice.SemanticCore.PartialLowering.closeNames [] x✝ = x✝
• NFChoice.SemanticCore.PartialLowering.closeNames (x_2 :: xs) x✝ = NFChoice.SemanticCore.Wff.all x_2 (NFChoice.SemanticCore.PartialLowering.closeNames xs x✝)

def NFChoice.SemanticCore.PartialLowering.assignNames {S : Type u_1} : List Var → (Var → S) → (Var → S) → Var → S

Assign every listed name its value in a target valuation.

Equations

• NFChoice.SemanticCore.PartialLowering.assignNames [] x✝¹ x✝ = x✝¹
• NFChoice.SemanticCore.PartialLowering.assignNames (x_3 :: xs) x✝¹ x✝ = NFChoice.SemanticCore.PartialLowering.assignNames xs (NFChoice.SemanticCore.update x✝¹ x_3 (x✝ x_3)) x✝

theorem NFChoice.SemanticCore.PartialLowering.assignNames_eq_of_not_mem {S : Type u_1} (names : List Var) (base target : Var → S) {x : Var} (hx : x ∉ names) : assignNames names base target x = base x

theorem NFChoice.SemanticCore.PartialLowering.assignNames_eq_of_mem {S : Type u_1} (names : List Var) (base target : Var → S) {x : Var} (hx : x ∈ names) : assignNames names base target x = target x

theorem NFChoice.SemanticCore.PartialLowering.holds_closeNames_assign {S : Fol.Structure Foundation.LNF} (names : List Var) (p : Wff) (base target : Var → S.carrier) (h : Wff.Holds S base (closeNames names p)) : Wff.Holds S (assignNames names base target) p

Specialize a nominal universal closure at a target valuation.

theorem NFChoice.SemanticCore.PartialLowering.valid_of_holds_closeNames {S : Fol.Structure Foundation.LNF} (names : List Var) (p : Wff) (base : Var → S.carrier) (hcover : p.fv ⊆ names.toFinset) (h : Wff.Holds S base (closeNames names p)) : Wff.Valid S p

Truth of a universal nominal closure yields global validity of its open body, provided the list covers all free names.

theorem NFChoice.SemanticCore.PartialLowering.valid_of_valid_closeNames {S : Fol.Structure Foundation.LNF} (names : List Var) (p : Wff) (hcover : p.fv ⊆ names.toFinset) (h : Wff.Valid S (closeNames names p)) : Wff.Valid S p

A valid universal nominal closure yields validity of its open body.

theorem NFChoice.SemanticCore.PartialLowering.fv_closeNames (names : List Var) (p : Wff) : (closeNames names p).fv = p.fv \ names.toFinset

theorem NFChoice.SemanticCore.PartialLowering.MappedAgreement.mono {S : Type u_1} {n : ℕ} {rho : Var → Option (Fin n)} {xs : DVec S n} {v : Var → S} {s t : Finset Var} (h : MappedAgreement rho xs v t) (hst : s ⊆ t) : MappedAgreement rho xs v s

theorem NFChoice.SemanticCore.PartialLowering.mappedAgreement_update {S : Type u_1} {n : ℕ} (rho : Var → Option (Fin n)) (xs : DVec S n) (v : Var → S) (x : Var) (candidate : Fin n) (p : Wff) (h : MappedAgreement rho xs v (p.fv.erase x)) : MappedAgreement (Function.update rho x (some candidate)) xs (update v x (Lowering.lookup xs candidate)) p.fv

theorem NFChoice.SemanticCore.PartialLowering.mappedAgreement_bind {S : Type u_1} {n : ℕ} (rho : Var → Option (Fin n)) (xs : DVec S n) (v : Var → S) (x : Var) (a : S) (p : Wff) (h : MappedAgreement rho xs v (p.fv.erase x)) : MappedAgreement (bindRhoOption rho x) (DVec.cons a xs) (update v x a) p.fv

theorem NFChoice.SemanticCore.PartialLowering.mappedAgreement_lift {S : Type u_1} {n : ℕ} (rho : Var → Option (Fin n)) (xs : DVec S n) (v : Var → S) (s : Finset Var) (a : S) (h : MappedAgreement rho xs v s) : MappedAgreement (liftRhoOption rho) (DVec.cons a xs) v s

theorem NFChoice.SemanticCore.PartialLowering.lowerClassPredOption_sound {S : Fol.Structure Foundation.LNF} {n : ℕ} (rho : Var → Option (Fin n)) (xs : DVec S.carrier n) (v : Var → S.carrier) (candidate : Fin n) (A : Class) (f : Foundation.Formula n) (hlower : lowerClassPredOption rho candidate A = some f) (hmap : MappedAgreement rho xs v A.fv) : Class.Holds S v A (Lowering.lookup xs candidate) ↔ Lowering.FormulaHolds S xs f

Soundness of successful partial class-predicate lowering.

theorem NFChoice.SemanticCore.PartialLowering.lowerWffOption_sound {S : Fol.Structure Foundation.LNF} {n : ℕ} (rho : Var → Option (Fin n)) (xs : DVec S.carrier n) (v : Var → S.carrier) (p : Wff) (f : Foundation.Formula n) (hlower : lowerWffOption rho p = some f) (hmap : MappedAgreement rho xs v p.fv) : Wff.Holds S v p ↔ Lowering.FormulaHolds S xs f

Soundness of every successful partial nominal-wff lowering.

theorem NFChoice.SemanticCore.PartialLowering.lowerClosed_sound {S : Fol.Structure Foundation.LNF} (p : Wff) (f : Foundation.Sentence) (hpClosed : p.fv = ∅) (hlower : lowerClosed p = some f) (v : Var → S.carrier) : Wff.Holds S v p ↔ Lowering.FormulaHolds S DVec.nil f

A successful closed lowering has exactly the nominal closed semantics.

theorem NFChoice.SemanticCore.PartialLowering.lowerClosed_realize_iff {S : Fol.Structure Foundation.LNF} (p : Wff) (f : Foundation.Sentence) (hpClosed : p.fv = ∅) (hlower : lowerClosed p = some f) (v : Var → S.carrier) : Wff.Holds S v p ↔ Fol.realizeSentence S (Foundation.Formula.toFlypitch f)

Closed nominal lowering reaches the exact Flypitch sentence semantics.

theorem NFChoice.SemanticCore.PartialLowering.valid_of_lowerClosed_realize {S : Fol.Structure Foundation.LNF} (p : Wff) (f : Foundation.Sentence) (hpClosed : p.fv = ∅) (hlower : lowerClosed p = some f) (hrealize : Fol.realizeSentence S (Foundation.Formula.toFlypitch f)) : Wff.Valid S p

Any realized closed lowering is globally valid in the nominal evaluator.

theorem NFChoice.SemanticCore.PartialLowering.valid_open_of_closed_lowering {S : Fol.Structure Foundation.LNF} (names : List Var) (p : Wff) (f : Foundation.Sentence) (hcover : p.fv ⊆ names.toFinset) (hlower : lowerClosed (closeNames names p) = some f) (hrealize : Fol.realizeSentence S (Foundation.Formula.toFlypitch f)) : Wff.Valid S p

Generic NF-leaf bridge. The compiler supplies only a reduction-checkable lowering equation for the source schema's universal closure; the theorem turns realization of that exact literal sentence into validity of the open nominal schema.