Preregistered Artifact Acceptance

Abstract

A missing routing envelope permits independent artifact acceptance exactly when a fixed criterion was recorded before production, and that witness survives seat death.

Theorem 1.1 (Missing-envelope acceptance is preregistered and inheritable).

$$\begin{array}{r}\forall C,B:\mathrm{Type},\\ [\mathrm{DecidableEq}\left(C\right)],[\mathrm{DecidableEq}\left(B\right)],\\ v:C\Rightarrow \mathrm{ToyState}\left(B\right)\Rightarrow Bool,\\ d:\mathrm{DeliveryRecord}\left(C,B\right),\\ (\mathrm{missingEnvelopeAcceptance}\left(v,d\right)=true⟺(\mathrm{EnvelopeMissing}\left(d\right)\wedge \mathrm{Nonempty}\left(\mathrm{PreregisteredAcceptanceWitness}\left(v,d\right)\right)))\wedge \\ (\mathrm{Nonempty}\left(\mathrm{PreregisteredAcceptanceWitness}\left(v,d\right)\right)\Rightarrow \mathrm{missingEnvelopeAcceptance}\left(v,\mathrm{inheritAfterSeatDeath}\left(d\right)\right)=true).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/OperationalTuition/PreregisteredArtifactAcceptance.missing_envelope_acceptance_iff_preregistered_and_inheritable (✓ std3). ∎

Source. Repository-derived.

Commentary.

A finite delivery keeps the optional routing envelope separate from a frozen toy artifact trajectory. The distinguished artifact checkpoint follows the complete finite prefix used by the independent verifier.

The executable judgment scans only that prefix. Its forward direction extracts a concrete registered criterion whose fixed Boolean verifier accepts the computed final artifact state; the reverse direction runs that witness.

Seat death clears the envelope and liveness flag but preserves the artifact and pre-artifact prefix. Consequently the same finite witness establishes postmortem acceptance without trusting a self-reported status.

References

• Truth anchor: D5/S3/ConceptDynamics/OperationalTuition/PreregisteredArtifactAcceptance.missing_envelope_acceptance_iff_preregistered_and_inheritable
• Dependency: D5/S3/ConceptDynamics/OperationalTuition/ArtifactSufficiencyAndKillLoss