As of now, the assumptions for the upward closure for attacker winning budgets of #37 do not apply to the spectroscopy energy game. This connection must be established for the main theorem proof #63.
Ben's suggestion would be to make the assumptions about how energies work part of the energy game locale. Then, you'll have to establish that the energies of the spectroscopy game follow these rules once at some point and can use the rule more easily afterwards.
As of now, the assumptions for the upward closure for attacker winning budgets of #37 do not apply to the spectroscopy energy game. This connection must be established for the main theorem proof #63.
Ben's suggestion would be to make the assumptions about how energies work part of the energy game locale. Then, you'll have to establish that the energies of the spectroscopy game follow these rules once at some point and can use the rule more easily afterwards.