Finite Reverse Criterion

Abstract

Empty carry yields a unique descent on the effective image.

Theorem 1.1 (Empty carry determines the effective-image descent).

$$\forall X,Y,B_C,B_D:\mathrm{Type},[\mathrm{Fintype}(X)],[\mathrm{DecidableEq}(X)],[\mathrm{Fintype}(B_C)],[\mathrm{DecidableEq}(B_C)],[\mathrm{Fintype}(B_D)],[\mathrm{DecidableEq}(B_D)],F:X\to Y,q_C:X\to B_C,q_D:Y\to B_D,\mathrm{IsEmpty}\left(\mathrm{Carry}(F,q_C,q_D)\right)\Rightarrow \exists !\overline{F}:\mathrm{range}(q_C)\to B_D,\forall x:X,\overline{F}(\mathrm{rangeFactorization}(q_C,x))=q_D(F(x)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Transport/FiniteReverseCriterion.finite_reverse_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let X, B_C, and B_D be finite types with decidable equality, let F map X to a process codomain Y, and let q_C and q_D be the current and future readouts. Carry consists exactly of pairs identified by q_C whose future readouts after F differ.

If the carry type is empty, there is a unique map from the realized range of q_C to B_D. On every source state, this map sends its effective current value to q_D(F(x)), so the image-restricted process/readout square commutes.

Pinned Mathlib supplies the canonical Set.rangeFactorization and Set.rangeSplitting maps used by the proof. Empty carry makes the chosen representative irrelevant, while every range element’s source witness proves uniqueness. Repository and pinned-library searches found no existing theorem packaging these facts.

This formalizes exactly theorem/13.2 of formal-concept-dynamics, atom generic-residual-88ab11467c06c97a9dd12a0627951364cfe0c6a897813bf9209fc113283a304e. No claim about infinite constructive models or the neighboring quantitative defect is included.

References

• Truth anchor: D5/S3/ConceptDynamics/Transport/FiniteReverseCriterion.finite_reverse_criterion