module module

`IndisputableMonolith.Gravity.SevenGaps.StrainDynamicsKernelReach`

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 (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.FunctionalEquation module_import
IndisputableMonolith.Cost.SymplecticAction module_import
IndisputableMonolith.Gravity.SevenGaps.DescentPrincipleUniversality module_import

declarations in this module (17)

structure KernelCostContent L103
theorem jcost_kernelCostContent L111
def reciprocalInvolution L146
theorem reciprocalInvolution_continuous L148
theorem reciprocalInvolution_preserves_cost L153
theorem reciprocalInvolution_iterate_even L159
theorem reciprocalInvolution_never_reaches L172
theorem kernel_cost_content_does_not_entail_cost_spending L189
theorem no_kernel_derivation_of_residue L209
structure CostSpendingSubstrate L230
theorem costSpendingSubstrate_nonempty L245
def collapseStep L257
def halfwayStep L260
def collapse_substrate L262
def halfway_substrate L269
theorem residue_has_two_models L288
theorem no_unique_dynamics_from_residue L299