---
title: "The satisfaction graph formula"
module: L.Coding.SatisfactionGraph
lang: en
site: "Bedrock"
description: "The satisfaction graph formula"
stage: "Internal coding: tables and uniform satisfaction"
reading_order: 67
canonical: https://bedrock.institute/en/L.Coding.SatisfactionGraph.html
html: L.Coding.SatisfactionGraph.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/SatisfactionGraph.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Model, L.Coding.Closure, L.Coding.Quantification, L.Coding.EnvironmentTower, L.Coding.CodeDomain, L.Coding.SatisfactionClauses]
routes: [internal-satisfaction]
translations: [https://bedrock.institute/zh/L.Coding.SatisfactionGraph.md, https://bedrock.institute/ja/L.Coding.SatisfactionGraph.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# The satisfaction graph formula

The recursive construction `Sat` assigns a set of satisfying environments to each formula, but that metatheoretic assignment cannot simply be named inside a first-order definition over `L`. The task of this chapter is to give a binary object-language formula that can later serve as the relation for such queries. Its witnesses will describe enough local data to satisfy the recursion equations around the queried key, without assuming in advance that a canonical or single-valued table has already been obtained.

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

Excluded middle is available at the required universe level because the environment-tower interface used below carries that assumption. The formula assembled in this chapter does not itself decide propositions by cases; its quantifiers and connectives receive their meaning from the established first-order semantics.

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

Fix a universe level and this one classical parameter. The relation to be defined holds of a formula key `x` and a set `y` exactly when some locally qualified candidate satisfaction table over the carrier records `y` at `x`. At this stage it asserts only the existence of such local data; it neither selects a canonical table nor proves that every key has a unique value.

```agda
module L.Coding.SatisfactionGraph {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

The formula language provides variables, constants, equality, conjunction, and existential quantification. Constants allow fixed constructible sets, such as the standard numerals used for tags, to occur directly in a formula, while `pr` encodes the ordered pairs used as graph entries. The ambient hierarchy supplies the semantics in which these formulas will be read.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _≐_; _∧̇_; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
```

Three descriptions organize the candidate data. `appAt` reads an encoded pair as a graph entry, `domAt T C` says that the key domain of the table `T` is exactly `C`, and `closedAt C` requires the keys in `C` to contain the direct subformula keys needed by compound formulas. The domain in `domAt` is the table's domain of keys; it is distinct from the environment sets that later occur as table values.

```agda
open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Model {ℓ} using ( domAt; appAt; appAt-adequate )
open import L.Coding.Closure {ℓ} using ( closedAt )
open import L.Coding.Quantification {ℓ} using
  ( f0; f1; f2; f3; f4; f5; f6; f7; f8; f9; i0; i1; i2; i3; i4; i5; i6; i7; i8; i9; i10; i11; i12; i13; sh )
```

The remaining descriptions prepare the local recursion equations. `towerAt` supplies candidate rows of encoded environments, `Tags` calibrates the ten constructor-tag slots, and `tableAt` combines propositional totality on the candidate key set, restriction of table entries to that set, and ten local extensional equations. These ingredients still describe only a candidate relation. `PinnedRecursion` proves the conditional uniqueness needed at a genuine formula key, while `SatisfactionBridge` independently interprets membership in the external value `Sat` as satisfaction in the restricted structure. `UniformSatisfaction` then combines existence with pinned uniqueness on `AllCodes B` to obtain a uniform table.

```agda
open import L.Coding.EnvironmentTower {ℓ} lem using ( nn; towerAt )
open import L.Coding.CodeDomain {ℓ} using ( Tags )
open import L.Coding.SatisfactionClauses {ℓ} using ( tableAt )
open import Cubical.Data.Nat using ( _+_ )
open import Cubical.Data.FinData using ( toℕ )
```

An interpretation environment for a formula with `n` free positions is a vector of `n` carrier elements. `lookup` reads the element assigned to a position, while cons extends an environment at its innermost end. This fixed convention will let fourteen auxiliary witnesses be placed in front of an arbitrary outer environment without losing the original query positions.

```agda
open import Cubical.Data.Vec using ( _∷_; []; lookup )
```

Object-language existence is interpreted by propositional truncation. Thus a proof of an existential formula records that a witness exists while forgetting which witness was used. This is essential for the satisfaction graph: the public reading may establish that suitable tags, a tower, a key set, and a table exist, but it does not expose data from which a caller could choose one candidate table globally.

```agda
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
```

From now on `S` is the carrier of the constructible structure: an element consists of a hierarchy set together with evidence of constructibility. Relations in this structure have proposition-valued truth values, and brackets expose the underlying proposition whose inhabitants are proofs. Equality or membership of the underlying hierarchy sets must therefore remain distinct from an object-language formula that asserts equality or membership.

```agda
open hPropStructure 𝒮ʟ
```

The judgment `γ ⊨ φ` now means that the object-language formula `φ` holds under the constructible environment `γ`. It connects the finite vector of semantic values to the syntax of the formula. In particular, the outer environment used to ask about a key and a proposed value is a metatheoretic assignment; it is not one of the encoded environment sets arranged in the tower.

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

## The guarded recursion frame

The first four names describe the structural core of the fourteen new positions. From the innermost position outward they hold the carrier `b`, the candidate satisfaction table `T`, its candidate key set `C`, and the candidate environment tower `E`. Keeping these roles separate prevents two tempting confusions: elements of `C` are formula keys, whereas elements of `T` encode key-value pairs, and the rows represented through `E` organize encoded environments by arity.

```agda
Bi Ti Ci Ei : ∀ {n} → Fin (14 + n)
Bi = i0
Ti = i1
Ci = i2
Ei = i3
```

The next ten positions are constructor tags. `NN` begins their common address map by sending constructor indices zero through three to positions `i4` through `i7`. Before calibration these positions may contain arbitrary carrier elements, so the local clauses merely use them as parameters identifying code shapes.

```agda
NN : ∀ {n} → Fin 10 → Fin (14 + n)
NN zero = i4
NN (suc zero) = i5
NN (suc (suc zero)) = i6
NN (suc (suc (suc zero))) = i7
```

The same map continues consecutively through constructor eight. This uniform indexing matters because closure and the ten table equations must agree on which numeral marks each formula constructor. Once that agreement is fixed, one family of clauses can cover atoms, the three binary connectives, falsity, the two unbounded quantifiers, and the two bounded quantifiers.

```agda
NN (suc (suc (suc (suc zero)))) = i8
NN (suc (suc (suc (suc (suc zero))))) = i9
NN (suc (suc (suc (suc (suc (suc zero)))))) = i10
NN (suc (suc (suc (suc (suc (suc (suc zero))))))) = i11
NN (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = i12
```

The last equation places constructor nine at `i13`, completing the layout
`b, T, C, E, N0, ..., N9` from the innermost position outward. The environment tower occupies one position as the candidate set `E`; its arity-indexed rows are encoded entries described by `towerAt`, rather than ten further positions in this vector.

```agda
NN (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = i13
```

The query key and proposed value remain in the caller's environment outside these fourteen positions. The shift `sh14` moves either original position across all fourteen binders, so a later occurrence such as `appAt Ti (sh14 x) (sh14 y)` still asks whether the original pair `(x,y)` is recorded in `T`.

```agda
sh14 : ∀ {n} → Fin n → Fin (14 + n)
sh14 i = sh 14 i
```

The function `ev` is the semantic realization of this position map. It places `b`, `T`, `C`, `E`, and the ten values supplied by `ν` in front of the outer environment `γ`. Consequently every named slot used by `Tags`, `towerAt`, `closedAt`, `domAt`, and `tableAt` refers to the same witness throughout the argument.

```agda
ev : ∀ {n} → (Fin 10 → S) → S → S → S → S → S ^ n → S ^ (14 + n)
ev ν E C T b γ =
  b ∷ T ∷ C ∷ E ∷ ν f0 ∷ ν f1 ∷ ν f2 ∷ ν f3 ∷ ν f4 ∷ ν f5
    ∷ ν f6 ∷ ν f7 ∷ ν f8 ∷ ν f9 ∷ γ
```

For the canonical tag assignment, constructor index `k` is sent to the model numeral `nn (toℕ k)`. Its underlying hierarchy set is the finite ordinal representing `k`, while its second component certifies constructibility. Packaging the numeral as an element of `S` lets the object language name it by a constant.

```agda
numν : Fin 10 → S
numν k = nn (toℕ k)
```

`Tags γ NN` asks, for every constructor index `k`, whether the underlying set at position `NN k` is the numeral for `k`. In the environment built from `numν`, the first four cases hold by reflexivity because lookup and first projection compute to that numeral. The statement compares underlying sets, so it does not require the constructibility certificates themselves to be definitionally equal.

```agda
numTags : ∀ {n} (E C T b : S) (γ : S ^ n) → Tags (ev numν E C T b γ) NN
numTags E C T b γ zero = refl
numTags E C T b γ (suc zero) = refl
numTags E C T b γ (suc (suc zero)) = refl
numTags E C T b γ (suc (suc (suc zero))) = refl
```

Reflexivity also proves the cases for indices four through eight. The longer successor patterns carry only the finite-index bookkeeping: `NN k` selects the slot occupied by `numν k`, whose first projection is the required numeral. Thus the proof remains pointwise and introduces no constructor-specific semantic assumption.

```agda
numTags E C T b γ (suc (suc (suc (suc zero)))) = refl
numTags E C T b γ (suc (suc (suc (suc (suc zero))))) = refl
numTags E C T b γ (suc (suc (suc (suc (suc (suc zero)))))) = refl
numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc zero))))))) = refl
numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = refl
```

Index nine exhausts `Fin 10`, so the same reflexivity argument completes a total proof of `Tags` for the canonical assignment. Other assignments may still serve as candidate witnesses, but they must carry their own proof of this pointwise agreement before the ten constructor clauses acquire the intended tags.

```agda
numTags E C T b γ (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = refl
```

The object-language formula `numsAt` begins the same calibration as a right-associated conjunction of equations. Its first eight equations say that the values at positions `i4` through `i11` are the constants `nn 0` through `nn 7`. Thus the later variable-carrier form of the graph avoids naming the carrier as a constant, but the graph formula still names these fixed standard numerals.

```agda
numsAt : ∀ {n} → Formula S (14 + n)
numsAt =
  (var i4 ≐ con (nn 0)) ∧̇ ((var i5 ≐ con (nn 1)) ∧̇ ((var i6 ≐ con (nn 2)) ∧̇
  ((var i7 ≐ con (nn 3)) ∧̇ ((var i8 ≐ con (nn 4)) ∧̇ ((var i9 ≐ con (nn 5)) ∧̇
  ((var i10 ≐ con (nn 6)) ∧̇ ((var i11 ≐ con (nn 7)) ∧̇
```

The equations for `i12` and `i13` finish the calibration with numerals eight and nine. Satisfaction of the complete conjunction therefore carries exactly the ten equations required by `Tags`; the following read lemma extracts those equations from the nested conjunction. This calibration identifies constructor tags only and adds no claim that the candidate key set is the complete set of well-formed formula codes.

```agda
  ((var i12 ≐ con (nn 8)) ∧̇ (var i13 ≐ con (nn 9))))))))))
```

`nums-out` turns satisfaction of `numsAt` into the host-level family `Tags`. Since conjunction is interpreted as a pair, the case for tag zero takes the first projection, and the cases for tags one and two follow the second projection before taking the next first projection. The lemma works for an arbitrary tag assignment `ν`, so it can decode the calibration carried by any candidate graph witness.

```agda
nums-out : ∀ {n} (ν : Fin 10 → S) (E C T b : S) (γ : S ^ n)
         → ⟨ ev ν E C T b γ ⊨ numsAt ⟩ → Tags (ev ν E C T b γ) NN
nums-out ν E C T b γ h zero = h .fst
nums-out ν E C T b γ h (suc zero) = h .snd .fst
nums-out ν E C T b γ h (suc (suc zero)) = h .snd .snd .fst
```

For every higher index, `nums-out` follows the second projection of the right-associated product until it reaches the corresponding equality. This is only elimination of conjunction: it neither chooses tag values nor proves them unique. When the fourteen existential witnesses are later eliminated under propositional truncation, these projections recover the tag certificate already present in the formula's satisfaction.

```agda
nums-out ν E C T b γ h (suc (suc (suc zero))) = h .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc zero)))) = h .snd .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc (suc zero))))) = h .snd .snd .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc zero)))))) = h .snd .snd .snd .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc zero))))))) = h .snd .snd .snd .snd .snd .snd .snd .fst
```

The deepest component of the right-associated conjunction is the pair of equations for tags eight and nine. Its two projections complete the pointwise family, so satisfaction of `numsAt` yields agreement at every index of `Fin 10` at once. This step only repackages the ten equations; it adds no condition on the candidate key set or table.

```agda
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = h .snd .snd .snd .snd .snd .snd .snd .snd .fst
nums-out ν E C T b γ h (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = h .snd .snd .snd .snd .snd .snd .snd .snd .snd
```

The converse reading `nums-in` starts from `Tags`: for each constructor index, the chosen tag has the same underlying set as the corresponding standard numeral. Placing these ten equalities into the right-associated conjunction proves `numsAt`. Together, `nums-out` and `nums-in` let the rest of the chapter move in either direction between the object-language calibration and its host-level family of equalities.

```agda
nums-in : ∀ {n} (ν : Fin 10 → S) (E C T b : S) (γ : S ^ n)
        → Tags (ev ν E C T b γ) NN → ⟨ ev ν E C T b γ ⊨ numsAt ⟩
nums-in ν E C T b γ tg =
    tg f0 , (tg f1 , (tg f2 , (tg f3 , (tg f4 , (tg f5
  , (tg f6 , (tg f7 , (tg f8 , tg f9))))))))
```

The auxiliary family `satGraphOn` now assembles the complete frame. Its parameter `pin` is a formula over the extended environment and specifies only how the newly bound carrier is related to an outer reference; the query positions `x` and `y` remain in the outer environment. Fourteen nested existentials bind the ten tags, the tower, the key set, the table, and finally the innermost carrier. Their first conjunct is `pin`, so changing the carrier policy leaves every other condition of the candidate graph unchanged.

```agda
private
  satGraphOn : ∀ {n} → Formula S (14 + n)
             → Fin n → Fin n → Formula S n
  satGraphOn pin x y =
    ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (( pin
```

After the pin, the conjunction records the conditions needed to interpret one table entry. The calibration `numsAt` identifies the ten tag slots with the standard numerals. The clause `towerAt Ei Bi (NN f0)` requires the candidate tower to have the row structure used by the recursive clauses over the bound carrier; it does not assert that the tower is canonical. The clause `closedAt Ci` closes the candidate key set under the seven possible immediate subformula keys. Next, `domAt Ti Ci` says that the key domain of the table is exactly `C`, while `appAt Ti (sh14 x) (sh14 y)` says that the original query pair is an entry after `x` and `y` have been shifted past all fourteen binders.

```agda
      ∧̇ ( numsAt
      ∧̇ ( towerAt Ei Bi (NN f0)
      ∧̇ ( closedAt Ci
      ∧̇ ( domAt Ti Ci
      ∧̇ ( appAt Ti (sh14 x) (sh14 y)
```

The final conjunct `tableAt Ti Bi Ci Ei NN` supplies the local recursion specification. Its first domain condition gives, under propositional truncation, some value for every key in `C`; its second says that every member of `T` can be decomposed, again under truncation, as a key from `C` paired with a value. The remaining ten clauses characterize matching entries by extensional equations, one for each formula constructor. These conditions describe a candidate relation locally. They neither make `T` single-valued nor choose a value for each key. Uniqueness at a genuine formula key is proved later by structural induction in `PinnedRecursion`.

```agda
      ∧̇ tableAt Ti Bi Ci Ei NN ))))))))))))))))))))
```

## Witnesses for the satisfaction graph

The host-level type `GraphWitOn` flattens the same information into five pieces of data, `ν`, `E`, `C`, `T`, and `b`, followed by seven certificates. They assert equality of the underlying sets of `b` and the reference `W`, agreement of all ten tags, satisfaction of the tower, closure, and exact-domain clauses at the assembled environment, membership of the query pair in the underlying table, and satisfaction of `tableAt`. The two domain certificates have different later uses: `domAt` lets a consumer infer that a queried key lies in `C`, whereas the totality component inside `tableAt` supplies values for subkeys during structural induction. Public readings expose this concrete record only through propositional truncation, so they establish existence without selecting a particular candidate table.

```agda
private
  GraphWitOn : ∀ {n} → S → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ)
  GraphWitOn W x y γ =
    Σ[ ν ∈ (Fin 10 → S) ] (Σ[ E ∈ S ] (Σ[ C ∈ S ] (Σ[ T ∈ S ] (Σ[ b ∈ S ] ((fst b ≡ fst W) × (Tags (ev ν E C T b γ) NN × (⟨ (ev ν E C T b γ) ⊨ towerAt Ei Bi (NN f0) ⟩ × (⟨ (ev ν E C T b γ) ⊨ closedAt Ci ⟩ × (⟨ (ev ν E C T b γ) ⊨ domAt Ti Ci ⟩ × (⟨ pr (fst (lookup x γ)) (fst (lookup y γ)) ∈ fst T ⟩ × ⟨ (ev ν E C T b γ) ⊨ tableAt Ti Bi Ci Ei NN ⟩))))))))))
```

To compare satisfaction of `satGraphOn` with the flat record, fix the pin, its reference `W`, the query positions, and the outer environment. Every field of the record except the carrier equation already has a fixed interpretation among the frame's conjuncts. The only extra hypothesis is therefore a reading `rd` for the pin. The inward implication turns an equality `fst b ≡ fst W` into satisfaction of `pin`; the outward implication reads satisfaction of `pin` back as that equality.

```agda
  module _ {n : ℕ} (pin : Formula S (14 + n)) (W : S)
           (x y : Fin n) (γ : S ^ n) where
```

The inward reading turns a truncated witness record into satisfaction of the
whole frame. Its hypothesis `rd` says how the pin is to be read: for
any choice of the ten tag values, the tower, the index set, the table and the
carrier, if the carrier agrees with the reference, then the pin is satisfied
at the assembled environment. The input is a truncation and the output is a
satisfaction, itself a truncation, so the whole proof is a map inside
truncations: it sends the flat record, matched component by component, to the
fourteen-level witness the formula demands. No witness is selected anywhere;
a map between truncations transports only the fact that witnesses exist.

```agda
    graphOn-in : ((ν : Fin 10 → S) (E C T b : S) → fst b ≡ fst W
                   → ⟨ ev ν E C T b γ ⊨ pin ⟩)
               → ∥ GraphWitOn W x y γ ∥₁ → ⟨ γ ⊨ satGraphOn pin x y ⟩
    graphOn-in rd = PT.map
      (λ { (ν , (E , (C , (T , (b , (eb , (tg , (hE , (hc , (hd , (ha , h12))))))))))) →
```

The flat record is re-nested in the reverse of the layout order. The outermost existential receives the tag of the ninth constructor, the next one the eighth, and so on, until the innermost existential receives the carrier; this is exactly the de Bruijn order of the layout, read from the outside in. The pin's satisfaction is supplied by `rd`, applied to the assembled witnesses and to the carrier equation the record carries. The calibration is converted by `nums-in` from the host-level agreement into satisfaction of the ten equations, so that every later conjunct meets standard numerals.

```agda
          ν f9
        , ∣ ν f8 , ∣ ν f7 , ∣ ν f6 , ∣ ν f5 , ∣ ν f4
        , ∣ ν f3 , ∣ ν f2 , ∣ ν f1 , ∣ ν f0 , ∣ E , ∣ C , ∣ T , ∣ b
        , ( rd ν E C T b eb
          , ( nums-in ν E C T b γ tg
```

The three guard certificates pass through unchanged: they are satisfactions
of formulas read at the very environment the frame assembles, so they can
stand where the conjuncts stand. The query entry is the one component that
must change languages. On the host side it is an ordinary membership: the
ordered pair of the two query values belongs to the underlying set of the
table. The adequacy law of the application atom identifies satisfaction of
the atom with exactly this membership, and the proof transports along that
one path. This is the single substantial bridge of the inward direction;
everything else is re-packing.

```agda
          , ( hE
          , ( hc
          , ( hd
          , ( subst ⟨_⟩
                (sym (appAt-adequate Ti (sh14 x) (sh14 y) (ev ν E C T b γ))) ha
```

After the clause-family certificate has been placed in the last conjunct, the only remaining work is to restore the nested truncations. The call to `PT.map` supplies the outermost truncation: its mapping function returns the witness pair for the outermost existential. Inside that pair, the thirteen explicit insertions supply the remaining existential layers down to the carrier. Thus the construction turns the truncated flat record into satisfaction of all fourteen nested existentials without exposing any of its chosen data outside a truncation.

```agda
            , h12 ))))))
          ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ })
```

The outward reading reverses the journey, and its hypothesis `rd` now
runs the pin the other way: from a satisfaction of the pin at an assembled
environment, it recovers the carrier equation. The input is a satisfaction of
the whole frame, whose fourteen existentials are all truncated, and the
output is the truncated witness record. The proof eliminates the existentials
one level at a time, and every elimination targets the truncation of the
record, a proposition, so each one is legitimate: the lemma never claims to
produce the record itself, only the fact that one exists.

```agda
    graphOn-out : ((ν : Fin 10 → S) (E C T b : S)
                    → ⟨ ev ν E C T b γ ⊨ pin ⟩ → fst b ≡ fst W)
                → ⟨ γ ⊨ satGraphOn pin x y ⟩ → ∥ GraphWitOn W x y γ ∥₁
    graphOn-out rd h = PT.rec squash₁ (λ { (n9 , h9) →
      PT.rec squash₁ (λ { (n8 , h8) →
```

Each application of `PT.rec` removes one truncated tag witness while keeping the same propositional target `∥ GraphWitOn W x y γ ∥₁`. The values recovered for slots nine through three may therefore be passed to the next continuation, but none can escape into untruncated data. Repeating this one legitimate elimination is what makes the nested object-language existentials compatible with one flat truncated record.

```agda
      PT.rec squash₁ (λ { (n7 , h7) →
      PT.rec squash₁ (λ { (n6 , h6) →
      PT.rec squash₁ (λ { (n5 , h5) →
      PT.rec squash₁ (λ { (n4 , h4) →
      PT.rec squash₁ (λ { (n3 , h3) →
```

Once all ten tag values have been recovered, the same propositional elimination reaches the candidate tower `E` and key set `C`. The names `hE'` and `hC'` denote the truncated tails that still contain the table, carrier, and certificates; they are not proofs of the tower or closure conditions. Those proofs remain inside the final conjunction and will enter the record only after `T` and `b` have also been exposed within the truncation.

```agda
      PT.rec squash₁ (λ { (n2 , h2) →
      PT.rec squash₁ (λ { (n1 , h1) →
      PT.rec squash₁ (λ { (n0 , h0) →
      PT.rec squash₁ (λ { (E , hE') →
      PT.rec squash₁ (λ { (C , hC') →
```

At the innermost level the proof maps rather than eliminates further. What
remains is a truncation whose content is the carrier record, and a map sends
it, component by component, into the truncated flat witness. The tag function
is rebuilt from the ten named slots by a small function defined below the
readings, and `rd`, applied to the rebuilt function, the three
structural witnesses, the carrier and the pin's satisfaction, delivers the
carrier equation that heads the record. Every operation here stays inside
truncations: the map transports the fact that a record exists, and constructs
the corresponding fact on the other side.

```agda
      PT.rec squash₁ (λ { (T , hT') →
      PT.map (λ { (b , (hpin , (hnum , (hE , (hc , (hd , (ha , h12))))))) →
        let ν : Fin 10 → S
            ν = ν' n0 n1 n2 n3 n4 n5 n6 n7 n8 n9
        in ν , (E , (C , (T , (b , (rd ν E C T b hpin
```

The remaining fields are recovered in the directions required by the flat record. The calibration conjunct is read by `nums-out` as the host-level `Tags` family. The tower, closure, and exact-domain satisfactions already have the required types and are retained unchanged. Satisfaction of the query atom is the one field that crosses back to an ordinary membership: transport along `appAt-adequate` turns it into membership of the ordered query pair in the underlying set of `T`.

```agda
           , ( nums-out ν E C T b γ hnum
           , ( hE
           , ( hc
           , ( hd
           , ( subst ⟨_⟩
```

Satisfaction of `tableAt` supplies the last certificate of the record. Applying the accumulated continuations then discharges the nested eliminations and yields an element of `∥ GraphWitOn W x y γ ∥₁`. Together, the two readings show that frame satisfaction and the truncated existence of a qualified flat record imply one another. This is a pair of implications between propositions, not a procedure for choosing a canonical table, and it contains no uniqueness claim for table values.

```agda
                 (appAt-adequate Ti (sh14 x) (sh14 y) (ev ν E C T b γ)) ha
             , h12 )))))))))) })
        hT' }) hC' }) hE' }) h0 }) h1 }) h2 }) h3 }) h4 }) h5 }) h6 })
        h7 }) h8 }) h9 }) h
      where
```

The existential formula presents the ten tags as ten separate bound values, whereas `GraphWitOn` expects one function `Fin 10 → S`. The local function `ν'` reconciles these presentations by case analysis on the constructor index. Its first four branches return `a0` through `a3`; no semantic fact is used here, only the fixed correspondence between indices and the slots already recovered from the formula.

```agda
      ν' : S → S → S → S → S → S → S → S → S → S → Fin 10 → S
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 zero = a0
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc zero) = a1
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc zero)) = a2
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc zero))) = a3
```

For constructor indices four through eight, the same case analysis returns the correspondingly named values `a4` through `a8`. Because these branches follow the indexing map `NN`, the equalities extracted by `nums-out` apply to the reconstructed function at precisely the slots where the table and closure clauses expect those tags.

```agda
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc zero)))) = a4
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc zero))))) = a5
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc zero)))))) = a6
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc zero))))))) = a7
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc (suc zero)))))))) = a8
```

The case at index nine exhausts `Fin 10` and makes `ν'` a total function. Thus the fourteen separate object-language witnesses are represented in the host record by exactly one ten-entry tag function together with `E`, `C`, `T`, and `b`. This is only a change of presentation: it creates no new tag and discards none of the existential data.

```agda
      ν' a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 (suc (suc (suc (suc (suc (suc (suc (suc (suc zero))))))))) = a9
```

## The carrier supplied by a variable

The variable-carrier witness type chooses its reference from the ambient environment. In `GraphWitAt B x y γ`, the internal carrier `b` is required to have the same underlying set as `lookup B γ`; the proof does not identify the packaged elements themselves. Because the reference is obtained by lookup, the same witness type remains meaningful when later formulas add binders around the graph and shift the carrier slot accordingly.

```agda
GraphWitAt : ∀ {n} → Fin n → Fin n → Fin n → S ^ n → Type (ℓ-suc ℓ)
GraphWitAt B x y γ = GraphWitOn (lookup B γ) x y γ
```

The formula `satGraphAt B x y` implements this reference by using the pin `var Bi ≐ var (sh14 B)`: the newly bound carrier slot is equated with the original carrier slot after that slot has been shifted past all fourteen internal binders. This instance therefore does not insert the carrier as a constant, although the ten standard numeral constants in `numsAt` remain. The formula is opaque so that larger descriptions can use it as one relation; its witness readings provide the public way to establish or consume its satisfaction.

```agda
opaque
  satGraphAt : ∀ {n} → Fin n → Fin n → Fin n → Formula S n
  satGraphAt B x y = satGraphOn (var Bi ≐ var (sh14 B)) x y
```

The body of `satGraphAt` is unfolded only while its two witness implications are established. Inside this scope the proof may compare the large formula with `GraphWitAt` field by field. Outside it, later mathematics uses the exact statements of `graphAt-in` and `graphAt-out`, so the fourteen binders remain an internal presentation of the same relation.

```agda
opaque
  unfolding satGraphAt
```

For the inward reading, the pin hypothesis is the identity: satisfaction of the variable equality is exactly the underlying-set equality already stored in `GraphWitAt`. Hence a truncated witness record at any ambient environment gives satisfaction of `satGraphAt` there. This flexibility is used concretely in `DefAt`, where `DefBody` places the graph below the element slot and two adjacent existentials, and in `DenoteBody`, where the graph reaches the same carrier through five added slots. In both cases the carrier stays in the caller's environment rather than being substituted into the graph as a constant.

```agda
  graphAt-in : ∀ {n} (B x y : Fin n) (γ : S ^ n)
             → ∥ GraphWitAt B x y γ ∥₁ → ⟨ γ ⊨ satGraphAt B x y ⟩
  graphAt-in B x y γ =
    graphOn-in (var Bi ≐ var (sh14 B)) (lookup B γ) x y γ (λ _ _ _ _ _ e → e)
```

The outward reading completes the variable-carrier interface. From a proof of
`satGraphAt B x y`, it recovers, under propositional truncation, the
same candidate data and certificates recorded by `GraphWitAt B x y γ`.
In particular, the internally bound carrier agrees on underlying sets with
the value of the outer slot `B`, while the queried key and value are
still read from the outer slots `x` and `y`. The identity passed
to `graphOn-out` reflects exactly this variable-to-variable pin. A
consumer may eliminate the resulting truncation when proving a proposition,
as the later uniqueness arguments do, but it cannot retain a chosen tower,
closed key set, or table.

```agda
  graphAt-out : ∀ {n} (B x y : Fin n) (γ : S ^ n)
              → ⟨ γ ⊨ satGraphAt B x y ⟩ → ∥ GraphWitAt B x y γ ∥₁
  graphAt-out B x y γ =
    graphOn-out (var Bi ≐ var (sh14 B)) (lookup B γ) x y γ (λ _ _ _ _ _ h → h)
```

## The carrier fixed as a constant

When the carrier is already available as an element `B`, the second
instance uses the constant `B` instead of referring to an outer carrier
slot. It has exactly two free positions: `suc zero` is the input key and
`zero` is the proposed output value. The rest of the frame is unchanged,
so the formula still says merely that some locally suitable candidate package
records this query. In particular, `SatisfactionClauses` supplies totality and
domain restriction for the candidate table together with its ten local
equations; neither those clauses nor this instance by itself makes the graph
single-valued.

```agda
opaque
  satGraph : S → Formula S 2
  satGraph B = satGraphOn (var Bi ≐ con B) (suc zero) zero
```

The witness type makes the direction of this binary relation explicit. In the
environment `y ∷ x ∷ []`, the innermost position contains `y`
and the next contains `x`; hence `GraphWit B x y` says that the
candidate table contains the encoded pair with key `x` and value
`y`. Its reference carrier is the fixed element `B`. The record
also contains calibrated tags, a candidate environment tower, a subcode-closed
candidate key set, a table whose key domain is exactly that set, and the
certificates required by `tableAt`. The key set is only locally closed;
this definition does not identify it with the set of all genuine formula keys.

```agda
GraphWit : (B x y : S) → Type (ℓ-suc ℓ)
GraphWit B x y = GraphWitOn B (suc zero) zero (y ∷ x ∷ [])
```

The constant pin admits the same two witness implications, proved by unfolding `satGraph` only in this scope. They turn the large existential formula into a stable binary relation: `graph-in` establishes the relation from a propositionally truncated candidate record, and `graph-out` recovers exactly such a truncation from the relation. This is the form in which `UniformSatisfaction` can use `satGraph B` as the graph parameter of abstract recursion.

```agda
opaque
  unfolding satGraph
```

The inward reading applies the general conversion with the constant pin. A
record begins with an equality between the underlying sets of its bound
carrier and `B`; satisfaction of the object-language equation
`var Bi ≐ con B` has exactly that content, so the pin reader is the
identity. The remaining fields already certify the tag calibration, tower and
closure conditions, exact key domain, queried table entry, and packaged table
conditions. Mapping this record through `graphOn-in` preserves its
propositional truncation: it proves that a suitable package exists, without
choosing one for later use.

```agda
  graph-in : (B x y : S) → ∥ GraphWit B x y ∥₁ → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩
  graph-in B x y =
    graphOn-in (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ _ _ e → e)
```

The outward reading reverses this conversion and completes the chapter: a
satisfaction of the binary formula yields only the propositional truncation of
a candidate record with the queried entry. This is the exact limit of the
satisfaction graph formula. `PinnedRecursion` subsequently proves, by
structural recursion on a genuine formula, that if its key lies in the
candidate key set and the candidate table records a value there, then that
value has the same underlying set as the externally defined value
`Sat`. `SatisfactionBridge` separately gives that value its semantics
by relating membership in it to satisfaction in the restricted structure.
Finally, `UniformSatisfaction` uses `satGraph B` on the genuine domain
`AllCodes B`; existence together with the pinned uniqueness there
allows the abstract recursion theorem to assemble one uniform table. The
present two readings supply the represented relation on which those later
arguments operate, but do not themselves choose, prove unique, or semantically
interpret a table.

```agda
  graph-out : (B x y : S) → ⟨ (y ∷ x ∷ []) ⊨ satGraph B ⟩ → ∥ GraphWit B x y ∥₁
  graph-out B x y =
    graphOn-out (var Bi ≐ con B) B (suc zero) zero (y ∷ x ∷ []) (λ _ _ _ _ _ h → h)
```