feat(machines): the tables of explicit block-counting networks on numbers (#1833 H3) - #1909

Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/

`Turing.MultiTapePTM.explicitVerticesNum` and `Turing.MultiTapePTM.explicitBlockNetwork` (Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork.lean:252) share a 167-node subterm, 65% of the smaller body, built from `Turing.MultiTapePTM.letterBits`. Advisory only; see the job summary.

`Turing.MultiTapePTM.blockIndexNum` and `Turing.MultiTapePTM.scheduleOfNat` (Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/Graph.lean:109) share a 251-node subterm, 48% of the smaller body, built from `Equiv`, `Equiv.symm`, `finSuccEquiv`. Advisory only; see the job summary.

`Turing.MultiTapePTM.decodeControlData` and `Turing.MultiTapePTM.scheduleOfNat` (Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/Graph.lean:109) share a 251-node subterm, 48% of the smaller body, built from `Equiv`, `Equiv.symm`, `finSuccEquiv`. Advisory only; see the job summary.

`Turing.MultiTapePTM.blockMoveNum` and `Turing.MultiTapePTM.scheduleOfNat` (Complexity/Computability/Machines/Turing/MultiTape/Probabilistic/ExplicitBlockNetwork/Graph.lean:109) share a 265-node subterm, 52% of the smaller body, built from `Equiv`, `Equiv.symm`, `finSuccEquiv`. Advisory only; see the job summary.