Continuant obstruction and coordinate dimensions

Abstract

Continuant obstruction and coordinate dimensions.

Definition 1.1 (Theta coordinate structure).

$$\forall E:\mathrm{Type},[\mathrm{AddCommGroup}\left(E\right)][\mathrm{Module}\left(\mathrm{Real},E\right)]\forall k:\mathrm{Nat},\forall t:\mathrm{Real},\forall e:\mathrm{Real},\mathrm{ThetaCoordinates}Ekte:\mathrm{structure}(A:E{\to }_{l[\mathrm{Real}]}\mathrm{Real};D:E{\to }_{l[\mathrm{Real}]}\mathrm{Real};B:E{\to }_{l[\mathrm{Real}]}\mathrm{Real};C:E{\to }_{l[\mathrm{Real}]}\mathrm{Real};B^{\prime }:E{\to }_{l[\mathrm{Real}]}\mathrm{Real};C^{\prime }:E{\to }_{l[\mathrm{Real}]}\mathrm{Real};Y:\mathrm{Nat}\to E{\to }_{l[\mathrm{Real}]}\mathrm{Real};(Y\left(0\right)=A)\wedge ((Y\left(6\cdot k+4\right)=D)\wedge ((\forall x:E,t\cdot B\left(x\right)=A\left(x\right)+C\left(x\right))\wedge ((\forall x:E,t\cdot C\left(x\right)=B\left(x\right)+D\left(x\right))\wedge ((\forall x:E,t\cdot B^{\prime }\left(x\right)=A\left(x\right)+C^{\prime }\left(x\right))\wedge ((\forall x:E,t\cdot C^{\prime }\left(x\right)=B^{\prime }\left(x\right)+D\left(x\right))\wedge ((\forall x:E,Y\left(1,x\right)=\left(t+e\right)\cdot A\left(x\right)-B\left(x\right)-B^{\prime }\left(x\right))\wedge ((\forall x:E,Y\left(6\cdot k+3,x\right)=\left(t+e\right)\cdot D\left(x\right)-C\left(x\right)-C^{\prime }\left(x\right))\wedge ((\forall j:\mathrm{Nat},(j+2\le 6\cdot k+4)\Rightarrow (\forall x:E,Y\left(j+2,x\right)=t\cdot Y\left(j+1,x\right)-Y\left(j,x\right)))\wedge (\forall x:E,(A\left(x\right)=0)\Rightarrow ((D\left(x\right)=0)\Rightarrow ((B\left(x\right)=0)\Rightarrow ((C\left(x\right)=0)\Rightarrow ((B^{\prime }\left(x\right)=0)\Rightarrow ((C^{\prime }\left(x\right)=0)\Rightarrow ((\forall j:\mathrm{Nat},(j\le 6\cdot k+4)\Rightarrow (Y\left(j,x\right)=0))\Rightarrow (x=0)))))))))))))))))$$

Formalization. D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaRecurrence.ThetaCoordinates (✓ std3).

Source. Repository-derived.

Acknowledgement. Monther Rashed Alfuraidan, Suliman Khan, Lorenzo Sauras-Altuzarra (2026). Metric dimension and maximum eigenvalue multiplicity of graph Laplacians. DOI: 10.48550/arXiv.2610.26875. URL: https://arxiv.org/abs/2610.26875v1.

Commentary.

The fields A,D,B,C,B’,C’ are real linear maps, and Y is a sequence of real linear maps. The first and last fields identify the long-path endpoints; the four short-path equations, the two terminal equations and the bounded recurrence describe the operator. The separates field says that these coordinates determine a vector.

Theorem 1.2 (Singular coordinate dimension bound).

$$\forall E:\mathrm{Type},[\mathrm{AddCommGroup}\left(E\right)][\mathrm{Module}\left(\mathrm{Real},E\right)][\mathrm{FiniteDimensional}\left(\mathrm{Real},E\right)]\forall k:\mathrm{Nat},\forall t:\mathrm{Real},((t=1)\vee (t=-(1)))\Rightarrow (\mathrm{ThetaCoordinates}\left(E,k,t,1\right)\to \left(\mathrm{Module}.\mathrm{finrank}\left(\mathrm{Real},E\right)\le 2\right))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaRecurrence.model_laplacian_singular_finrank (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Monther Rashed Alfuraidan, Suliman Khan, Lorenzo Sauras-Altuzarra (2026). Metric dimension and maximum eigenvalue multiplicity of graph Laplacians. DOI: 10.48550/arXiv.2610.26875. URL: https://arxiv.org/abs/2610.26875v1.

Commentary.

At t=1 and t=−1, the recurrence is periodic. The terminal equations leave at most 2 independent real coordinates.

Theorem 1.3 (Singular coordinate dimension bound).

$$\forall E:\mathrm{Type},[\mathrm{AddCommGroup}\left(E\right)][\mathrm{Module}\left(\mathrm{Real},E\right)][\mathrm{FiniteDimensional}\left(\mathrm{Real},E\right)]\forall k:\mathrm{Nat},\forall t:\mathrm{Real},((t=1)\vee (t=-(1)))\Rightarrow (\mathrm{ThetaCoordinates}\left(E,k,t,-(1)\right)\to \left(\mathrm{Module}.\mathrm{finrank}\left(\mathrm{Real},E\right)\le 1\right))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaRecurrence.model_signless_singular_finrank (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Monther Rashed Alfuraidan, Suliman Khan, Lorenzo Sauras-Altuzarra (2026). Metric dimension and maximum eigenvalue multiplicity of graph Laplacians. DOI: 10.48550/arXiv.2610.26875. URL: https://arxiv.org/abs/2610.26875v1.

Commentary.

At t=1 and t=−1, the recurrence is periodic. The terminal equations leave at most 1 independent real coordinates.

Theorem 1.4 (Nonsingular coordinate dimension bound).

$$\forall E:\mathrm{Type},[\mathrm{AddCommGroup}\left(E\right)][\mathrm{Module}\left(\mathrm{Real},E\right)][\mathrm{FiniteDimensional}\left(\mathrm{Real},E\right)]\forall k:\mathrm{Nat},\forall eQ:\mathrm{Rat},\forall t:\mathrm{Real},((eQ=1)\vee (eQ=-(1)))\Rightarrow ((t\ne 1)\Rightarrow ((t\ne -(1))\Rightarrow (\mathrm{ThetaCoordinates}\left(E,k,t,(eQ:\mathrm{Real})\right)\to \left(\mathrm{Module}.\mathrm{finrank}\left(\mathrm{Real},E\right)\le 1\right))))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaRecurrence.model_nonsingular_finrank (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Monther Rashed Alfuraidan, Suliman Khan, Lorenzo Sauras-Altuzarra (2026). Metric dimension and maximum eigenvalue multiplicity of graph Laplacians. DOI: 10.48550/arXiv.2610.26875. URL: https://arxiv.org/abs/2610.26875v1.

Commentary.

Away from t=±1, endpoints determine every coordinate. If two endpoint coordinates were independent, two consecutive continuant values would be forced. Their determinant identity and quadratic conjugation exclude that collision.

References

• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaRecurrence.ThetaCoordinates
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaRecurrence.model_laplacian_singular_finrank
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaRecurrence.model_nonsingular_finrank
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/TwinFreeThetaRecurrence.model_signless_singular_finrank
• Dependency: D5/S3/Combinatorics/SpectralGraph/CyclicTridiagonalTransferTrace