GenericLieLengthConstruction

Abstract

A three-colour anchored binary heap produces a logarithmic-length generating pair.

Definition 1.1 (heapColor).

$$\forall (v:\mathbb{N}),\mathrm{heapColor}v=\mathrm{if}v\le 1\mathrm{then}0\mathrm{else}\mathrm{Nat}.\mathrm{mod}(\mathrm{heapColor}(\mathrm{Nat}.\mathrm{div}v2)+(\mathrm{if}\mathrm{Nat}.\mathrm{mod}v2=0\mathrm{then}1\mathrm{else}2))3$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.heapColor (✓ std3).

Source. Repository-derived.

Commentary.

Three colours distinguish a parent from each child and distinguish its two children. Nat.div and Nat.mod are natural quotient and remainder.

Definition 1.2 (energy).

$$\forall (v:\mathbb{N}),\mathrm{energy}v=\mathrm{if}v=0\mathrm{then}7\mathrm{else}\mathrm{if}\mathrm{heapColor}v=0\mathrm{then}0\mathrm{else}\mathrm{if}\mathrm{heapColor}v=1\mathrm{then}1\mathrm{else}3$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.energy (✓ std3).

Source. Repository-derived.

Commentary.

The distinguished zero vertex has energy 7; the three heap colours have energies 0, 1 and 3.

Definition 1.3 (heapEdge).

$$\forall (uv:\mathbb{N}),\mathrm{heapEdge}uv⟺((u=0\wedge v=1)\vee (u=1\wedge v=0)\vee (2\le u\wedge \mathrm{Nat}.\mathrm{div}u2=v)\vee (2\le v\wedge \mathrm{Nat}.\mathrm{div}v2=u))$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.heapEdge (✓ std3).

Source. Repository-derived.

Commentary.

The anchor edge joins zero to one, and every other edge joins a positive vertex to its binary-heap parent.

Definition 1.4 (meanEnergy).

$$\forall (n:\mathbb{N}),\mathrm{meanEnergy}n=(\sum _{v:\mathrm{Fin}(n+2)}(\mathrm{energy}v.\mathrm{val}:\mathbb{C}))/(n+2:\mathbb{C})$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.meanEnergy (✓ std3).

Source. Repository-derived.

Commentary.

Subtracting the mean makes the diagonal trace zero.

Definition 1.5 (centeredEnergy).

$$\forall (n:\mathbb{N})(v:\mathrm{Fin}(n+2)),\mathrm{centeredEnergy}nv=(\mathrm{energy}v.\mathrm{val}:\mathbb{C})-\mathrm{meanEnergy}n$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.centeredEnergy (✓ std3).

Source. Repository-derived.

Commentary.

These centered complex entries are real-valued.

Definition 1.6 (A).

$$\forall (n:\mathbb{N}),An=\mathrm{Matrix}.\mathrm{diagonal}(\mathrm{centeredEnergy}n)$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.A (✓ std3).

Source. Repository-derived.

Commentary.

The first Hermitian generator is the centered energy diagonal.

Definition 1.7 (B).

$$\forall (n:\mathbb{N}),Bn=(\mathrm{SimpleGraph}.\mathrm{fromRel}(\mathrm{fun}(ij:\mathrm{Fin}(n+2))\mapsto \mathrm{heapEdge}i.\mathrm{val}j.\mathrm{val})).\mathrm{adjMatrix}\mathbb{C}$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.B (✓ std3).

Source. Repository-derived.

Commentary.

The second Hermitian generator is the symmetric adjacency matrix of the anchored heap.

Definition 1.8 (gen).

$$\forall (n:\mathbb{N}),\mathrm{gen}n=![An,Bn]$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.gen (✓ std3).

Source. Repository-derived.

Commentary.

The two-entry vector lists the diagonal and adjacency generators.

Definition 1.9 (iGen).

$$\forall (n:\mathbb{N})(i:\mathrm{Fin}2),\mathrm{iGen}ni=\mathrm{HSMul}.\mathrm{hSMul}\mathrm{Complex}.I(\mathrm{gen}ni)$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.iGen (✓ std3).

Source. Repository-derived.

Commentary.

Multiplication by the complex imaginary unit gives traceless skew-Hermitian generators.

Theorem 1.10 (anchored_units_mem).

$$\forall (n:\mathbb{N})(v:\mathrm{Fin}(n+2)),1\le v.\mathrm{val}\to (\mathrm{Matrix}.\mathrm{single}v0(1:\mathbb{C})\in \mathrm{rightSpan}(K:=\mathbb{C})(\mathrm{gen}n)(8\ast \mathrm{Nat}.\mathrm{size}v.\mathrm{val})\wedge \mathrm{Matrix}.\mathrm{single}0v(1:\mathbb{C})\in \mathrm{rightSpan}(K:=\mathbb{C})(\mathrm{gen}n)(8\ast \mathrm{Nat}.\mathrm{size}v.\mathrm{val}))$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/GenericLieLengthConstruction.anchored_units_mem (✓ std3). ∎

Source. Repository-derived.

Commentary.

Degree-seven Lagrange polynomials in the diagonal adjoint select gaps from {−7,−3,−2,−1,1,2,3,7}. The anchor units then propagate to both children in eight additional letters per level. Nat.size is the binary length, zero at zero and 1 + Nat.log 2 v for positive v.

Definition 1.11 (suLieRing).

$$\forall (n:\mathbb{N}),\mathrm{suLieRing}n=\mathrm{inferInstanceAs}(\mathrm{LieRing}(\mathrm{suLie}n))$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.suLieRing (✓ std3).

Source. Repository-derived.

Commentary.

The Lie-ring structure on the real submodule is the one on the corresponding Lie subalgebra.

Definition 1.12 (suLieAlgebra).

$$\forall (n:\mathbb{N}),\mathrm{suLieAlgebra}n=\mathrm{inferInstanceAs}(\mathrm{LieAlgebra}\mathbb{R}(\mathrm{suLie}n))$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.suLieAlgebra (✓ std3).

Source. Repository-derived.

Commentary.

The real Lie-algebra structure is inherited from the same Lie subalgebra.

Definition 1.13 (compactPair).

$$\forall (n:\mathbb{N})(i:\mathrm{Fin}2),(compactPairni:\mathrm{Matrix}(\mathrm{Fin}(n+2))(\mathrm{Fin}(n+2))\mathbb{C})=\mathrm{iGen}ni$$

Formalization. D5/S3/Quantum/Algebra/GenericLieLengthConstruction.compactPair (✓ std3).

Source. Repository-derived.

Commentary.

compactPair has type Fin 2 → suSet (n + 2), with value iGen n i. Its subtype property is exactly traceless skew-Hermiticity.

Theorem 1.14 (rightSpan_map).

$$\forall (IKMN:\mathrm{Type}\ast )[\mathrm{CommRing}K][\mathrm{LieRing}M][\mathrm{LieAlgebra}KM][\mathrm{LieRing}N][\mathrm{LieAlgebra}KN](f:\mathrm{LieHom}KMN)(S:I\to M)(L:\mathbb{N}),\mathrm{Submodule}.\mathrm{map}f.\mathrm{toLinearMap}(\mathrm{rightSpan}(K:=K)SL)=\mathrm{rightSpan}(K:=K)(\mathrm{fun}(i:I)\mapsto f(Si))L$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/GenericLieLengthConstruction.rightSpan_map (✓ std3). ∎

Source. Repository-derived.

Commentary.

A Lie homomorphism commutes with every word evaluation and hence with its span.

Theorem 1.15 (compactPair_span_top).

$$\forall (n:\mathbb{N}),\mathrm{rightSpan}(K:=\mathbb{R})(\mathrm{compactPair}n)(16\ast (1+\mathrm{Nat}.\log 2(n+1)))=\mathrm{Top}.\mathrm{top}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Algebra/GenericLieLengthConstruction.compactPair_span_top (✓ std3). ∎

Source. Repository-derived.

Commentary.

Bracketing the anchored matrix units gives all adjusted units, which span the trace kernel. Scaling by the imaginary unit and taking skew-adjoint parts gives the whole real subalgebra.

References

• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.A
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.B
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.anchored_units_mem
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.centeredEnergy
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.compactPair
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.compactPair_span_top
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.energy
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.gen
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.heapColor
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.heapEdge
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.iGen
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.meanEnergy
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.rightSpan_map
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.suLieAlgebra
• Truth anchor: D5/S3/Quantum/Algebra/GenericLieLengthConstruction.suLieRing
• Dependency: D5/S3/Quantum/Algebra/GenericLieLengthFiltration