# The three-quarter exponent for honeycomb self-avoiding walk

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Polynomial vacuum representations and bridge mass for honeycomb walks](../../preprints/Polynomial-vacuum-representations-and-bridge-mass-for-honeycomb-walks-September-26-2026/main.pdf)
- [Renewal and changes of law for critical honeycomb walks](../../preprints/Renewal-and-changes-of-law-for-critical-honeycomb-walks-September-26-2026/main.pdf)
- [Critical strip-crossing mass on the honeycomb lattice](../../preprints/Critical-strip-crossing-mass-on-the-honeycomb-lattice-September-26-2026/main.pdf)
- [Critical honeycomb chords with prescribed boundary endpoints](../../preprints/Critical-honeycomb-chords-with-prescribed-boundary-endpoints-September-26-2026/main.pdf)

## Scope

The linked formalization establishes finiteness of the critical bridge measures used in the paper. For every strip height $h\ge1$, the total weight and first length moment of self-avoiding honeycomb bridges from a fixed initial port to a free terminal port are finite. The corresponding sums are also finite when the bridge is confined to the corridor of horizontal width $h(\log h)^2$, including the normalized first-moment sums.

These are supporting summability statements. The paper's $h^{4/3+o(1)}$ mean-length law and its central-visit and hexagonal-chord exponents are outside them.

The linked formalization proves existence of the infinite-length free energy for the critical honeycomb self-avoiding-walk partition function. For every starting vertex, force direction, and real force parameter, the logarithm of the length-$n$ partition function divided by $n$ converges to its stated free-energy limit.

This selected result supplies the limiting free energy. It does not state the paper's small-force exponent, near-critical correlation scale, or the $3/4$ spatial and moment laws.

For critical self-avoiding walks on the honeycomb lattice, the formalization proves that the total weight of paths crossing a strip of height $N$ is comparable to $N^{-1/4}$, while the first horizontal-displacement moment of return paths is comparable to $N^{3/4}$. It also proves finiteness of the strip sums, the exact arch–bridge balance identity, comparison of successive moment increments with bridge mass, and monotonicity of bridge mass. The comparison constants are uniform in the strip height.

For the prescribed-boundary-endpoint companion, let $B_h$ be the total critical weight of strict bridges crossing a strip of integral height $h$, from one fixed bottom port to all compatible top ports, with $B_0=1$. The formalization proves
$c(1+h)^{-1/4}\le B_h\le C(1+h)^{-1/4}$
for all $h\ge0$ and fixed positive constants $c,C$. This includes finiteness of the path sum. The prescribed-endpoint length law, arch and strip mean laws, and remaining moment and renewal conclusions are outside this supporting statement.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Finiteness of critical bridge mass and first length moments | [HoneycombBridgeFiniteness.lean](../ComparatorChallenges/HoneycombBridgeFiniteness.lean) |
| Existence of the honeycomb free-energy limit | [HoneycombFreeEnergy.lean](../ComparatorChallenges/HoneycombFreeEnergy.lean) |
| Critical honeycomb strip mass and displacement moment | [CriticalStripMass.lean](../ComparatorChallenges/CriticalStripMass.lean) |
| Strict honeycomb bridge mass of order $(1+h)^{-1/4}$ | [HoneycombBridgeMassSupport.lean](../ComparatorChallenges/HoneycombBridgeMassSupport.lean) |