Function-Graph Spectrum Collision

Abstract

Equal trace and rank spectra do not determine an eight-state functional graph.

Theorem 1.1 (The complete spectra agree while the functional graphs do not).

$t a u A (0) = 0 \land t a u A (1) = 0 \land t a u A (2) = 0 \land t a u A (3) = 0 \land t a u A (4) = 1 \land t a u A (5) = 1 \land t a u A (6) = 1 \land t a u A (7) = 2 \land t a u B (0) = 0 \land t a u B (1) = 0 \land t a u B (2) = 0 \land t a u B (3) = 0 \land t a u B (4) = 1 \land t a u B (5) = 1 \land t a u B (6) = 2 \land t a u B (7) = 2 \land (\forall x, t a u A (x) = x ⟺ x = 0) \land (\forall x, t a u B (x) = x ⟺ x = 0) \land card (F in (8)) = 8 \land r ank Sp ec t r u mVa l u e (t a u A, 1) = 3 \land r ank Sp ec t r u mVa l u e (t a u B, 1) = 3 \land (\forall k, 2 \leq k \Rightarrow r ank Sp ec t r u mVa l u e (t a u A, k) = 1) \land (\forall k, 2 \leq k \Rightarrow r ank Sp ec t r u mVa l u e (t a u B, k) = 1) \land (\forall k, t r a ce Sp ec t r u mVa l u e (t a u A, k) = t r a ce Sp ec t r u mVa l u e (t a u B, k)) \land (\forall k, r ank Sp ec t r u mVa l u e (t a u A, k) = r ank Sp ec t r u mVa l u e (t a u B, k)) \land d e pt h O n e L e a f M u lt i se t (t a u A) = {3, 1, 0} \land d e pt h O n e L e a f M u lt i se t (t a u B) = {2, 2, 0} \land d e pt h O n e L e a f M u lt i se t (t a u A) \neq = d e pt h O n e L e a f M u lt i se t (t a u B) \land \neg\exists e : Eq u i v . P er m (F in (8)), Semiconj (e, t a u A, t a u B) .$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/InverseLimits/FunctionGraphSpectrumCollision.same_trace_rank_spectra_not_function_graph_conjugate (✓ std3). ∎

Source. Repository-derived.

Commentary.

Identify 0,a,b,c,d,e,f,g with Fin 8 in that order. The displayed sixteen equations are the complete tables of tauA and tauB. The rank value is the cardinality of the iterated image, and the trace value is the number of fixed points of the iterate.

A leaf has no predecessor. The depth-one leaf multiset collects the leaf counts at the non-root children mapped directly to 0. Its values are {3,1,0} and {2,2,0}.

A functional-graph isomorphism is expressed without a new classifier: it is a permutation semiconjugating tauA to tauB. Such a map would preserve every fiber cardinality, but tauA has a fiber of size three and tauB has none, so no conjugacy exists.

Repository and pinned-Mathlib searches found no equal or stronger statement. Mathlib supplies Semiconj, iterate_add_apply, image_const, and card_congr; GitHub Lean-code search found only those building blocks and mirrors.

References

Truth anchor: D5/S3/ObserverMemory/InverseLimits/FunctionGraphSpectrumCollision.same_trace_rank_spectra_not_function_graph_conjugate

Keyboard shortcuts

trureturing Blueprint

Function-Graph Spectrum Collision

Abstract

References