The graph-relationalization spike (issue #10, Unit 1 part 2)

The two remaining Unit-1 acceptance gates of audit v2 (D4, graph-translation route):

• the relationalization micro-pilot — a nested numeral formula (f(s(c)) = s(c), Marker's bullet-2 shape) mapped into the tagged KLang L along the left-witness embedding, relationalized through the Craig Layer-3 files, with its realization verified through graphExpansion all the way back to the witness-language semantics (pilot_realize), plus the side-specific graph axioms realized by the expansion (pilot_graphAxioms);
• the decisive occurrence theorem (occurrence_intersection_base) — the intersection of the two sides' complete relationalized symbol sets, graph axioms included, contains only graph-language images of base-L symbols. No witness symbol survives: left/right witness symbols are disjoint (WitnessLang.lean), equality introduces no relation symbols (relationsIn_relationalizeFormula, .equal case), and the sharp calculation is Craig's relSym_inter.

With this compiled, the graph-language route is frozen and the hand-rolled relational vocabulary of the audit's D4 is retired to its historical fallback note.

instance FirstOrder.Language.instCountableElemSigmaNatFunctionsFunctionsIn {L' : Language} {α : Type} {n : ℕ} (ψ : L'.BoundedFormulaω α n) : Countable ↑ψ.functionsIn

Countability of a formula's function-symbol occurrence set, as an instance (feeds graphAxioms).

instance FirstOrder.Language.instCountableElemSigmaNatFunctionsKLangLeftFuns (L : Language) : Countable ↑L.leftFuns

instance FirstOrder.Language.instCountableElemSigmaNatFunctionsKLangRightFuns (L : Language) : Countable ↑L.rightFuns

The micro-pilot

def FirstOrder.Language.pilotFormula : WitnessLang.Sentenceω

The pilot formula f(s(c)) = s(c) — Marker's bullet-2 shape, with a nested numeral.

Equations

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

theorem FirstOrder.Language.pilot_realize (L : Language) {M : Type} [instM : L.KLang.Structure M] : (relationalizeFormula (BoundedFormulaω.mapLanguage L.leftWitnessEmb pilotFormula)).Realize Empty.elim Fin.elim0 ↔ pilotFormula.Realize M

Micro-pilot, realization: the relationalized image of the mapped pilot formula realizes through the graph expansion exactly as the pilot formula realizes through the left-witness reduct.

theorem FirstOrder.Language.pilot_graphAxioms (L : Language) {M : Type} [Nonempty M] [L.KLang.Structure M] : (graphAxioms L.leftFuns).Realize M

Micro-pilot, side-specific graph axioms: the graph expansion of any tagged structure realizes the left-witness graph axioms.

The decisive occurrence theorem

theorem FirstOrder.Language.occurrence_intersection_base (L : Language) (ψ₀ ψ₁ : L.KLang.Sentenceω) (hF₀ : BoundedFormulaω.functionsIn ψ₀ ⊆ L.baseFuns ∪ L.leftFuns) (hR₀ : BoundedFormulaω.relationsIn ψ₀ ⊆ L.baseRels ∪ L.leftRels) (hF₁ : BoundedFormulaω.functionsIn ψ₁ ⊆ L.baseFuns ∪ L.rightFuns) (hR₁ : BoundedFormulaω.relationsIn ψ₁ ⊆ L.baseRels ∪ L.rightRels) : (BoundedFormulaω.and (graphAxioms (BoundedFormulaω.functionsIn ψ₀)) (relationalizeFormula ψ₀)).relationsIn ∩ (BoundedFormulaω.and (graphAxioms (BoundedFormulaω.functionsIn ψ₁)) (relationalizeFormula ψ₁)).relationsIn ⊆ L.KLang.relSym L.baseFuns L.baseRels

The decisive occurrence theorem (Unit-1 acceptance gate): for two KLang-sentences whose symbols lie in base-plus-left and base-plus-right respectively, the intersection of their complete relationalized symbol sets — graph axioms included — contains only graph-language images of base-L symbols. No witness symbol survives.