Depends on one-time signature correctness, the Merkle path lemma, and signing landing first.
The headline theorem for this tree: a signature this specification produces is one this specification accepts.
key generation gives (sk, pk), signing at an in-range epoch gives a signature
=> verification of that signature returns true
The proof is an assembly rather than new work. Signing only succeeds once it has found a randomizer whose encoding is admissible, and the verifier recomputes the encoding from the same public parameter, message, randomizer and epoch, so both see the same 42 digits. One-time signature correctness then makes the recovered chain values the honest ones, so the recomputed leaf is the honest leaf, and the Merkle path lemma carries that leaf to the honest root.
This is the theorem worth naming in the README once it lands.
Depends on one-time signature correctness, the Merkle path lemma, and signing landing first.
The headline theorem for this tree: a signature this specification produces is one this specification accepts.
The proof is an assembly rather than new work. Signing only succeeds once it has found a randomizer whose encoding is admissible, and the verifier recomputes the encoding from the same public parameter, message, randomizer and epoch, so both see the same 42 digits. One-time signature correctness then makes the recovered chain values the honest ones, so the recomputed leaf is the honest leaf, and the Merkle path lemma carries that leaf to the honest root.
This is the theorem worth naming in the README once it lands.