module module

`IndisputableMonolith.Gravity.Analysis.Q3PatchSeating`

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

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Gravity.Analysis.OrderSensitiveHistoryResponse4D module_import
IndisputableMonolith.Gravity.Analysis.Q3PatchSeatingAudit module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Patterns module_import

declarations in this module (18)

def bitNat L26
theorem bitNat_le_one L30
def seatNat L33
theorem seatNat_lt L36
def seat L44
def unseat L47
def flipTime L54
theorem seat_unseat L59
theorem pack4_testBit L65
theorem unseat_seat L71
theorem seat_injective L82
theorem seat_surjective L87
theorem seat_bijective L91
theorem xor8_lt_eight L100
theorem xor8_add_eight L103
theorem seat_flipTime L106
theorem flipTime_involutive L122
theorem timeSlice_is_patch_symmetry L127