A Δ₀ description of the satisfaction table

The external semantic recursion has already produced the uniform satisfaction table. The question is now how a formula interpreted in L can recognize a candidate set as that same graph. We will package the environment tower, formula code domain, the table's two domain conditions, and its ten recursive constructor clauses into a bounded description that later formulas can quantify over.

{-# OPTIONS --cubical --safe --guardedness #-}

The construction remains relative to excluded middle at level ℓ-suc ℓ. This hypothesis supports the coding and satisfaction machinery used below; it is carried explicitly rather than turned into an additional property of the candidate table.

open import Base.Prelude
open import Base.Classical using ( LEM )

Fix a universe level ℓ and this single classical hypothesis. Every object used in the description, from constructible sets to encoded formula keys, lives at the corresponding level, so no stronger classical assumption enters the result.

module L.GCH.SatisfactionDescription {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

The final description is built by conjoining three formulas. Its syntactic goal is a Δ₀ certificate: every quantifier in the description remains bounded. This boundedness is the precise condition that later allows satisfaction in L to be compared with satisfaction in the ambient hierarchy.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using
  ( Formula; _∧̇_ )
open import FOL.LevyHierarchy using ( Δ₀; δ-∧ )
import FOL.Absoluteness

Three kinds of encoded data must agree. Formula keys belong to the canonical set AllCodes W; an arity k points to the environment set envSet W k; and ordered pairs package keys with their semantic values. Membership in AllCodes W reveals a formula key only under propositional truncation, a boundary that every later decoding step preserves.

open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet )
open import L.Coding.CodeSet {ℓ} lem using ( AllCodes; AllCodes-out; key∈AllCodes; keyS )

For each genuine formula key, the semantic recursion produces a satisfaction set SatW ψ, while the functional table records the corresponding value. The bounded description does not rerun that recursion internally. It lists ten local constructor clauses, and a structural argument shows that any candidate obeying them is pinned to the externally defined value at every genuine key.

open import L.Coding.UniformSatisfaction {ℓ} lem using ( module Table; val-at )
open import L.Coding.PinnedRecursion {ℓ} lem using ( module Match ) public
open import L.Coding.PinnedRecursion {ℓ} lem using ( module SatSoundC; module SatHoldsC )
open import L.Coding.Quantification {ℓ} using ( f0; down )
open import L.Coding.CodeAlphabet {ℓ} using ( module Alphabet )

The constructor clauses can be read only after their domain is controlled. The candidate code domain must contain all genuine formula keys and admit only such keys, while the environment tower relates each natural-number arity to the environments of that length. These two descriptions supply the induction with exactly the subformula keys and environments it needs.

open import L.Coding.CodeDomain {ℓ} using ( Tags; codesAt; Δ₀-codesAt )
open import L.Coding.CodeDomainAdequacy {ℓ} lem
  using ( module CodesSound; module CodesComplete; module CodesHolds )
open import L.Coding.EnvironmentTower {ℓ} lem
  using ( towerAt; Δ₀-towerAt; module Tower; module TowerRead; module TowerHolds )

The remaining object is the graph of the uniform table. Its entries are encoded pairs of a formula key and a satisfaction set. The ten bounded clauses describe how the second component depends on the constructor encoded by the first, and the real graph will provide the completeness witness for those clauses.

open import L.Coding.SatisfactionClauses {ℓ} using ( tableAt; Δ₀-tableAt )
open import L.Coding.SatisfactionClauseSemantics {ℓ} lem using ( module Frame; module Bridge )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )

An interpreting environment is a finite vector of constructible sets, and its indices identify the table, working set, code domain, tower, and numeral tags. Dependent pairs express the witnesses returned by the readers. Whenever such a witness is propositionally truncated, it may be used only to prove another proposition, never as globally chosen data.

open import Cubical.Data.Vec using ( lookup )
open import Cubical.Data.Sigma using ( _×_ )
open import Cubical.Foundations.HLevels using ( isPropΣ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )

Natural-number arities are represented inside the cumulative hierarchy by the numerals # k. Thus an environment-tower entry is encoded as the pair of # k with envSet W k. Equality is always asserted between the underlying hierarchy sets, which is the level at which the coding theorems operate.

open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_ )

Write S for the carrier of the constructible structure. An element of S consists of an underlying hierarchy set together with evidence of constructibility. The table readers compare the underlying sets; they do not assert equality of the accompanying constructibility evidence.

open hPropStructure 𝒮ʟ using ( S )

Formulas in this chapter are interpreted inside L, with finite environments in S. Their boundedness later permits comparison with the ambient hierarchy, but the present soundness argument first works entirely with this internal satisfaction relation.

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans using ( _^_; _⊨ᵐ_ )
open AbsL using ( _^_ ) renaming ( _⊨ᵐ_ to _⊨_ )

Soundness of the bounded description

For soundness, fix candidate sets T, C, and E, a working set W, ten numeral tags, and the environment in which they are read. Assume separately that the tower, code-domain, and table descriptions hold, and align only the working-set slot with W. None of the three description hypotheses follows from the other two.

module SatSound {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N)
  (hE : ⟨ γ ⊨ towerAt E w (N f0) ⟩) (hC : ⟨ γ ⊨ codesAt C w E N ⟩)
  (hT : ⟨ γ ⊨ tableAt T w C E N ⟩) where
  open Alphabet W

Let Tv, Cv, and Ev denote the underlying sets presented by the candidate table, code domain, and environment tower. The clause semantics supplies the bridge from bounded formulas about these sets to the ambient membership and equality facts needed by the structural argument.

  open Bridge W
  private
    Tv = fst (lookup T γ)
    Cv = fst (lookup C γ)
    Ev = fst (lookup E γ)

Suppose an entry of Ev is already presented as the encoded pair of n and F. Reading the tower yields, under propositional truncation, an arity k with n = # k; forgetting the accompanying equation F = envSet W k gives exactly the arity fact needed to analyze candidate formula keys. The converse tower reading places every genuine arity entry in Ev, so genuine keys can also be inserted into Cv.

    module TR = TowerRead E w (N f0) γ W qw (tg f0) hE
    arity : (n F : S) → ⟨ pr (fst n) (fst F) ∈ Ev ⟩ → ∥ Σ[ k ∈ ℕ ] (fst n ≡ # k) ∥₁
    arity n F q∈ = PT.map (λ { (k , (qk , _)) → k , qk }) (TR.entry-out n F q∈)
    module CS = CodesSound C w E N γ W qw tg arity (hC .fst)
    module CC = CodesComplete C w E N γ W qw tg TR.entry-in (hC .snd)

The hypothesis hT consists of totality, the on-domain condition, and the ten constructor clauses, and Frame supplies their semantic readings. The pinning argument in SatSoundC uses totality and the ten clauses together with the tower facts and closure of the candidate code domain. It does not need the on-domain condition, because the entry to be pinned is already given as a pair at a genuine formula key; that condition will instead be used when reading an arbitrary presented table pair below.

    module Fr = Frame T w C E N γ tg
    module SC = SatSoundC T w C E N γ W qw tg hE CS.closed hT

The two domain conditions have complementary forms. Totality gives, for every c in Cv, merely some y with pr c y in Tv. The on-domain condition starts from an arbitrary member e of Tv and, again under propositional truncation, decomposes it as pr c y with c in Cv. Neither condition chooses values or pair components globally, and neither alone makes the table single-valued.

    hTot = hT .fst
    hOn = hT .snd .fst

Apply totality to the genuine key of a formula a, using the fact that code-domain completeness places that key in Cv. The result merely says that some value is paired with the key in Tv: the witness remains under propositional truncation. It supplies no chosen value or decoding function, and it will later be eliminated only into a proposition.

    sub : ∀ {n} (a : Formula Ab n) → ∥ Σ[ ya ∈ S ] ⟨ pr (fst (keyS W a)) (fst ya) ∈ Tv ⟩ ∥₁
    sub a = Fr.total-out hTot (keyS W a) (CC.key-in a)

The pinning predicate says: whenever a value y is paired with the key of ψ in the candidate table, the underlying set of y equals the recursively defined satisfaction set of ψ. It pins the underlying set only; the constructibility certificate of y and the formula itself are not fixed by it.

  Pinned : ∀ {n} (ψ : Formula Ab n) → Type (ℓ-suc ℓ)
  Pinned ψ = (y : S) → ⟨ pr (fst (keyS W ψ)) (fst y) ∈ Tv ⟩ → fst y ≡ fst (SatW ψ)

The proof proceeds by structural recursion on ψ. Closure of Cv supplies the keys of the immediate subformulas, and totality supplies their table values only under propositional truncation. The recursive hypotheses pin those child values; the matching constructor clause then gives the same extensional condition as the semantic recursion, so extensionality pins the parent value. The fact CC.key-in ψ supplies the candidate-domain membership needed to start this argument at the key of ψ.

  pinned : ∀ {n} (ψ : Formula Ab n) → Pinned ψ
  pinned ψ = SC.pinned ψ (CC.key-in ψ)

Every member of the candidate code domain belongs to the canonical code set. The candidate-key reader reveals an arity, a formula, and a key equation only under propositional truncation. Since the desired canonical membership is a proposition, the witness may be eliminated there and membership transported along its equation; no formula is selected by this argument.

  C-out : (c : S) → ⟨ fst c ∈ Cv ⟩ → ⟨ fst c ∈ fst (AllCodes W) ⟩
  C-out c c∈ = PT.rec (snd (fst c ∈ fst (AllCodes W)))
    (λ { (k , ψ , e) → subst (λ u → ⟨ u ∈ fst (AllCodes W) ⟩) (sym e) (key∈AllCodes W ψ) })
    (CS.key-out c c∈)

Conversely, every member of the canonical code set belongs to Cv. Canonical membership supplies a formula-key presentation under propositional truncation, and code-domain completeness inserts that key into the candidate domain. Again the witness is used only to prove membership, rather than to define a decoder.

  C-in : (c : S) → ⟨ fst c ∈ fst (AllCodes W) ⟩ → ⟨ fst c ∈ Cv ⟩
  C-in c c∈ = PT.rec (snd (fst c ∈ Cv))
    (λ { (k , ψ , e) → subst (λ u → ⟨ u ∈ Cv ⟩) (sym e) (CC.key-in ψ) })
    (AllCodes-out W c c∈)

The outward tower reading concerns an entry already presented as pr n F. Under propositional truncation it yields a natural number k with n = # k and F = envSet W k. It neither chooses k globally nor claims that this lemma alone supplies a coded-pair presentation for an arbitrary member of Ev.

  E-out : (n F : S) → ⟨ pr (fst n) (fst F) ∈ Ev ⟩
        → ∥ Σ[ k ∈ ℕ ] ((fst n ≡ # k) × (fst F ≡ fst (envSet W k))) ∥₁
  E-out = TR.entry-out

The inward tower reading supplies the complementary fact without propositional truncation: for each given natural number k, the standard entry pr (# k) (envSet W k) belongs to Ev. Together with the previous reading, this controls standard encoded entries in both directions without asserting a chosen arity for every arbitrary tower member.

  E-in : (k : ℕ) → ⟨ pr (# k) (fst (envSet W k)) ∈ Ev ⟩
  E-in = TR.entry-in

The table reading is the heart of the soundness direction. It is stated only for members already presented as the ordered pair of x and y; arbitrary members of the candidate table are not covered by this lemma.

  T-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ Tv ⟩
        → Σ[ mx ∈ ⟨ fst x ∈ fst (AllCodes W) ⟩ ] (fst y ≡ fst (Table.val W W x mx))
  T-out x y h = PT.rec (isPropΣ (snd (fst x ∈ fst (AllCodes W))) (λ mx → setIsSet _ _))
    (λ { (c , yc , (ee , c∈)) → PT.rec (isPropΣ (snd (fst x ∈ fst (AllCodes W))) (λ mx → setIsSet _ _))
      (λ { (k , ψ , e) →

The pairing equation splits into the first components of the two sides, and the code equation identifies the recorded key with the key of some decoded formula; the membership of that formula's key in the canonical code set follows by transport.

        let q = pr-inj ee
            qx : fst x ≡ fst (keyS W ψ)
            qx = q .fst ∙ e
            mx : ⟨ fst x ∈ fst (AllCodes W) ⟩
            mx = subst (λ u → ⟨ u ∈ fst (AllCodes W) ⟩) (sym qx) (key∈AllCodes W ψ)

Pinning identifies the recorded value with the recursive satisfaction set, and val-at identifies that set with the functional table value at the same key. The conclusion contains canonical code-set membership together with an equality of underlying sets. Although it is not propositionally truncated, it can be obtained from the truncated decoding because the entire dependent pair is itself a proposition; it is not computational decoding.

        in mx , ( pinned ψ y (subst (λ u → ⟨ u ∈ Tv ⟩) (cong (λ a → pr a (fst y)) qx) h)
                ∙ sym (cong fst (val-at W W ψ x mx qx)) ) })
      (CS.key-out c c∈) })
    (Fr.onC-out hOn (down (lookup T γ) (pr (fst x) (fst y)) h) h)

For the converse table reading, begin with a specified canonical code x. Its membership in AllCodes W gives, under propositional truncation, a formula ψ whose key is x. Totality then gives, again under propositional truncation, some candidate value recorded at that formula key.

  T-in : (x : S) (mx : ⟨ fst x ∈ fst (AllCodes W) ⟩) → ⟨ pr (fst x) (fst (Table.val W W x mx)) ∈ Tv ⟩
  T-in x mx = PT.rec (snd (pr (fst x) (fst (Table.val W W x mx)) ∈ Tv))
    (λ { (k , ψ , e) → PT.rec (snd (pr (fst x) (fst (Table.val W W x mx)) ∈ Tv))
      (λ { (y , my) →
        subst (λ u → ⟨ u ∈ Tv ⟩)

The candidate value is pinned to the recursive satisfaction set, and the value lemma aligns it with the functional table value; the membership is then transported along the equation of the ordered pairs. Both eliminations land in the table membership, which is a proposition.

          (cong₂ pr (sym e) (pinned ψ y my ∙ sym (cong fst (val-at W W ψ x mx e))))
          my })
      (sub ψ) })
    (AllCodes-out W x mx)

Completeness and the two readings

Completeness starts from concrete semantic objects rather than an arbitrary candidate. The four environment slots are aligned separately with W, the real graph SatGraph.pairs W, the canonical code set AllCodes W, and the real tower Tower.tower W; the ten tags are also fixed. These alignments are hypotheses, not consequences of the bounded clauses.

module SatHolds {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (qT : fst (lookup T γ) ≡ fst (SatGraph.pairs W))
  (qC : fst (lookup C γ) ≡ fst (AllCodes W)) (qE : fst (lookup E γ) ≡ fst (Tower.tower W))
  (tg : Tags γ N) where
  open Alphabet W

Write Tv and Cv for the underlying sets in the table and code-domain slots. The alignments qT and qC transport their membership facts to the genuine graph and the canonical code set. Consequently, a presented table pair can be read with the graph lemmas, whereas a code is decoded only under propositional truncation. Every equality below still compares underlying hierarchy sets.

  open Bridge W
  private
    Tv = fst (lookup T γ)
    Cv = fst (lookup C γ)

A table value at a code identified with a formula key equals the recursive satisfaction set of that formula. The proof reads the pair out of the real satisfaction graph, transports its second component through the identification of the presented key with the formula key, and finishes with the value lemma.

    val≡ : ∀ {n} (ψ : Formula Ab n) (c yc : S) → fst c ≡ fst (keyS W ψ)
         → ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ → fst yc ≡ fst (SatW ψ)
    val≡ ψ c yc qc h =
      let p = SatGraph.pairs-out W c yc (subst (λ u → ⟨ pr (fst c) (fst yc) ∈ u ⟩) qT h)
      in p .snd ∙ cong fst (SatGraph.valOf≡ W c (p .fst)) ∙ cong fst (val-at W W ψ c (p .fst) qc)

If a code-domain member is presented as pr (# n) z, transporting it into AllCodes W permits decoding under propositional truncation: some formula ψ : Formula Ab n has payload z. This gives neither a chosen formula nor uniqueness of decoding, and therefore does not define a decoding function.

    decode : (c : S) → ⟨ fst c ∈ Cv ⟩ → (n : ℕ) (z : V ℓ) → fst c ≡ pr (# n) z
           → ∥ Σ[ ψ ∈ Formula Ab n ] (z ≡ cd ψ) ∥₁
    decode c c∈ = Match.decodeAll W c (subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈)

For a candidate code c, alignment with the canonical code set makes c a valid input to the real graph. Its real graph value provides a table entry, which is transported back along the alignment of Tv with SatGraph.pairs W. The resulting existence statement remains under propositional truncation, exactly as the totality clause requires.

    tot : (c : S) → ⟨ fst c ∈ Cv ⟩ → ∥ Σ[ yc ∈ S ] ⟨ pr (fst c) (fst yc) ∈ Tv ⟩ ∥₁
    tot c c∈ =
      let mx = subst (λ u → ⟨ fst c ∈ u ⟩) qC c∈
      in ∣ SatGraph.valOf W c mx , subst (λ u → ⟨ pr (fst c) (fst (SatGraph.valOf W c mx)) ∈ u ⟩) (sym qT) (SatGraph.pairs-in W c mx) ∣₁

The real graph also supplies the required shape of arbitrary table members. Under propositional truncation, every such member is an encoded pair of some code and its graph value, and that code belongs to Cv. This is an existence-only decomposition; it does not choose components for each member.

    onc : (e : S) → ⟨ fst e ∈ Tv ⟩
        → ∥ Σ[ c ∈ S ] Σ[ yc ∈ S ] ((fst e ≡ pr (fst c) (fst yc)) × ⟨ fst c ∈ Cv ⟩) ∥₁
    onc e e∈ = PT.map
      (λ { (x , mx , ee) → x , SatGraph.valOf W x mx , (ee , subst (λ u → ⟨ fst x ∈ u ⟩) (sym qC) mx) })
      (SatGraph.pairs-shape W e (subst (λ u → ⟨ fst e ∈ u ⟩) qT e∈))

The inputs to SatHoldsC.holds have distinct jobs. The real tower supplies the environment rows, val≡ identifies values at genuine formula keys, decode merely recovers a formula from a shaped code, and tot and onc establish the two domain conditions. The structural argument then verifies all ten constructor clauses. Whenever it consumes a propositionally truncated arity, formula, or decomposition, it eliminates that witness only into the proposition that the relevant clause is satisfied; no decoder or choice of table values escapes.

  holds : ⟨ γ ⊨ tableAt T w C E N ⟩
  holds = SatHoldsC.holds W T w C E N γ qw tg
    (TowerHolds.holds E w (N f0) γ W qw qE (tg f0)) val≡ decode tot onc

The sealed formula satAt packages three independent descriptions: towerAt, codesAt, and tableAt. The tower component is passed the tag slot N f0, which Tags identifies with the numeral zero; the code-domain and table components receive the whole ten-slot family N. This conjunction by itself adds no equality with the canonical tower, code set, or satisfaction graph.

opaque
  satAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin  → Fin m) → Formula S m
  satAt T w C E N = towerAt E w (N f0) ∧̇ (codesAt C w E N ∧̇ tableAt T w C E N)

Later arguments may treat satAt as one bounded predicate rather than repeatedly expanding its three components. Its definition is unfolded in a controlled scope when checking syntactic properties such as membership in the Lévy hierarchy; semantic use proceeds through the projection and completeness results below. Opacity marks this proof boundary and contributes no additional model-theoretic property.

opaque
  unfolding satAt

The certificate Δ₀-satAt uses closure of the bounded fragment under conjunction to combine the certificates for the three components. It establishes only the syntactic boundedness of satAt; it says nothing yet about which sets satisfy the formula. The semantic directions are supplied later by SatRead and sat-complete.

  Δ₀-satAt : ∀ {m} (T w C E : Fin m) (N : Fin  → Fin m) → Δ₀ (satAt T w C E N)
  Δ₀-satAt T w C E N = δ-∧ (Δ₀-towerAt E w (N f0)) (δ-∧ (Δ₀-codesAt C w E N) (Δ₀-tableAt T w C E N))

From a proof of satAt, one recovers the three precise hypotheses needed for soundness: the environment-tower description, the code-domain description, and the table description. This projection adds no semantic conclusion and supplies no equality with the canonical objects.

  satAt-out : ∀ {m} (T w C E : Fin m) (N : Fin  → Fin m) (γ : S ^ m)
            → ⟨ γ ⊨ satAt T w C E N ⟩
            → ⟨ γ ⊨ towerAt E w (N f0) ⟩ × (⟨ γ ⊨ codesAt C w E N ⟩ × ⟨ γ ⊨ tableAt T w C E N ⟩)
  satAt-out T w C E N γ h = h

Conversely, proofs of those three descriptions combine to establish satAt. The construction is purely conjunctive: each component must be supplied independently, so the table clause cannot compensate for a missing tower or code-domain clause.

  satAt-in : ∀ {m} (T w C E : Fin m) (N : Fin  → Fin m) (γ : S ^ m)
           → ⟨ γ ⊨ towerAt E w (N f0) ⟩ → ⟨ γ ⊨ codesAt C w E N ⟩ → ⟨ γ ⊨ tableAt T w C E N ⟩
           → ⟨ γ ⊨ satAt T w C E N ⟩
  satAt-in T w C E N γ hE hC hT = hE , (hC , hT)

SatRead is the soundness-facing interface for a candidate satisfying satAt. It applies only after the working-set slot has been aligned with W and Tags has calibrated the numeral slots, and it exports the six precise outward and inward rules proved above. Their original conclusion shapes are retained: the interface neither turns them into blanket set equalities nor exposes selected decoders or witnesses.

module SatRead {m : ℕ} (T w C E : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (W : S)
  (qw : fst (lookup w γ) ≡ fst W) (tg : Tags γ N) (h : ⟨ γ ⊨ satAt T w C E N ⟩) where
  private
    module SS = SatSound T w C E N γ W qw tg
      (satAt-out T w C E N γ h .fst) (satAt-out T w C E N γ h .snd .fst) (satAt-out T w C E N γ h .snd .snd)

For codes, the two directions compare membership with AllCodes W. For tower entries, they read or insert standard pairs pr (# k) (envSet W k). For table entries, they compare a presented pair with the functional table value at a canonical code. Keeping these three conclusion shapes distinct prevents a stronger, unsupported uniqueness claim.

  open SS public using ( C-out; C-in; E-out; E-in; T-out; T-in )

The converse theorem assumes that the four slots already present the intended objects: W, its satisfaction graph, its complete code set, and its environment tower. It also assumes the ten correct numeral tags. These alignments are input data for completeness and are not recovered from satAt.

sat-complete : ∀ {m} (T w C E : Fin m) (N : Fin  → Fin m) (γ : S ^ m) (W : S)
             → fst (lookup w γ) ≡ fst W
             → fst (lookup T γ) ≡ fst (SatGraph.pairs W)
             → fst (lookup C γ) ≡ fst (AllCodes W)
             → fst (lookup E γ) ≡ fst (Tower.tower W)

The conclusion is a satisfaction proof for the already aligned environment. The proof first fills the tower and code-domain components from qw, qE, qC, and the calibrated tags; those alignments remain assumptions throughout. This step introduces no existential witness for a new tower, code set, or graph, and it does not claim that every quadruple satisfying satAt is uniquely canonical.

             → Tags γ N → ⟨ γ ⊨ satAt T w C E N ⟩
sat-complete T w C E N γ W qw qT qC qE tg =
  satAt-in T w C E N γ
    (TowerHolds.holds E w (N f0) γ W qw qE (tg f0))
    (CodesHolds.holds C w E N γ W qw qC qE tg)

The final line supplies the table conjunct by reusing SatHolds.holds. As proved above, this establishes all of tableAt: its two domain conditions and its ten constructor clauses, rather than only the ten clauses. satAt-in combines that result with the tower and code-domain conjuncts. Thus sat-complete writes already aligned canonical data into the bounded description; the propositionally truncated decoding used inside the table proof exposes no global decoder or selected value.

    (SatHolds.holds T w C E N γ W qw qT qC qE tg)