Axis Trace Definitions

Abstract

The partial sum ranges over words of bounded depth; the weight is the exponential.

The clause introduces two objects: the axis weight at a depth, read as an exponential at the two Galois embeddings, and the axis partial sum, the total weight of the legal words whose digit depth is at most that depth.

The implementation sums over an initial segment of the naturals rather than over a set described by depth. Those are the same family only because depth at most K is exactly membership below the next Fibonacci number. That equivalence is the third conjunct here: without it the bound in the definition would be an unexplained constant, and a reader could not check the implementation against the source line.

Theorem 1.1 (The two objects and the depth bridge).

$$t\left(K\right)=\exp \left(y\cdot {psi}^{K+1}-x\cdot {phi}^{K+1}\right)\wedge \left(W\left(K\right)=\mathrm{sum}\left(\mathrm{range}\left(\mathrm{fib}\left(K+1\right)\right),\mathrm{wordWeight}\left(n\right)\right)\wedge \left(\mathrm{greatestFib}\left(n\right)\le K\iff n<\mathrm{fib}\left(K+1\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Axis/AxisTraceDefinitions.axis_trace_definitions (✓ std3). ∎

Source. Repository-derived.

Commentary.

The first two conjuncts hold by definition and pin it: changing the exponent or the summation bound makes the module fail to build. The third is a proved equivalence rather than a restatement, and it is what makes the summation bound mean bounded depth.

References

• Truth anchor: D5/S3/Axis/AxisTraceDefinitions.axis_trace_definitions
• Dependency: D5/S3/Axis/AxisPartialSum