Weighted-tree cycle row error and sharp constant one

Abstract

Actual rows of a positively weighted finite tree cannot uniformly approximate a positive bidirectional simple cycle below its least directed rate; endpoint folding attains the bound for every cycle size.

Definition 1.1 (Original positive tree data).

$$\forall V\in \mathrm{Type},\mathrm{TreeData}\left(V\right):\mathrm{Type}$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.TreeData (✓ std3).

Source. Repository-derived.

Commentary.

TreeData consists of an actual simple tree, positive real mass at each original vertex, symmetric conductances positive on every edge, and arbitrary nonnegative killing. Conductance values off edges are unused. The theorem concerns finite carriers; connectedness supplies nonemptiness. Fibres need not be connected.

Definition 1.2 (Killed coarse generators).

$$\forall B\in \mathrm{Type},\mathrm{KilledGenerator}\left(B\right):\mathrm{Type}$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.KilledGenerator (✓ std3).

Source. Repository-derived.

Commentary.

A killed generator stores arbitrary nonnegative off-diagonal rates and nonnegative killing. Its diagonal rate field has no effect on its action, since it multiplies a zero difference.

Definition 1.3 (The original backward generator).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall T\in \mathrm{TreeData}\left(V\right),\forall f\in V\to \mathrm{Real},\forall x\in V,\mathrm{generator}\left(T,f,x\right)=\sum _{y\in V}\mathrm{ite}\left(\mathrm{Adj}\left(\mathrm{graph}\left(T\right),x,y\right),\frac{\mathrm{conductance}\left(T,x,y\right)}{\mathrm{mass}\left(T,x\right)}\cdot \left(f\left(y\right)-f\left(x\right)\right),0\right)-\mathrm{killing}\left(T,x\right)\cdot f\left(x\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.generator (✓ std3).

Source. Repository-derived.

Commentary.

Only actual neighbours contribute. Division is by the original vertex mass, with no time rescaling; killing is subtracted in the same clock.

Definition 1.4 (Actual off-label row sums).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall T\in \mathrm{TreeData}\left(V\right),\forall p\in V\to B,\forall x\in V,\forall b\in B,\mathrm{labelRate}\left(T,p,x,b\right)=\sum _{y\in V}\mathrm{ite}\left(\mathrm{Adj}\left(\mathrm{graph}\left(T\right),x,y\right)\wedge p\left(y\right)=b,\frac{\mathrm{conductance}\left(T,x,y\right)}{\mathrm{mass}\left(T,x\right)},0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.labelRate (✓ std3).

Source. Repository-derived.

Commentary.

The sum runs over every original vertex, retaining exactly actual neighbours with the requested label. No quotient-edge multiplicity or displayed proxy matrix replaces these rows.

Definition 1.5 (Uniform off-label error).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall T\in \mathrm{TreeData}\left(V\right),\forall p\in V\to B,\forall Q\in \mathrm{KilledGenerator}\left(B\right),\mathrm{delta}\left(T,p,Q\right)=\underset{x\in V,b\in B}{\max }\mathrm{ite}\left(b\ne p\left(x\right),|\mathrm{labelRate}\left(T,p,x,b\right)-\mathrm{rate}\left(Q,p\left(x\right),b\right)|,0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.delta (✓ std3).

Source. Repository-derived.

Commentary.

The finite maximum contains every original vertex row. Same-label entries are assigned zero; the nonnegative finite supremum has bottom zero, so an empty off-label maximum is zero.

Definition 1.6 (Induced masses).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall T\in \mathrm{TreeData}\left(V\right),\forall p\in V\to B,\forall a\in B,\mathrm{inducedMass}\left(T,p,a\right)=\sum _{x\in V}\mathrm{ite}\left(p\left(x\right)=a,\mathrm{mass}\left(T,x\right),0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.inducedMass (✓ std3).

Source. Repository-derived.

Commentary.

Each label mass is the sum of the original positive masses in its fibre.

Definition 1.7 (Induced conductances).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall T\in \mathrm{TreeData}\left(V\right),\forall p\in V\to B,\forall a\in B,\forall b\in B,\mathrm{inducedConductance}\left(T,p,a,b\right)=\sum _{x\in V}\mathrm{ite}\left(p\left(x\right)=a,\sum _{y\in V}\mathrm{ite}\left(\mathrm{Adj}\left(\mathrm{graph}\left(T\right),x,y\right)\wedge p\left(y\right)=b,\mathrm{conductance}\left(T,x,y\right),0\right),0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.inducedConductance (✓ std3).

Source. Repository-derived.

Commentary.

Actual conductances are summed over ordered edges from the first class to the second. No missing edge is inserted.

Definition 1.8 (Literal mass-weighted compression).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall T\in \mathrm{TreeData}\left(V\right),\forall p\in V\to B,\left(\forall a\in B,\forall b\in B,\mathrm{rate}\left(\mathrm{compression}\left(T,p\right),a,b\right)=\frac{{\sum }_{x\in V}\mathrm{ite}\left(p\left(x\right)=a,\mathrm{mass}\left(T,x\right)\cdot \mathrm{labelRate}\left(T,p,x,b\right),0\right)}{\mathrm{inducedMass}\left(T,p,a\right)}\right)\wedge \left(\forall a\in B,\mathrm{killing}\left(\mathrm{compression}\left(T,p\right),a\right)=\frac{{\sum }_{x\in V}\mathrm{ite}\left(p\left(x\right)=a,\mathrm{mass}\left(T,x\right)\cdot \mathrm{killing}\left(T,x\right),0\right)}{\mathrm{inducedMass}\left(T,p,a\right)}\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.compression (✓ std3).

Source. Repository-derived.

Commentary.

Rates average the actual original row sums with original masses; killing is averaged with the same masses. The generator action identity in the sharpness theorem proves that this is the literal compression of G on pulled-back label functions. Empty fibres are permitted in the definition; all theorem label maps are onto.

Definition 1.9 (Coarse backward action).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall Q\in \mathrm{KilledGenerator}\left(B\right),\forall f\in B\to \mathrm{Real},\forall a\in B,\mathrm{coarseAction}\left(Q,f,a\right)=\sum _{b\in B}\mathrm{rate}\left(Q,a,b\right)\cdot \left(f\left(b\right)-f\left(a\right)\right)-\mathrm{killing}\left(Q,a\right)\cdot f\left(a\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.coarseAction (✓ std3).

Source. Repository-derived.

Commentary.

Diagonal rates cancel. This action includes the complete killed diagonal through the rate differences and killing term.

Definition 1.10 (Original mass average).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall T\in \mathrm{TreeData}\left(V\right),\forall p\in V\to B,\forall g\in V\to \mathrm{Real},\forall a\in B,\mathrm{massAverage}\left(T,p,g,a\right)=\frac{{\sum }_{x\in V}\mathrm{ite}\left(p\left(x\right)=a,\mathrm{mass}\left(T,x\right)\cdot g\left(x\right),0\right)}{\mathrm{inducedMass}\left(T,p,a\right)}$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.massAverage (✓ std3).

Source. Repository-derived.

Commentary.

This is the original-mass average of a vertex function on a label class.

Definition 1.11 (Every direction of a full simple cycle).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall Q\in \mathrm{KilledGenerator}\left(B\right),\forall eta\in \mathrm{Real},\mathrm{CycleRates}\left(Q,eta\right)\iff \left(\exists n\in \mathrm{Nat},\exists i\in \mathrm{Fin}\left(n+3\right)\to B,\mathrm{Injective}\left(i\right)\wedge \left(\forall a\in \mathrm{Fin}\left(n+3\right),\forall b\in \mathrm{Fin}\left(n+3\right),\mathrm{Adj}\left(\mathrm{cycleGraph}\left(n+3\right),a,b\right)\Rightarrow eta\le \mathrm{rate}\left(Q,i\left(a\right),i\left(b\right)\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.CycleRates (✓ std3).

Source. Repository-derived.

Commentary.

An injective cyclic list has length n+3, hence at least three. Both ordered directions of every cycle edge satisfy the lower bound, while all other labels and rates remain arbitrary.

Theorem 1.12 (A finite nonempty forest has a vertex with at most one neighbor).

Lean statement: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.forest_not_two_neighbors

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

Source. Repository-derived.

Commentary.

For every type W with Finite and Nonempty, every simple graph G on W and every proof that G is acyclic, it is false that every vertex x has two distinct neighbors y,z. There is no connectedness assumption. The connected component of any vertex is a finite tree; if all vertices had two distinct neighbors, its degree-one vertex would give a contradiction. The same statement supplies isolated-or-leaf reduction for native independence realizations of forests.

Theorem 1.13 (Universal actual-tree lower bound).

$$\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall T\in \mathrm{TreeData}\left(V\right),\forall p\in V\to B,\mathrm{Surjective}\left(p\right)\Rightarrow \left(\forall Q\in \mathrm{KilledGenerator}\left(B\right),\forall eta\in \mathrm{Real},\left(0<eta\wedge \mathrm{CycleRates}\left(Q,eta\right)\right)\Rightarrow eta\le \mathrm{delta}\left(T,p,Q\right)\right)$$

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

Source. Repository-derived.

Commentary.

Restrict the original tree to vertices carrying cycle labels. If every such vertex had a neighbour of each adjacent cycle label, cycle degree two and injectivity would give two distinct actual neighbours at every vertex of this induced forest. A finite nonempty forest component has a leaf, a contradiction. Thus an actual original row misses an adjacent cycle class, has row sum zero there, and differs from its specified coarse rate by at least eta. No missing-neighbour hypothesis, connected-fibre hypothesis, diagonal condition or killing equality is assumed.

Definition 1.14 (The entire sharp path family).

$$\forall k\in \mathrm{Nat},\forall eta\in \mathrm{Real},\forall he\in 0<eta,\mathrm{graph}\left(\mathrm{sharpPath}\left(k,eta\right)\right)=\mathrm{pathGraph}\left(k+1\right)\wedge \left(\forall x\in \mathrm{Fin}\left(k+1\right),\mathrm{mass}\left(\mathrm{sharpPath}\left(k,eta\right),x\right)=1\wedge \left(\mathrm{killing}\left(\mathrm{sharpPath}\left(k,eta\right),x\right)=0\wedge \left(\forall y\in \mathrm{Fin}\left(k+1\right),\mathrm{conductance}\left(\mathrm{sharpPath}\left(k,eta\right),x,y\right)=2\cdot eta\right)\right)\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.sharpPath (✓ std3).

Source. Repository-derived.

Commentary.

There are k+1 original vertices and k edges. Every original mass is one, every edge conductance is 2 eta, and killing vanishes. Positivity follows for every real eta>0.

Definition 1.15 (Endpoint-folding labels).

$$\forall k\in \mathrm{Nat},\forall hk\in 0<k,\forall x\in \mathrm{Fin}\left(k+1\right),\mathrm{endpointFold}\left(k\right)\left(x\right)=\mathrm{ite}\left(\mathrm{val}\left(x\right)<k,\mathrm{val}\left(x\right),0\right)$$

Formalization. D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.endpointFold (✓ std3).

Source. Repository-derived.

Commentary.

Vertices zero through k-1 retain their indices; vertex k receives label zero. The zero fibre consists of the two endpoints and is disconnected for k>=3.

Theorem 1.16 (All sizes and scales attain the bound).

$$\forall k\in \mathrm{Nat},\forall hk\in 3\le k,\forall eta\in \mathrm{Real},\forall he\in 0<eta,\mathrm{Surjective}\left(\mathrm{endpointFold}\left(k\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\mathrm{inducedMass}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),a\right)=\mathrm{ite}\left(a=0,2,1\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\forall b\in \mathrm{Fin}\left(k\right),\mathrm{inducedConductance}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),a,b\right)=\mathrm{ite}\left(\mathrm{Adj}\left(\mathrm{cycleGraph}\left(k\right),a,b\right),2\cdot eta,0\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\forall b\in \mathrm{Fin}\left(k\right),\mathrm{rate}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),a,b\right)=\mathrm{ite}\left(\mathrm{Adj}\left(\mathrm{cycleGraph}\left(k\right),a,b\right),\mathrm{ite}\left(a=0,eta,2\cdot eta\right),0\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\mathrm{killing}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),a\right)=0\right)\wedge \left(\mathrm{CycleRates}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),eta\right)\wedge \left(\left(\exists a\in \mathrm{Fin}\left(k\right),\exists b\in \mathrm{Fin}\left(k\right),\mathrm{Adj}\left(\mathrm{cycleGraph}\left(k\right),a,b\right)\wedge \mathrm{rate}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),a,b\right)=eta\right)\wedge \left(\left(\forall x\in \mathrm{Fin}\left(k+1\right),\forall b\in \mathrm{Fin}\left(k\right),|\mathrm{labelRate}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),x,b\right)-\mathrm{rate}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),\mathrm{endpointFold}\left(k\right)\left(x\right),b\right)|\le eta\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\forall b\in \mathrm{Fin}\left(k\right),a\ne 0\Rightarrow \mathrm{labelRate}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),\mathrm{castSucc}\left(a\right),b\right)=\mathrm{rate}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),a,b\right)\right)\wedge \left(\left(\forall b\in \mathrm{Fin}\left(k\right),\mathrm{labelRate}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),0,b\right)=\mathrm{ite}\left(\mathrm{val}\left(b\right)=1,2\cdot eta,0\right)\right)\wedge \left(\left(\forall b\in \mathrm{Fin}\left(k\right),\mathrm{labelRate}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),\mathrm{last}\left(k\right),b\right)=\mathrm{ite}\left(\mathrm{val}\left(b\right)+1=k,2\cdot eta,0\right)\right)\wedge \left(\left(\forall f\in \mathrm{Fin}\left(k\right)\to \mathrm{Real},\forall a\in \mathrm{Fin}\left(k\right),\mathrm{coarseAction}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),f,a\right)=\mathrm{massAverage}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),\mathrm{generator}\left(\mathrm{sharpPath}\left(k,eta\right),f\circ \mathrm{endpointFold}\left(k\right)\right),a\right)\right)\wedge \mathrm{delta}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right)\right)=eta\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For each integer k>=3 and real eta>0, the indicated literal compression has mass two at zero and one elsewhere, conductance 2 eta on every cycle edge, rate eta out of zero and 2 eta out of every other label. Every directed cycle rate is at least eta and a rate out of zero equals eta. Every internal original row agrees with Q. At the first endpoint the only nonzero row entry is 2 eta toward label one; at the last it is 2 eta toward label k-1. Both endpoint errors are bounded by eta, as are all rows, and the universal lower bound gives exact delta=eta. The full operator compression identity is included. This establishes sharpness in the unrestricted weighted-tree comparison class; it makes no fixed native orbit, native-operation, physical-space, or arbitrary memory/encoding assertion.

Theorem 1.17 (The complete cycle obstruction and optimal constant).

$$\left(\forall V\in \mathrm{Type},\forall B\in \mathrm{Type},[\mathrm{Fintype}\left(V\right)][\mathrm{Fintype}\left(B\right)]\forall T\in \mathrm{TreeData}\left(V\right),\forall p\in V\to B,\mathrm{Surjective}\left(p\right)\Rightarrow \left(\forall Q\in \mathrm{KilledGenerator}\left(B\right),\forall eta\in \mathrm{Real},\left(0<eta\wedge \mathrm{CycleRates}\left(Q,eta\right)\right)\Rightarrow eta\le \mathrm{delta}\left(T,p,Q\right)\right)\right)\wedge \left(\forall k\in \mathrm{Nat},\forall hk\in 3\le k,\forall eta\in \mathrm{Real},\forall he\in 0<eta,\mathrm{Surjective}\left(\mathrm{endpointFold}\left(k\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\mathrm{inducedMass}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),a\right)=\mathrm{ite}\left(a=0,2,1\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\forall b\in \mathrm{Fin}\left(k\right),\mathrm{inducedConductance}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),a,b\right)=\mathrm{ite}\left(\mathrm{Adj}\left(\mathrm{cycleGraph}\left(k\right),a,b\right),2\cdot eta,0\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\forall b\in \mathrm{Fin}\left(k\right),\mathrm{rate}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),a,b\right)=\mathrm{ite}\left(\mathrm{Adj}\left(\mathrm{cycleGraph}\left(k\right),a,b\right),\mathrm{ite}\left(a=0,eta,2\cdot eta\right),0\right)\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\mathrm{killing}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),a\right)=0\right)\wedge \left(\mathrm{CycleRates}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),eta\right)\wedge \left(\left(\exists a\in \mathrm{Fin}\left(k\right),\exists b\in \mathrm{Fin}\left(k\right),\mathrm{Adj}\left(\mathrm{cycleGraph}\left(k\right),a,b\right)\wedge \mathrm{rate}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),a,b\right)=eta\right)\wedge \left(\left(\forall x\in \mathrm{Fin}\left(k+1\right),\forall b\in \mathrm{Fin}\left(k\right),|\mathrm{labelRate}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),x,b\right)-\mathrm{rate}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),\mathrm{endpointFold}\left(k\right)\left(x\right),b\right)|\le eta\right)\wedge \left(\left(\forall a\in \mathrm{Fin}\left(k\right),\forall b\in \mathrm{Fin}\left(k\right),a\ne 0\Rightarrow \mathrm{labelRate}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),\mathrm{castSucc}\left(a\right),b\right)=\mathrm{rate}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),a,b\right)\right)\wedge \left(\left(\forall b\in \mathrm{Fin}\left(k\right),\mathrm{labelRate}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),0,b\right)=\mathrm{ite}\left(\mathrm{val}\left(b\right)=1,2\cdot eta,0\right)\right)\wedge \left(\left(\forall b\in \mathrm{Fin}\left(k\right),\mathrm{labelRate}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),\mathrm{last}\left(k\right),b\right)=\mathrm{ite}\left(\mathrm{val}\left(b\right)+1=k,2\cdot eta,0\right)\right)\wedge \left(\left(\forall f\in \mathrm{Fin}\left(k\right)\to \mathrm{Real},\forall a\in \mathrm{Fin}\left(k\right),\mathrm{coarseAction}\left(\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right),f,a\right)=\mathrm{massAverage}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),\mathrm{generator}\left(\mathrm{sharpPath}\left(k,eta\right),f\circ \mathrm{endpointFold}\left(k\right)\right),a\right)\right)\wedge \mathrm{delta}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right),\mathrm{compression}\left(\mathrm{sharpPath}\left(k,eta\right),\mathrm{endpointFold}\left(k\right)\right)\right)=eta\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The complete statement combines the universal lower bound with the full endpoint-folding construction for every k>=3 and every eta>0. Both clauses use the same original generator, actual row norm, masses and clock described above.

References

• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.CycleRates
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.KilledGenerator
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.TreeData
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.coarseAction
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.compression
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.cycle_row_error_and_sharpness
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.cycle_row_error_lower_bound
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.delta
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.endpointFold
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.endpoint_folding_sharpness
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.forest_not_two_neighbors
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.generator
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.inducedConductance
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.inducedMass
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.labelRate
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.massAverage
• Truth anchor: D5/S3/Combinatorics/SpectralGraph/ScalarCycleRowError.sharpPath