Finite Error-Class Half-Life

Abstract

Finite same-class capture histories have an executable least stable gate suffix, while the ink-not-dry recurrence remains unconverged.

Theorem 1.1 (Half-life is computable and the ink-not-dry trace is nontrivial).

$$\begin{array}{r}\forall C,I:\mathrm{Type},\\ [\mathrm{DecidableEq}\left(C\right)],\\ tau:\mathrm{OperationalTrajectory}\left(C,I\right),\\ c:C,n:Nat,\\ (\mathrm{gateHalfLife}\left(tau,c\right)=\mathrm{some}\left(n\right)⟺(\mathrm{StableAtGate}\left(\mathrm{classMaturity}\left(tau,c\right),n\right)\wedge \forall m:Nat,m<n\Rightarrow \neg \mathrm{StableAtGate}\left(\mathrm{classMaturity}\left(tau,c\right),m\right)))\wedge \\ (\mathrm{classMaturity}\left(inkNotDryTrajectory,unit\right)=[wall,wall,wall])\wedge \\ \mathrm{gateHalfLife}\left(inkNotDryTrajectory,unit\right)=none.\end{array}$$

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

Source. Repository-derived.

Commentary.

The frozen operational trajectory supplies a finite event list and its same-class capture history. The executable half-life searches the finite list of suffixes and rejects the empty suffix.

A returned index is characterized independently: its nonempty suffix is entirely gate-or-higher, and every earlier suffix fails that condition. Thus the value is the first stable capture index, not merely any successful suffix.

The ink-not-dry witness contains three occurrences of one error class, all captured at wall level. Its compiled maturity list is exactly three walls and its executable half-life is none.

References

• Truth anchor: D5/S3/ConceptDynamics/OperationalTuition/HalfLifeWellDefined.half_life_computable_and_ink_not_dry_nontrivial
• Dependency: D5/S3/ConceptDynamics/OperationalTuition/InstitutionalMappingAndCaptureFiltration