IndisputableMonolith.Verification.RecognitionClosureNonVacuityCert

   1import Mathlib
   2import IndisputableMonolith.RecogSpec.Spec
   3import IndisputableMonolith.RecogSpec.ClosureShim
   4
   5/-!
   6# Recognition Closure Non-Vacuity Certificate
   7
   8This certificate upgrades the RS “closure” story by explicitly asserting that the
   9closure bundle includes **proved** content (not just Prop-valued fields inside packs):
  10
  11- the `UD_explicit φ` strong-CP witness holds,
  12- the 8-tick minimal witness holds,
  13- and the two-branch Born bridge holds.
  14
  15These are packaged inside `RecogSpec.Inevitability_dimless` (and thus inside
  16`RecogSpec.Recognition_Closure`) so closure is not vacuously satisfied by merely carrying
  17unproven propositions.
  18-/
  19
  20namespace IndisputableMonolith
  21namespace Verification
  22namespace RecognitionClosure
  23
  24open IndisputableMonolith.RecogSpec
  25
  26structure RecognitionClosureNonVacuityCert where
  27  deriving Repr
  28
  29@[simp] def RecognitionClosureNonVacuityCert.verified (_c : RecognitionClosureNonVacuityCert) : Prop :=
  30  ∀ φ : ℝ,
  31    RecogSpec.Recognition_Closure φ →
  32      (RecogSpec.UD_explicit φ).strongCP0 ∧
  33      (RecogSpec.UD_explicit φ).eightTick0 ∧
  34      (RecogSpec.UD_explicit φ).born0
  35
  36@[simp] theorem RecognitionClosureNonVacuityCert.verified_any (c : RecognitionClosureNonVacuityCert) :
  37    RecognitionClosureNonVacuityCert.verified c := by
  38  intro φ h
  39  -- `Recognition_Closure` is `Inevitability_dimless ∧ Inevitability_absolute`
  40  -- and `Inevitability_dimless` now carries the proven UD-explicit properties.
  41  exact h.left.right
  42
  43end RecognitionClosure
  44end Verification
  45end IndisputableMonolith
  46