---
layout: default
file: "src/FLRP/Certificates.lagda.md"
title: "FLRP.Certificates module (The Agda Universal Algebra Library)"
date: "2026-07-22"
author: "the agda-algebras development team"
---

### Machine-checked representation certificates

This is the [FLRP.Certificates][] module of the [Agda Universal Algebra Library][].

The FLRP program's computational campaigns[^1] produce claims of the form "`Con š‘Ø ā‰…
š‘³` for this finite algebra `š‘Ø` and this finite lattice `š‘³`" from external engines ā€”
GAP, UACalc, SAT and model finders.

Per the certificate discipline of [the roadmap](docs/notes/flrp-research-roadmap.md)
Ā§ 6 and [the WP-6 design note](docs/notes/flrp-wp6-freese-certificates.md), nothing
enters the corpus on the authority of an external tool: the engine emits a
whole-lattice certificate (normal-form parent vectors, Freese traces, and pointer
tables ā€” [Setoid.Congruences.Certificates.Schema][]), the generic checkers verify it
with no search and no `Cg-dec`{.AgdaFunction}
([Setoid.Congruences.Certificates.Congruence][],
[Setoid.Congruences.Certificates.Lattice][]), and *this* module turns the
checked certificate into the FLRP-facing theorem: a
`Representableįµˆ`{.AgdaRecord} witness ([FLRP.Representable][]) for the target
lattice.

Concretely, we are given

+  a finite finitary algebra (`š‘­`, `š‘ŗ`, everything at level `0ā„“`, as
   `ConIsoįµˆ`{.AgdaFunction} demands),
+  a target `FiniteLattice`{.AgdaRecord} `š‘³` ([FLRP.Problem][]), and
+  a whole-lattice certificate `lc` whose entry list is indexed by `š‘³`'s carrier.

Then two checked hypotheses produce the order isomorphism; the hypotheses are
as follows:

+  `LatticeCertOK lc`{.AgdaRecord} ā€” the whole-lattice checker's bundle
   (decided by one `latticeCertOK?`{.AgdaFunction});
+  `MeetMatches lc`{.AgdaFunction} ā€” the certificate's meet table is
   *syntactically* the target lattice's `āˆ§`{.AgdaFunction} table (decided by
   `meetMatches?`{.AgdaFunction}).

The isomorphism's two maps are the whole-lattice checker's completeness fold
`indexOf`{.AgdaFunction} (which executes only the given congruence's own decision
procedure and table lookups) and the certificate's entry decoder
`entryDec`{.AgdaFunction}; the four order-isomorphism laws are exactly the exported
fold lemmas, with the meet-table match translating containment of entries into the
lattice's meet order `x ā‰¤ y := x āˆ§ y ā‰ˆ x` ([Classical.Properties.Lattice][]).

Since `toLattice`{.AgdaFunction} builds its carrier setoid on propositional equality,
the translation is definitional.

This is problem-specific wiring; all reusable mathematics lives under the `Setoid`
tree; in this case, under `Setoid.Congruences.Certificates`.

<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

module FLRP.Certificates where

open import Agda.Primitive using () renaming ( Set to Type )

-- Imports from the Agda Standard Library -----------------------------------
open import Data.Fin.Base                          using  ( Fin )
open import Data.Fin.Properties                    using  ( all? )
                                                   renaming ( _ā‰Ÿ_ to _ā‰Ÿį¶ _ )
open import Data.Nat.Base                          using  ( suc )
open import Data.Product                           using  ( projā‚ )
open import Level                                  using  ( 0ā„“ )
open import Relation.Binary.PropositionalEquality  using  ( _ā‰”_ ; sym ; trans )
open import Relation.Nullary.Decidable             using  ( Dec )

-- Imports from the Agda Universal Algebra Library ----------------------------
open import FLRP.Problem                                using  ( FiniteLattice
                                                               ; toLattice )
open import FLRP.Representable                          using  ( Representableįµˆ ; ConIsoįµˆ )
open import Overture                                    using  ( Signature )
open import Setoid.Algebras.Basic                       using  ( Algebra )
open import Setoid.Algebras.Finite                      using  ( FiniteAlgebra )
open import Setoid.Congruences.Finite.Basic             using  ( DecCon )
open import Setoid.Congruences.Lattice                  using  ( ā‰‘-sym )
open import Setoid.Congruences.Certificates.Schema      using  ( LatticeCert )
open import Setoid.Congruences.Certificates.Congruence  using  ( module CertCheck )
open import Setoid.Congruences.Certificates.Lattice     using  ( module LatticeCheck )
open import Setoid.Signatures.Finite                    using  ( FiniteSignature )
```
-->

#### The certified order isomorphism

Fix the finite finitary algebra, the target finite lattice, and a certificate
whose entry list is indexed by the lattice's carrier `Fin (suc size)`.

```agda
module _ {š‘† : Signature 0ā„“ 0ā„“} {š‘Ø : Algebra {š‘† = š‘†} 0ā„“ 0ā„“}
         (š‘­ : FiniteAlgebra š‘Ø) (š‘ŗ : FiniteSignature š‘†) (š‘³ : FiniteLattice)
  where

  open FiniteAlgebra š‘­ using ( card )
  open FiniteSignature š‘ŗ using ( opCard )
  open CertCheck š‘­ š‘ŗ using ( arOf )
  open LatticeCheck š‘­ š‘ŗ
  open FiniteLattice š‘³ using ( size ; _āˆ§_ )

  module _ (lc : LatticeCert card opCard arOf (suc size)) where
    open LatticeCert lc using ( meet )
```

The meet-table match: the certificate's meet table *is* the target lattice's
`āˆ§`{.AgdaFunction} table.  This is what pins the certificate's entry indexing
to the intended lattice, and it is decided by an `m Ā²` sweep of
`Fin`{.AgdaDatatype} comparisons.

```agda
    -- The certificate's meet table is the target lattice's āˆ§ table.
    MeetMatches : Type
    MeetMatches = āˆ€ k l ā†’ meet k l ā‰” k āˆ§ l

    meetMatches? : Dec MeetMatches
    meetMatches? = all? (Ī» k ā†’ all? (Ī» l ā†’ meet k l ā‰Ÿį¶  k āˆ§ l))
```

Given the two checked hypotheses, the order isomorphism between the decidable
congruences of `š‘Ø` and the meet order of the target lattice.  The maps and all
four laws are the whole-lattice checker's exports; only the two monotonicity
clauses do any translation, moving between containment of entries and
meet-table idempotence through `MeetMatches`{.AgdaFunction} ā€” definitionally,
because the classical lattice's carrier equality is propositional.

```agda
    module _ (OK : LatticeCertOK lc) (mm : MeetMatches) where

      private
        -- the two maps of the isomorphism
        toIdx : DecCon š‘Ø 0ā„“ ā†’ Fin (suc size)
        toIdx = indexOf lc OK

        fromIdx : Fin (suc size) ā†’ DecCon š‘Ø 0ā„“
        fromIdx = entryDec lc OK

      -- The certified order isomorphism Con(š‘Ø) ā‰… š‘³, at Layer D.
      certConIsoįµˆ : ConIsoįµˆ š‘Ø (toLattice š‘³)
      certConIsoįµˆ = record
        { to         = toIdx
        ; from       = fromIdx
        ; to-mono    = Ī» {d} {e} dāŠ†e ā†’
            trans (sym (mm (toIdx d) (toIdx e)))
                  (āŠ†ā†’meetIdem lc OK (toIdx d) (toIdx e)
                    (fold-mono lc OK d e dāŠ†e))
        ; from-mono  = Ī» {u} {v} uā‰¤v ā†’
            meetIdemā†’āŠ† lc OK u v (trans (mm u v) uā‰¤v)
        ; toāˆ˜from    = fold-entry lc OK
        ; fromāˆ˜to    = Ī» d ā†’
            ā‰‘-sym {Īø = projā‚ d} {Ļ† = projā‚ (fromIdx (toIdx d))}
                  (dā‰‘fold lc OK d)
        }
```

#### The certified representability witness

Packaging the finite finitary data with the certified isomorphism gives the
headline: the target lattice is decidably representable ā€” a machine-checked
representation, on no authority but the checker's.

```agda
      -- The certificate's Representableįµˆ witness for the target lattice.
      certRepresentableįµˆ : Representableįµˆ (toLattice š‘³)
      certRepresentableįµˆ = record
        { sigįµˆ      = š‘†
        ; algįµˆ      = š‘Ø
        ; finiteįµˆ   = š‘­
        ; finsigįµˆ   = š‘ŗ
        ; con-isoįµˆ  = certConIsoįµˆ
        }
```

--------------------------------------


[^1]: See [the roadmap](docs/notes/flrp-research-roadmap.md) Ā§ 5, Avenue A.