Hofstadter sequences include the following two sequences. Set 
and 
.
For 
,
let 
be the least integer 
which can be expressed as the sum
of two or more consecutive already constructed terms. The resulting sequence
is 1, 2, 3, 5, 6, 8, 10, 11, 14, 16, ... (OEIS A005243).
Starting from 2 and 3, take the smallest set closed under
for distinct members 
and 
, and list its members in increasing order without repetition.
The resulting sequence is 2, 3, 5, 9, 14, 17, 26, 27,
... (OEIS A005244).
Another family, containing the Hofstadter G-sequence and Hofstadter H-sequence, is defined
for 
by 
and 
for 
.
Here 
and 
,
and the superscript denotes 
-fold iteration rather than exponentiation. Letouzey (2026)
proved 
whenever 
.
The proofs of this strict-ordering result and the non-strict
inequality for all 
are formalized in Rocq.
