NF weak partition development: NFStandard.HailperinAlgebra.

Exact products, cylindrification, and sections

noncomputable def NFChoice.Foundation.NFStandard.crossObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B : S.carrier) : S.carrier

Cartesian product of two set objects.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_crossObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (A B a b : S.carrier) : SemanticCore.Mem S (kPair hH a b) (crossObj hH A B) ↔ SemanticCore.Mem S a A ∧ SemanticCore.Mem S b B

@[simp]

theorem NFChoice.Foundation.NFStandard.valuationCode_nil {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (cap : ℤ) (ty : Fin 0 → ℤ) : valuationCode hH cap ty DVec.nil = oneC hH

@[simp]

theorem NFChoice.Foundation.NFStandard.valuationCode_one {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) (cap k : ℤ) (a : S.carrier) : valuationCode hH cap (fun (i : Fin (0 + 1)) => Fin.cases k Fin.elim0 i) (DVec.cons a DVec.nil) = raise hH (capOffset cap k) a

@[simp]

theorem NFChoice.Foundation.NFStandard.valuationCode_cons_succ {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap k : ℤ) (ty : Fin (n + 1) → ℤ) (a : S.carrier) (xs : DVec S.carrier (n + 1)) : valuationCode hH cap (fun (i : Fin (n + 1 + 1)) => Fin.cases k ty i) (DVec.cons a xs) = kPair hH (raise hH (2 * n) (raise hH (capOffset cap k) a)) (valuationCode hH cap ty xs)

theorem NFChoice.Foundation.NFStandard.valuationCode_cons {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin (n + 2) → ℤ) (a : S.carrier) (xs : DVec S.carrier (n + 1)) : valuationCode hH cap ty (DVec.cons a xs) = kPair hH (raise hH (2 * n) (raise hH (capOffset cap (ty 0)) a)) (valuationCode hH cap (fun (i : Fin (n + 1)) => ty i.succ) xs)

noncomputable def NFChoice.Foundation.NFStandard.existsSetObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} : ℤ → (Fin n → ℤ) → ℤ → S.carrier → S.carrier

Existentially discard the newest coordinate. At positive output arity this is the exact raised image of the input set. At arity zero the result is a truth flag observed at the fixed nullary tuple sentinel.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_existsSetObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (k : ℤ) (A : S.carrier) (xs : DVec S.carrier n) : SemanticCore.Mem S (valuationCode hH cap ty xs) (existsSetObj hH cap ty k A) ↔ ∃ (a : S.carrier), SemanticCore.Mem S (valuationCode hH cap (fun (i : Fin (n + 1)) => Fin.cases k ty i) (DVec.cons a xs)) A

noncomputable def NFChoice.Foundation.NFStandard.sliceObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} : ℤ → (Fin (n + 1) → ℤ) → S.carrier → DVec S.carrier n → S.carrier

Fix the tail coordinates and lower the normalized head back to a set.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Foundation.NFStandard.sliceObj hH x✝¹ ty x✝ x_5 = NFChoice.Foundation.NFStandard.unitUnionIter hH (NFChoice.Foundation.NFStandard.capOffset x✝¹ (ty 0)) x✝

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_sliceObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin (n + 1) → ℤ) (A : S.carrier) (xs : DVec S.carrier n) (z : S.carrier) : SemanticCore.Mem S z (sliceObj hH cap ty A xs) ↔ SemanticCore.Mem S (valuationCode hH cap ty (DVec.cons z xs)) A

Coordinate selectors

headRel j R lifts a binary relation R to homogeneous tuple codes and tests the head against coordinate j. Ins3 handles the next coordinate; Ins2 skips it and recurses. This is precisely the purpose of the two inserted-pair primitives in the Metamath Hailperin-derived finite basis.

noncomputable def NFChoice.Foundation.NFStandard.headRel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} : Fin n → S.carrier → S.carrier

Test the head and coordinate j of a homogeneous tuple against R.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Foundation.NFStandard.headRel hH j x✝ = j.elim0
• NFChoice.Foundation.NFStandard.headRel hH x_3 x✝ = NFChoice.Foundation.NFStandard.universalObj hH
• NFChoice.Foundation.NFStandard.headRel hH j x✝ = Fin.cases (NFChoice.Foundation.NFStandard.universalObj hH) (fun (x : Fin 1) => x✝) j

theorem NFChoice.Foundation.NFStandard.mem_headRel_or_zero {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (j : Fin (n + 1)) (R : S.carrier) (xs : DVec S.carrier (n + 1)) : j = 0 ∨ (SemanticCore.Mem S (htuple hH xs) (headRel hH j R) ↔ SemanticCore.Mem S (kPair hH (SemanticCore.Lowering.lookup xs 0) (SemanticCore.Lowering.lookup xs j)) R)

theorem NFChoice.Foundation.NFStandard.mem_headRel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (j : Fin (n + 1)) (hj : j ≠ 0) (R : S.carrier) (xs : DVec S.carrier (n + 1)) : SemanticCore.Mem S (htuple hH xs) (headRel hH j R) ↔ SemanticCore.Mem S (kPair hH (SemanticCore.Lowering.lookup xs 0) (SemanticCore.Lowering.lookup xs j)) R

noncomputable def NFChoice.Foundation.NFStandard.coordinateRel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} : Fin n → Fin n → S.carrier → S.carrier

Test arbitrary distinct coordinates of a homogeneous tuple against R.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.Foundation.NFStandard.coordinateRel hH i x_4 x✝ = i.elim0

theorem NFChoice.Foundation.NFStandard.mem_coordinateRel_or_eq {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (i j : Fin (n + 1)) (R : S.carrier) (xs : DVec S.carrier (n + 1)) : i = j ∨ (SemanticCore.Mem S (htuple hH xs) (coordinateRel hH i j R) ↔ SemanticCore.Mem S (kPair hH (SemanticCore.Lowering.lookup xs i) (SemanticCore.Lowering.lookup xs j)) R)

theorem NFChoice.Foundation.NFStandard.mem_coordinateRel {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (i j : Fin (n + 1)) (hij : i ≠ j) (R : S.carrier) (xs : DVec S.carrier (n + 1)) : SemanticCore.Mem S (htuple hH xs) (coordinateRel hH i j R) ↔ SemanticCore.Mem S (kPair hH (SemanticCore.Lowering.lookup xs i) (SemanticCore.Lowering.lookup xs j)) R

Atomic relations on normalized valuation codes

noncomputable def NFChoice.Foundation.NFStandard.eqSetObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (i j : Fin n) : S.carrier

Equality atom at arbitrary coordinates.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_eqSetObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (_hcap : ∀ (i : Fin n), ty i ≤ cap) (i j : Fin n) (h : ty i = ty j) (xs : DVec S.carrier n) : SemanticCore.Mem S (valuationCode hH cap ty xs) (eqSetObj hH cap ty i j) ↔ SemanticCore.Lowering.lookup xs i = SemanticCore.Lowering.lookup xs j

noncomputable def NFChoice.Foundation.NFStandard.memSetObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (i j : Fin n) : S.carrier

Membership atom at arbitrary coordinates.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem NFChoice.Foundation.NFStandard.mem_memSetObj {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) {n : ℕ} (cap : ℤ) (ty : Fin n → ℤ) (hcap : ∀ (i : Fin n), ty i ≤ cap) (i j : Fin n) (h : ty j = ty i + 1) (xs : DVec S.carrier n) : SemanticCore.Mem S (valuationCode hH cap ty xs) (memSetObj hH cap ty i j) ↔ SemanticCore.Mem S (SemanticCore.Lowering.lookup xs i) (SemanticCore.Lowering.lookup xs j)

The complete cap-aware cylinder algebra

noncomputable def NFChoice.Foundation.NFStandard.hailperinCylinderAlgebra {S : Fol.Structure LNF} (hH : Fol.allRealizeSentence S ExactLiteralTrial.LiteralHailperinNF) : CylinderAlgebra S

the Metamath Hailperin-derived finite basis supplies the full uniform cylinder compiler.

Equations

• One or more equations did not get rendered due to their size.