module module

`IndisputableMonolith.Foundation.HamiltonianEmergenceOperator`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.HamiltonianEmergence module_import

declarations in this module (15)

theorem for L11
def Hc L56
theorem Hc_isHermitian L60
def gen L70
theorem gen_skewHermitian L75
def U L88
theorem U_zero L92
theorem U_add L97
theorem U_conjTranspose L107
theorem U_unitary L116
theorem U_mem_unitaryGroup L123
theorem step_eq_firstOrder L134
structure StoneGeneratorCert L163
theorem stoneGeneratorCert L174
theorem operator_level_hamiltonian_emergence L187