Dear Klaas,
thank you for your comment! I'm glad you found something of interest in my essay.
Regarding the importance of free choice, indeed you can make an argument that one might be constrained to make only measurements for which f(n,k) yields a definite value, thus never running into the sorts of phenomena following from its indefiniteness. That we do, apparently, run into them would then be evidence that there is no such constraint (which of course doesn't entail that we have free choice).
However, one does not need to think about changing measurement conditions to derive the paradox, merely about the totality of all possible measurements on the system---whether they are ever performed or not. The index n is then essentially just an attempt to enumerate these measurements, with the argument then showing that no such enumeration can be complete.
As for superposition, you're right to point out that the structure of linear operators on Hilbert space is a quite specific one; but in the end, the project of deriving a theory from underlying principles is one to derive the specific from the general---for comparison, the structure of Lorentz transformations on Minkowski space is also quite specific, while following from the very general principle of relativity, together with the constancy of the speed of light.
Indeed, if one views Hilbert space as a concrete realization of an abstract propositional structure---the orthomodular lattice of its subspaces---then one can show that this essentially follows from the notion that there exists a maximum amount of information that can be extracted from any system (https://link.springer.com/article/10.1007/s10702-005-1129-0). This is both connected to undecidability (as in Chaitin's principle, you can't derive---under a suitable measure of complexity---a theorem more complex than the set of axioms), and superposition, with the failure of the distributive law in quantum logic.
For simple (that is, not subject to Gödelian phenomena) axiom systems, this correspondence was demonstrated by Brukner (https://link.springer.com/article/10.1007/s11047-009-9118-z) and Paterek et al (https://iopscience.iop.org/article/10.1088/1367-2630/12/1/013019/meta), who show an explicit way to encode axioms in a quantum system and demonstrate that a given measurement will produce random outcomes whenever the corresponding proposition is not derivable from the axioms. In a sense, my work is simply an extension of this to cases where undecidability is not due to the limitations of the axiom system, but to the inherent limitations imposed by the limitative theorems of metamathematics (although in the treatment using Lawvere's theorem, one can pass over first establishing a correspondence with formal axiomatic systems).
Having said that, I of course don't claim to have a complete reconstruction of quantum theory in hand. There are still different options possible---for instance, it's not easy to see why one should use Hilbert spaces over the complex field, and not over the reals or quaternions. In that sense, perhaps one should think of the connections I point out, as of yet, as 'family resemblances', rather than strict formal equivalences. I view them as enticing prospects that seem sufficiently promising for me to carry on exploring this point of view; but I would not be the first wanderer to be deceived by tantalizing lights in the dark forest.
Cheers
Jochen