The query-code closed embedding (issue #10, Unit 0a)

The frozen named query encoding of the López–Escobar audit (D3, v2): a fixed embedding queryEmbedding : RelQuery L ↪ ℕ and the induced code map

queryCode : StructureSpace L → (ℕ → Bool)

sending a structure code to its bit sequence along the embedding, false outside the embedding's range. The four gates, plus the capstone:

• queryCode_embedding — every query is recovered at its encoded coordinate;
• queryCode_of_notMem_range — coordinates outside the embedding's range are false;
• range_queryCode — range membership is the default condition, and the range is closed as an intersection of clopen coordinate conditions (isClosed_range_queryCode);
• queryCode_isClosedEmbedding — the capstone, via the continuous retraction decodeCode and Function.LeftInverse.isClosedEmbedding.

This is the stop/go gate's first half; the analytic tree normal form (Unit 0b) builds the cylinder tree in (ℕ → Bool) × (ℕ → ℕ) on top of it.

@[reducible]

noncomputable def FirstOrder.Language.queryEncodable {L : Language} [Countable ((l : ℕ) × L.Relations l)] : Encodable L.RelQuery

The frozen query encoding — one named Encodable witness, never re-synthesized.

Equations

• FirstOrder.Language.queryEncodable = Encodable.ofCountable L.RelQuery

noncomputable def FirstOrder.Language.queryEmbedding {L : Language} [Countable ((l : ℕ) × L.Relations l)] : L.RelQuery ↪ ℕ

The frozen query embedding RelQuery L ↪ ℕ (audit D3, v2).

Equations

• FirstOrder.Language.queryEmbedding = { toFun := Encodable.encode, inj' := ⋯ }

noncomputable def FirstOrder.Language.queryCode {L : Language} [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (n : ℕ) : Bool

The query code of a structure code: the bit at coordinate n is the code's value at the query encoded by n, and false when n encodes no query.

Equations

• FirstOrder.Language.queryCode c n = if h : ∃ (q : L.RelQuery), FirstOrder.Language.queryEmbedding q = n then c h.choose else false

noncomputable def FirstOrder.Language.decodeCode {L : Language} [Countable ((l : ℕ) × L.Relations l)] (x : ℕ → Bool) : L.StructureSpace

The continuous retraction: read the structure code back off the embedded coordinates.

Equations

• FirstOrder.Language.decodeCode x q = x (FirstOrder.Language.queryEmbedding q)

@[simp]

theorem FirstOrder.Language.queryCode_embedding {L : Language} [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) (q : L.RelQuery) : queryCode c (queryEmbedding q) = c q

Gate 1: every query is recovered at its encoded coordinate.

theorem FirstOrder.Language.queryCode_of_notMem_range {L : Language} [Countable ((l : ℕ) × L.Relations l)] (c : L.StructureSpace) {n : ℕ} (h : n ∉ Set.range ⇑queryEmbedding) : queryCode c n = false

Gate 2: coordinates outside the embedding's range are false.

theorem FirstOrder.Language.decodeCode_queryCode {L : Language} [Countable ((l : ℕ) × L.Relations l)] : Function.LeftInverse decodeCode queryCode

theorem FirstOrder.Language.queryCode_injective {L : Language} [Countable ((l : ℕ) × L.Relations l)] : Function.Injective queryCode

theorem FirstOrder.Language.continuous_queryCode {L : Language} [Countable ((l : ℕ) × L.Relations l)] : Continuous queryCode

theorem FirstOrder.Language.continuous_decodeCode {L : Language} [Countable ((l : ℕ) × L.Relations l)] : Continuous decodeCode

theorem FirstOrder.Language.range_queryCode {L : Language} [Countable ((l : ℕ) × L.Relations l)] : Set.range queryCode = {x : ℕ → Bool | ∀ n ∉ Set.range ⇑queryEmbedding, x n = false}

Gate 3 (range characterization): the range of queryCode is exactly the default condition — false at every coordinate outside the embedding's range.

theorem FirstOrder.Language.isClosed_range_queryCode {L : Language} [Countable ((l : ℕ) × L.Relations l)] : IsClosed (Set.range queryCode)

Gate 4: the range is closed — an intersection of clopen coordinate conditions.

theorem FirstOrder.Language.queryCode_isClosedEmbedding {L : Language} [Countable ((l : ℕ) × L.Relations l)] : Topology.IsClosedEmbedding queryCode

The capstone: queryCode is a closed embedding.