Institutional Mapping and Capture Filtration

Abstract

Append-only institution registration and T1-compliant event classification make operational tuition monotone, decidable, and locally auditable.

Theorem 1.1 (Institution domains grow and defects are decidable).

$$\begin{gathered} \forall C,I:Type,[\mathrm{DecidableEq}\left(C\right)], \\ (\forall tau,upsilon:\mathrm{OperationalTrajectory}\left(C,I\right),\mathrm{IsTrajectoryPrefix}\left(tau,upsilon\right)\Rightarrow \mathrm{institutionDomain}\left(tau\right)\subseteq \mathrm{institutionDomain}\left(upsilon\right))\wedge \\ (\forall h:\mathrm{List}\left(\mathrm{Event}\left(C\right)\right),e:\mathrm{Event}\left(C\right),\mathrm{defectDecision}\left(h,e\right)=true⟺\mathrm{InstitutionalDefect}\left(h,e\right)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

An operational trajectory is a finite event list. A registration event adds its error class to the defined domain of the partial institution map, and list extension never removes that witness.

The second conjunct is computational: defectDecision returns true exactly when the class occurred earlier and its institution was already registered. Thus the same-class recurrence violation is decidable without a private axiom.

Theorem 1.2 (Capture levels filter and decreases locate defects).

$$\begin{gathered} \forall C,I:Type,[\mathrm{DecidableEq}\left(C\right)], \\ tau:T1CompliantTrajectory\left(C,I\right), \\ \mathrm{Monotone}\left(\mathrm{captureFiltration}\left(tau\right)\right)\wedge \\ (\forall h,m,s:\mathrm{List}\left(\mathrm{Event}\left(C\right)\right),e0,e1:\mathrm{Event}\left(C\right), \\ (\mathrm{events}\left(tau\right)=\mathrm{append}\left(h,\mathrm{append}\left([e0],\mathrm{append}\left(m,\mathrm{append}\left([e1],s\right)\right)\right)\right)\wedge \mathrm{institutionEstablished}\left(h,\mathrm{errorClass}\left(e0\right)\right)=true\wedge \mathrm{errorClass}\left(e0\right)=\mathrm{errorClass}\left(e1\right))\Rightarrow \\ \mathrm{capture}\left(e0\right)\le \mathrm{capture}\left(e1\right)\vee \mathrm{LocatedInstitutionalDefect}\left(tau,e1\right)). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The threshold event sets are monotone from wall through gate to author: raising the threshold retains every event already admitted.

For two occurrences of an already institutionalized class, either the later capture level is no lower or T1 marks that later occurrence as an institutional defect. The located-defect conclusion carries the exact prefix and suffix around the exceptional event.

The T1 law is evidence stored in T1CompliantTrajectory, not a Lean axiom. A compiled finite witness realizes the exception branch with a gate-to-wall decrease.

References

• Truth anchor: D5/S3/ConceptDynamics/OperationalTuition/InstitutionalMappingAndCaptureFiltration.capture_ladder_filtration_and_t1_nondecreasing
• Truth anchor: D5/S3/ConceptDynamics/OperationalTuition/InstitutionalMappingAndCaptureFiltration.institution_domain_monotone_and_defect_decidable