NF weak partition development: ReplaySupport.Basic.

def NFChoice.ReplaySupport.freshVar (support : Finset SemanticCore.Var) (offset : ℕ := 0) : SemanticCore.Var

A deterministic supply of nominal variables strictly above a finite support.

Equations

• NFChoice.ReplaySupport.freshVar support offset = support.sup id + offset + 1

theorem NFChoice.ReplaySupport.mem_lt_freshVar {support : Finset SemanticCore.Var} {x : SemanticCore.Var} (hx : x ∈ support) (offset : ℕ := 0) : x < freshVar support offset

theorem NFChoice.ReplaySupport.freshVar_not_mem (support : Finset SemanticCore.Var) (offset : ℕ := 0) : freshVar support offset ∉ support

theorem NFChoice.ReplaySupport.freshVar_not_mem_of_subset {small support : Finset SemanticCore.Var} (hsubset : small ⊆ support) (offset : ℕ := 0) : freshVar support offset ∉ small

theorem NFChoice.ReplaySupport.freshVar_injective (support : Finset SemanticCore.Var) {i j : ℕ} (hij : i ≠ j) : freshVar support i ≠ freshVar support j

theorem NFChoice.ReplaySupport.realizes_literal_axiom {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (name : Foundation.HailperinAxiomName) : Fol.realizeSentence S (Foundation.ExactLiteralTrial.literalAxiomFormula name)

Every exact Hailperin axiom is available in a model of the literal theory.

theorem NFChoice.ReplaySupport.extensional_of_literal_model {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) : SemanticCore.Extensional S

Extensionality extracted from the exact ax-ext member of the theory.

theorem NFChoice.ReplaySupport.valid_literal_leaf {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (name : Foundation.HailperinAxiomName) (names : List SemanticCore.Var) (p : SemanticCore.Wff) (hcover : p.fv ⊆ names.toFinset) (hlower : SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames names p) = some (Foundation.ExactLiteralTrial.literalAxiomSyntax name)) : SemanticCore.Wff.Valid S p

Generic bridge used by generated concrete NF-leaf certificates. The generated file supplies only a finite support inclusion and a reduction-checkable lowering equation for the universally closed source instance.

theorem NFChoice.ReplaySupport.derives_not_of_nominal_validity (p : SemanticCore.Wff) (f : Foundation.Sentence) (hpClosed : p.fv = ∅) (hlower : SemanticCore.PartialLowering.lowerClosed p = some f) (hsemantic : ∀ (S : Fol.Structure Foundation.LNF), Nonempty S.carrier → Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF → SemanticCore.Wff.Valid S p.neg) : Foundation.ExactLiteralTrial.LiteralHailperinNF.sprovable (Fol.bdNot (Foundation.Formula.toFlypitch f))

Completeness boundary for the control experiment. Once the generated replay has proved nominal validity of neg p in every literal-Hailperin model, this theorem produces the requested object-level first-order derivability result.