GV112 assurance

GV112 is established by a generic total-disposition construction plus the first real declared recovery corpus. A concrete corpus chooses a finite observation type, binds it to immutable source provenance, and can enter the project-wide registry only together with a total Observation → Disposition closure.

This proves complete treatment of the declared observation set. It deliberately does not claim that the compiler can prove perfect extraction from natural language or inspect hidden model memory.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV112 where

open import Agda.Builtin.Equality using (_≡_; refl)
open import Govenv.Consolidation.Baseline20260923 using
  (Observation; declared; closure)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Consolidation using
  (Corpus; Consolidation)
open import Govenv.Roadmap using (roadmap)

record Proposition : Set where
  constructor satisfied
  field
    recoveryCorpusIdIsStable :
      Corpus.corpusId declared ≡ "recovery-baseline-2026-09-23"
    recoveryRevisionIsImmutable :
      Corpus.recoveryRevision declared ≡
        "2dbf8937fc43e8fa035e8f7575e0e8fe81b2b92c"
    declaredObservationSetIsClosed :
      Consolidation Observation roadmap declared

proof : Proposition
proof = satisfied refl refl closure

evidence : StaticEvidence 
evidence = staticEvidence Proposition proof