Finite response tables

Abstract

Finite response tables compute least forgetting depths and deterministic sorted quotient sections for numbered incoming lifts.

Throughout, n and q are arbitrary natural numbers, A is a natural count matrix on Fin n, and L is an IncomingLift A (Fin q), including its given surjective projection and typed numbered-edge lifts. Nat subtraction is truncated. ForgettingDepths(L) denotes every natural d satisfying Forgets(L,d), without a bounded-depth restriction. In the displays, liftValue(L,edge(i,j,a),u) is the value of the typed lift in the guarded target fiber; proof arguments are implicit. sortedIndex and sortedEntry are the inverse and forward maps of the increasing Finset.orderIsoOfFin, and QuotientClass denotes the response class at the displayed depth.

Definition 1.1 (Numbered input arrays).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\mathrm{Fields}\left(\mathrm{LiftTables}\left(n,q,A\right),\mathrm{project}\left(\mathrm{Fin}\left(q\right)\to \mathrm{Fin}\left(n\right)\right),\mathrm{predecessor}\left(\forall i\in \mathrm{Fin}\left(n\right),j\in \mathrm{Fin}\left(n\right),a\in \mathrm{Fin}\left(\mathrm{entry}\left(A,i,j\right)\right),u\in \mathrm{Fin}\left(q\right),\mathrm{Fin}\left(q\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.LiftTables (✓ std3).

Source. Repository-derived.

Commentary.

The input stores a projection from Fin q to Fin n and a predecessor state for every ordered pair of base vertices, every parallel edge number and every state. Target-fiber checks precede use of entries.

Definition 1.2 (Finite input validation).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall T\in \mathrm{LiftTables}\left(n,q,A\right),\mathrm{valid}\left(T\right)=\mathrm{decide}\left(\left(\forall i\in \mathrm{Fin}\left(n\right),\exists u\in \mathrm{Fin}\left(q\right),\mathrm{project}\left(T,u\right)=i\right)\wedge \left(\forall i\in \mathrm{Fin}\left(n\right),j\in \mathrm{Fin}\left(n\right),a\in \mathrm{Fin}\left(\mathrm{entry}\left(A,i,j\right)\right),u\in \mathrm{Fin}\left(q\right),\mathrm{project}\left(T,u\right)=j\Rightarrow \mathrm{project}\left(T,\mathrm{predecessor}\left(T,i,j,a,u\right)\right)=i\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.valid (✓ std3).

Source. Repository-derived.

Commentary.

The Boolean validator checks surjectivity and source-fiber coherence for each actual numbered edge whenever the supplied state lies in its target fiber. Zero edge counts and empty finite domains remain part of the input family.

Definition 1.3 (Typed incoming lift).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall T\in \mathrm{LiftTables}\left(n,q,A\right),h\in \mathrm{valid}\left(T\right)=true,\mathrm{project}\left(\mathrm{toLift}\left(T,h\right)\right)=\mathrm{project}\left(T\right)\wedge \left(\forall i\in \mathrm{Fin}\left(n\right),j\in \mathrm{Fin}\left(n\right),a\in \mathrm{Fin}\left(\mathrm{entry}\left(A,i,j\right)\right),u\in \mathrm{Fin}\left(q\right),hu\in \mathrm{project}\left(T,u\right)=j,\mathrm{liftValue}\left(\mathrm{toLift}\left(T,h\right),\mathrm{edge}\left(i,j,a\right),u\right)=\mathrm{predecessor}\left(T,i,j,a,u\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.toLift (✓ std3).

Source. Repository-derived.

Commentary.

A successful validator supplies the proof fields of the original IncomingLift structure. The projection and predecessor values are the supplied entries themselves.

Definition 1.4 (Pathwise response table).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),v\in \mathrm{Fin}\left(q\right),\mathrm{table}\left(L,0,u,v\right)=\mathrm{decide}\left(u=v\right)\wedge \mathrm{table}\left(L,d+1,u,v\right)=\mathrm{andBool}\left(\mathrm{decide}\left(\mathrm{project}\left(L,u\right)=\mathrm{project}\left(L,v\right)\right),\mathrm{decide}\left(\forall i\in \mathrm{Fin}\left(n\right),j\in \mathrm{Fin}\left(n\right),a\in \mathrm{Fin}\left(\mathrm{entry}\left(A,i,j\right)\right),\left(\mathrm{project}\left(L,u\right)=j\wedge \mathrm{project}\left(L,v\right)=j\right)\Rightarrow \mathrm{table}\left(L,d,\mathrm{liftValue}\left(L,\mathrm{edge}\left(i,j,a\right),u\right),\mathrm{liftValue}\left(L,\mathrm{edge}\left(i,j,a\right),v\right)\right)=true\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.table (✓ std3).

Source. Repository-derived.

Commentary.

Depth zero compares original state numbers. A successor first checks equality of projections, then checks the preceding table on both lifts along each identical numbered incoming edge. Parallel edges are never merged or averaged.

Definition 1.5 (Whole-fiber forgetting).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\forall d\in Nat,\mathrm{forgets}\left(L,d\right)=\mathrm{decide}\left(\forall u\in \mathrm{Fin}\left(q\right),v\in \mathrm{Fin}\left(q\right),\mathrm{project}\left(L,u\right)=\mathrm{project}\left(L,v\right)\Rightarrow \mathrm{table}\left(L,d,u,v\right)=true\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.forgets (✓ std3).

Source. Repository-derived.

Commentary.

At a given depth, every pair in each terminal projection fiber must have a true response-table bit. This is a pathwise forgetting test, not a marginal count.

Definition 1.6 (Inclusive finite depth search).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\forall d\in Nat,d\in \mathrm{successes}\left(L\right)\iff \left(d\le q-n\wedge \mathrm{forgets}\left(L,d\right)=true\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.successes (✓ std3).

Source. Repository-derived.

Commentary.

The successful-depth set filters every natural number from zero through q minus n, inclusive, using the actual forgetting Boolean.

Definition 1.7 (Least forgetting decision).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\mathrm{minimumDepth}\left(L\right)=\mathrm{ifThenElse}\left(\mathrm{Nonempty}\left(\mathrm{successes}\left(L\right)\right),\mathrm{some}\left(\mathrm{minimumElement}\left(\mathrm{successes}\left(L\right)\right)\right),none\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.minimumDepth (✓ std3).

Source. Repository-derived.

Commentary.

The result is some of the finite set minimum when a successful entry exists, and none otherwise. The implementation uses Finset.min’; the global completeness justification reuses the existing common nilpotency bound.

Definition 1.8 (Response class enumeration).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),v\in \mathrm{Fin}\left(q\right),v\in \mathrm{members}\left(L,d,u\right)\iff \mathrm{table}\left(L,d,v,u\right)=true$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.members (✓ std3).

Source. Repository-derived.

Commentary.

For a supplied state, the class is the finite set of original state numbers whose table comparison with that state is true.

Definition 1.9 (Least original state representative).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),\mathrm{representative}\left(L,d,u\right)=\mathrm{minimumElement}\left(\mathrm{members}\left(L,d,u\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.representative (✓ std3).

Source. Repository-derived.

Commentary.

The representative is the least member of that class. The supplied state certifies nonemptiness; no inhabitant of an empty state domain is chosen.

Definition 1.10 (Sorted representative set).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),u\in \mathrm{representatives}\left(L,d\right)\iff \mathrm{representative}\left(L,d,u\right)=u$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.representatives (✓ std3).

Source. Repository-derived.

Commentary.

Fixed points of the representative operation form the finite set of class representatives, ordered by the original state numbers.

Definition 1.11 (Dense sorted class numbers).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),\mathrm{classOf}\left(L,d,u\right)=\mathrm{sortedIndex}\left(\mathrm{representatives}\left(L,d\right),\mathrm{representative}\left(L,d,u\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.classOf (✓ std3).

Source. Repository-derived.

Commentary.

The inverse of Finset.orderIsoOfFin maps the computed least representative to its dense finite class index. Numbering follows the sorted state order.

Definition 1.12 (Computed quotient section).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\forall d\in Nat,i\in \mathrm{Fin}\left(\mathrm{card}\left(\mathrm{representatives}\left(L,d\right)\right)\right),\mathrm{representativeAt}\left(L,d,i\right)=\mathrm{sortedEntry}\left(\mathrm{representatives}\left(L,d\right),i\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.representativeAt (✓ std3).

Source. Repository-derived.

Commentary.

The forward order isomorphism maps a dense class index to its original representative state. Its domain depends on the computed representative count.

Definition 1.13 (Explicit quotient transport).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\left(\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),\mathrm{apply}\left(\mathrm{quotientEquiv}\left(L,d\right),\mathrm{QuotientClass}\left(L,d,u\right)\right)=\mathrm{classOf}\left(L,d,u\right)\right)\wedge \left(\forall d\in Nat,i\in \mathrm{Fin}\left(\mathrm{card}\left(\mathrm{representatives}\left(L,d\right)\right)\right),\mathrm{inverseApply}\left(\mathrm{quotientEquiv}\left(L,d\right),i\right)=\mathrm{QuotientClass}\left(L,d,\mathrm{representativeAt}\left(L,d,i\right)\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.quotientEquiv (✓ std3).

Source. Repository-derived.

Commentary.

Quotient.lift sends a semantic response class to its computed dense index. The inverse uses the computed section. The executable output uses neither Quotient.out nor Fintype.equivFin nor classical witness selection.

Definition 1.14 (Numbered identity and swap input).

$$\forall a\in \mathrm{Fin}\left(2\right),u\in \mathrm{Fin}\left(2\right),\mathrm{project}\left(parallelIdentityFlipTables,u\right)=0\wedge \mathrm{predecessor}\left(parallelIdentityFlipTables,0,0,a,u\right)=\mathrm{ifThenElse}\left(a=0,u,\mathrm{ifThenElse}\left(u=0,1,0\right)\right)$$

Formalization. D5/S3/ConceptDynamics/Coding/FiniteResponseTable.parallelIdentityFlipTables (✓ std3).

Source. Repository-derived.

Commentary.

This concrete checker input has one base vertex, two states and two parallel edges. Edge number zero preserves the state; edge number one swaps the two states. The bounded checker tests both numbered lifts separately.

Theorem 1.15 (Complete finite response and quotient refinement).

$$\forall n\in Nat,q\in Nat,A\in \mathrm{CountMat}\left(n,n\right),\forall L\in \mathrm{IncomingLift}\left(A,\mathrm{Fin}\left(q\right)\right),\left(\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),v\in \mathrm{Fin}\left(q\right),\mathrm{table}\left(L,d,u,v\right)=true\iff \mathrm{response}\left(L,d,u,v\right)\right)\wedge \left(\left(\forall d\in Nat,\mathrm{forgets}\left(L,d\right)=true\iff \mathrm{Forgets}\left(L,d\right)\right)\wedge \left(\left(\forall d\in Nat,\mathrm{minimumDepth}\left(L\right)=\mathrm{some}\left(d\right)\iff \mathrm{IsLeast}\left(\mathrm{ForgettingDepths}\left(L\right),d\right)\right)\wedge \left(\left(\mathrm{minimumDepth}\left(L\right)=none\iff \left(\neg \left(\exists d\in Nat,\mathrm{Forgets}\left(L,d\right)\right)\right)\right)\wedge \left(\left(\forall d\in Nat,\mathrm{minimumDepth}\left(L\right)=\mathrm{some}\left(d\right)\Rightarrow d\le q-n\right)\wedge \left(\left(\forall d\in Nat,\mathrm{table}\left(L,d+1\right)=\mathrm{table}\left(L,d\right)\Rightarrow \left(\forall t\in Nat,\mathrm{table}\left(L,d+t\right)=\mathrm{table}\left(L,d\right)\right)\right)\wedge \left(\left(\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),v\in \mathrm{Fin}\left(q\right),\mathrm{classOf}\left(L,d,u\right)=\mathrm{classOf}\left(L,d,v\right)\iff \mathrm{response}\left(L,d,u,v\right)\right)\wedge \left(\left(\forall d\in Nat,i\in \mathrm{Fin}\left(\mathrm{card}\left(\mathrm{representatives}\left(L,d\right)\right)\right),\mathrm{classOf}\left(L,d,\mathrm{representativeAt}\left(L,d,i\right)\right)=i\right)\wedge \left(\left(\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),\mathrm{representativeAt}\left(L,d,\mathrm{classOf}\left(L,d,u\right)\right)=\mathrm{representative}\left(L,d,u\right)\right)\wedge \left(\left(\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),\mathrm{response}\left(L,d,\mathrm{representative}\left(L,d,u\right),u\right)\right)\wedge \left(\forall d\in Nat,u\in \mathrm{Fin}\left(q\right),v\in \mathrm{Fin}\left(q\right),\mathrm{response}\left(L,d,v,u\right)\Rightarrow \mathrm{representative}\left(L,d,u\right)\le v\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Coding/FiniteResponseTable.finite_response_table_refinement (✓ std3). ∎

Source. Repository-derived.

Commentary.

1. For every depth and every pair of states, the table bit is true exactly when the original IncomingLift response relation holds.

2. For every depth, the whole-fiber forgetting Boolean is true exactly when the original Forgets predicate holds.

3. For every natural depth, minimumDepth returns that depth exactly when it is least among all forgetting depths.

4. minimumDepth is none exactly when no finite forgetting depth exists.

5. Every returned depth is at most q minus n, with truncated natural subtraction and no added bound hypothesis.

6. Equality of two adjacent whole response tables persists at every later depth.

7. Two dense class numbers agree exactly when their states have the original response relation.

8. Classifying the selected state of any dense class returns the same class index.

9. Selecting the class of a state returns its computed least representative.

10. Every computed representative is response-related to its input state.

11. That representative is no greater than any response-related original state number.

The proof relates the actual edge recursion to response_successor_iff and response_zero_and_step, connects forgetting to the private original pathwise kernel equivalence, and uses the existing common_nilpotency_forgetting_bound. The new algorithm refinement is distinct from those supplier results.

The theorem concerns one incoming lift. Separate applications can supply independent least depths for two lifts, but this module does not construct a controlled trace, serialize a trace exporter or decide a fixed-positive-lag certificate.

The domain permits zero states, zero base vertices, zero edge counts and depth zero. Surjectivity is part of the supplied IncomingLift. No essentiality, positive order, common lag, certificate or extra finite bound is added to this one-lift result.

References

• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.LiftTables
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.classOf
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.finite_response_table_refinement
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.forgets
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.members
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.minimumDepth
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.parallelIdentityFlipTables
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.quotientEquiv
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.representative
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.representativeAt
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.representatives
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.successes
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.table
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.toLift
• Truth anchor: D5/S3/ConceptDynamics/Coding/FiniteResponseTable.valid
• Dependency: D5/S3/ConceptDynamics/Coding/CommonNilpotencyForgettingBound
• Dependency: D5/S3/ConceptDynamics/Coding/ResponseKernelRecursion