---
title: "A Δ₀ description of the satisfaction table"
module: L.GCH.SatisfactionDescription
lang: en
site: "Bedrock"
description: "A Δ₀ description of the satisfaction table"
stage: "Proving GCH"
reading_order: 100
canonical: https://bedrock.institute/en/L.GCH.SatisfactionDescription.html
html: L.GCH.SatisfactionDescription.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/SatisfactionDescription.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.LevyHierarchy, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.EnvironmentSet, L.Coding.CodeSet, L.Coding.UniformSatisfaction, L.Coding.PinnedRecursion, L.Coding.Quantification, L.Coding.CodeAlphabet, L.Coding.CodeDomain, L.Coding.CodeDomainAdequacy, L.Coding.EnvironmentTower, L.Coding.SatisfactionClauses, L.Coding.SatisfactionClauseSemantics, L.Coding.SatisfactionGraphSet]
routes: [gch-descriptions]
translations: [https://bedrock.institute/zh/L.GCH.SatisfactionDescription.md, https://bedrock.institute/ja/L.GCH.SatisfactionDescription.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
module SatSound {m : ℕ} (T w C E : Fin m) (N : Fin 10 → 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.

```agda
  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`.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
  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 `ψ`.

```agda
  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.

```agda
  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.

```agda
  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`.

```agda
  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.

```agda
  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.

```agda
  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.

```agda
        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.

```agda
        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.

```agda
  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.

```agda
          (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.

```agda
module SatHolds {m : ℕ} (T w C E : Fin m) (N : Fin 10 → 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.

```agda
  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.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
    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.

```agda
  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.

```agda
opaque
  satAt : ∀ {m} → Fin m → Fin m → Fin m → Fin m → (Fin 10 → 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.

```agda
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`.

```agda
  Δ₀-satAt : ∀ {m} (T w C E : Fin m) (N : Fin 10 → 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.

```agda
  satAt-out : ∀ {m} (T w C E : Fin m) (N : Fin 10 → 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.

```agda
  satAt-in : ∀ {m} (T w C E : Fin m) (N : Fin 10 → 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.

```agda
module SatRead {m : ℕ} (T w C E : Fin m) (N : Fin 10 → 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.

```agda
  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`.

```agda
sat-complete : ∀ {m} (T w C E : Fin m) (N : Fin 10 → 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.

```agda
             → 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.

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