GV123 makes the learning gate reachable from zero instead of assuming that the human principal has followed Govenv prospectively since learning continuity was introduced. The bootstrap curriculum remains Protocol judgment; the compiler checks that it exists as governed data, that outstanding debt is derived from the current lesson contracts minus matching human evidence, and that the narrow evidence-only candidate path can advance only by strictly reducing governed debt. GV124 strengthens what counts as matching evidence by binding it to the lesson’s exact review contract.
{-# OPTIONS --safe #-}
module Govenv.Assurance.GV123 where
open import Agda.Builtin.Bool using (true; false)
open import Agda.Builtin.Equality using (_≡_; refl)
open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Learning using
(learningEvidenceCandidateAllowed; requirementsPresent)
open import Govenv.Learning using
( allLearningPrompts; allLessonsEvidenced; bootstrapComplete; bootstrapLessons
; lessonRequirements; outstanding; pendingLessonRequirements )
renaming (evidence to recordedEvidence)
record Proposition : Set where
constructor satisfied
field
bootstrapBaselineIsNonEmpty :
requirementsPresent (lessonRequirements bootstrapLessons) ≡ true
bootstrapCompletionIsEvidenceDerived :
bootstrapComplete ≡ allLessonsEvidenced bootstrapLessons recordedEvidence
outstandingDebtIsDerived :
outstanding ≡ pendingLessonRequirements allLearningPrompts recordedEvidence
evidenceOnlyReductionIsAllowed :
learningEvidenceCandidateAllowed true 13 12 ≡ true
evidenceWithoutDebtReductionIsRejected :
learningEvidenceCandidateAllowed true 13 13 ≡ false
mixedSemanticEvidenceCandidateIsRejected :
learningEvidenceCandidateAllowed false 13 12 ≡ false
proof : Proposition
proof = satisfied refl refl refl refl refl refl
evidence : StaticEvidence 123
evidence = staticEvidence Proposition proof