FPRD state-conditioned height theorem — audit and repository packet

Prepared: 28 July 2026
Status: independently audited and lead-lane verified at repository commit ba233faf
Novelty status: not assessed; no novelty claim
Intended recipient: FPRD repository lead lane

Requested repository action

Independently verify the theorem below against the repository’s exact normalization conventions. If it survives, record it as a state-conditioned raw/canonical height theorem with the stated scope.

Do not merge it with the pending fixed-target, cycle-dual, or gauge-reduced witnesses. Those are undergoing separate audits.

Definitions

Let $M$ be a trim deterministic sequential integer-weighted machine with:

• state set $Q$, $|Q|=m$;
• initial state $q_0$ and initial weight $\iota$;
• integer transition weights $w(e)$;
• integer final weights $\tau(q)$.

Let $h(M)$ be the maximum absolute value of its finite initial, transition, and final weights.

Let $T$ be the repository’s weight-blind BFS access tree, using the pinned letter order. Write $D$ for its depth and $W_T(q)$ for the original weight accumulated along the unique tree access path to $q$.

After BFS normalization and absorption of the initial weight, every non-tree transition $e:p\to q$ has canonical weight

$$w^{\mathrm{can}}(e) = W_T(p)+w(e)-W_T(q), \tag{1}$$

and every final state has canonical final weight

$$\tau^{\mathrm{can}}(q) = \iota+W_T(q)+\tau(q). \tag{2}$$

The displayed potential convention may have the opposite sign from the repository’s literal apply_gauge; the formulas are identical after $z\mapsto-z$.

For a non-tree edge $e:p\to q$, define

$$\ell_T(e) = 1+d_T(p)+d_T(q) -2d_T(\operatorname{lca}_T(p,q)). \tag{3}$$

This is the number of weighted coordinates remaining after the common root-to-LCA parts of the two access paths cancel.

Theorem 1 — fixed-presentation bound

$$\boxed{ H(M) \le \max\left\{ D+2,\ \max_{e\notin T}\ell_T(e) \right\}h(M) \le (m+1)h(M). } \tag{4}$$

Proof

Equation (1) contains the transition weight $w(e)$ and the signed access weights on the tree path between $p$ and $q$. Their common root-to-LCA segment cancels, so

$$|w^{\mathrm{can}}(e)|\le\ell_T(e)h(M).$$

The union of the two post-LCA branches contains at most $m-1$ tree edges; hence $\ell_T(e)\le m$.

Equation (2) contains at most $D$ tree-transition weights plus one initial and one final weight, so

$$|\tau^{\mathrm{can}}(q)|\le(D+2)h(M)\le(m+1)h(M).$$

Tree transitions and the absorbed initial weight are zero. This proves (4).

Trimming preserves the complete partial series, including undefinedness caused by a missing transition or a nonfinal endpoint.

Theorem 2 — state-conditioned target bound

For target $f$, horizon $N$, and state budget $n$, define

$$h_{f,\le n}(N) = \min\{h(M):M\text{ is \(N\)-correct for }f,\ |Q_M|\le n\},$$

$$H_{f,\le n}(N) = \min\{H(M):M\text{ is \(N\)-correct for }f,\ |Q_M|\le n\}.$$

If the section is feasible, then

$$\boxed{ h_{f,\le n}(N) \le H_{f,\le n}(N) \le (n+1)h_{f,\le n}(N). } \tag{5}$$

This first inequality is not the pointwise assertion $h(M)\le H(M)$. That assertion is false: a one-state machine with initial weight $5$, loop weight $0$, and final weight $-5$ has raw height $5$ and canonical height $0$. Equation (5) holds only after minimizing, because the canonical form of any competitor is itself a raw presentation in the same state-budget section.

Proof

The canonical form of any correct machine is another correct raw presentation with no additional states, so minimizing gives the first inequality.

For the second inequality, choose a raw-height minimizer, trim its live core, and apply Theorem 1. Integer heights ensure the minimum is attained.

Theorem 3 — optimality after target-level minimization

For every $n\ge1$, use the unary alphabet, horizon $N=n-1$, and target

$$f_n(a^j)= \begin{cases} n+1,&j=n-1,\\ -\infty,&0\le j<n-1. \end{cases} \tag{6}$$

Then

$$\boxed{ h_{f_n,\le n}(n-1)=1, \qquad H_{f_n,\le n}(n-1)=n+1. } \tag{7}$$

Proof

An $n$-state path with initial weight $1$, every transition weight $1$, and final weight $1$ realizes the horizon target, so raw height is at most $1$. A nonzero integer output rules out height $0$.

Every correct unary presentation must visit $n$ distinct states at times $0,\ldots,n-1$. If $q_i=q_j$ for $i<j$, determinism makes an earlier word reach the final state reached at time $n-1$, contradicting undefinedness. Thus any presentation with at most $n$ states uses the forced access path. BFS normalization zeros that path and leaves the final coordinate $n+1$.

For $n=1$, use the empty-word target of value $2$.

Consequence and safe interpretation

Whenever the constrained raw height is positive,

$$\boxed{ n \ge \frac{H_{f,\le n}(N)}{h_{f,\le n}(N)}-1. } \tag{8}$$

An unbounded raw/canonical ratio therefore cannot occur inside one fixed state-budget section.

This is an optimal worst-case coupling envelope. It does not establish:

• an exact conservation law;
• that canonical height has no independent content;
• a semantic characterization of canonical excess;
• invariance under the global length-and-constant repair;
• novelty relative to weight pushing or transducer normalization.

Independent checks requested

All six checks below were completed by the lead lane before commit ba233faf:

1. Equations (1)–(2) match the repository normalization after the stated sign reversal.
2. Initial and final weight accounting is correct and load-bearing.
3. Trim/dead-machine behavior and both kinds of undefinedness were checked.
4. The unary sharpness proof was independently reconstructed.
5. The result was recorded as a constrained Pareto-section theorem.
6. The no-novelty scope was preserved.