Multilayer Identity Insufficiency

Abstract

A concrete two-layer cone loses its upper bit, and noninjective projections neither admit left inverses nor determine a unique fiber-constant assignment.

Definition 1.1 (A compatible family commutes with every downward projection).

$$\begin{gathered} \forall I:Type,[\mathrm{Preorder}\left(I\right)], \\ S:I\to Type,p:\forall i,j:I,i\le j\to S\left(j\right)\to S\left(i\right), \\ \mathrm{CompatibleFamily}\left(S,p\right)=\{s:\forall i:I,S\left(i\right)\mid \forall i,j:I,h:i\le j,p\left(i,j,h,s\left(j\right)\right)=s\left(i\right)\}. \end{gathered}$$

Formalization. D5/S3/ConceptDynamics/Identity/MultilayerIdentityInsufficiency.CompatibleFamily (✓ std3).

Source. Repository-derived.

Commentary.

For a preordered layer index, a state family S, and downward maps p, a compatible family consists of one state s_i at each layer such that projecting s_j along every proof i <= j gives s_i.

Lemma 1.2 (The two-layer cone loses its upper bit).

$$\mathrm{Nonempty}\left(\mathrm{CompatibleFamily}\left(twoLayerState,twoLayerProjection\right)\right)\wedge \left(\exists x\in \mathrm{CompatibleFamily}\left(twoLayerState,twoLayerProjection\right),y\in \mathrm{CompatibleFamily}\left(twoLayerState,twoLayerProjection\right),x_0=y_0\wedge x_1\ne y_1\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Identity/MultilayerIdentityInsufficiency.two_layer_cone_nonempty_and_loses_high_information (✓ std3). ∎

Source. Repository-derived.

Commentary.

The concrete system has a one-point lower layer and a Boolean upper layer. Each Boolean value determines a compatible subject, so the space of compatible families is inhabited.

The subjects determined by false and true have the same lower component because the downward projection forgets the bit, while their upper components remain distinct. Thus lower-layer agreement does not recover the higher-layer state.

Theorem 1.3 (A noninjective layer cannot recover or choose uniquely).

$$\forall Sj\in Type,Si\in Type,Norm\in Type,p\in Sj\to Si,n1\in Norm,n2\in Norm,\left(\left(\neg \mathrm{Injective}\left(p\right)\right)\wedge n1\ne n2\right)\Rightarrow \left(\left(\neg \left(\exists r\in Si\to Sj,\mathrm{LeftInverse}\left(r,p\right)\right)\right)\wedge \left(\exists q1\in Sj\to Norm,q2\in Sj\to Norm,\mathrm{FiberConstant}\left(p,q1\right)\wedge \left(\mathrm{FiberConstant}\left(p,q2\right)\wedge q1\ne q2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Identity/MultilayerIdentityInsufficiency.noninjective_layer_cannot_recover (✓ std3). ∎

Source. Repository-derived.

Commentary.

A left inverse would force the layer projection to be injective. Hence a noninjective projection admits no recovery map that reconstructs every higher-layer state.

When the normative codomain contains two distinct values, the two constant assignments to those values are both constant on every projection fiber. They are distinct legal assignments, so fiber compatibility alone does not select a unique high-level choice.

References

• Truth anchor: D5/S3/ConceptDynamics/Identity/MultilayerIdentityInsufficiency.CompatibleFamily
• Truth anchor: D5/S3/ConceptDynamics/Identity/MultilayerIdentityInsufficiency.noninjective_layer_cannot_recover
• Truth anchor: D5/S3/ConceptDynamics/Identity/MultilayerIdentityInsufficiency.two_layer_cone_nonempty_and_loses_high_information