module module

`IndisputableMonolith.Foundation.RecognitionForcing`

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

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

IndisputableMonolith.NumberTheory.ConcreteEulerLedger module_import

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.LawOfExistence module_import
IndisputableMonolith.Foundation.LedgerForcing module_import
IndisputableMonolith.Recognition module_import

declarations in this module (23)

def recognition_cost L21
theorem self_recognition_zero_cost L25
theorem nontrivial_recognition_positive_cost L33
theorem recognition_is_cost_structure L59
structure Observable L84
structure ObservableExtractionMechanism L87
structure RecognitionStructure L91
def recognition_from_extraction L96
theorem recognition_unique L104
structure Configuration L111
def config_to_recognition L115
theorem cost_minima_are_recognition L118
theorem global_minimum_is_self_recognition L122
structure JStableStructure L130
structure RecognitionLikeStructure L135
def stable_to_recognition L141
theorem stability_forces_recognition L148
theorem recognition_necessary L154
theorem recognition_forcing_complete L161
structure RecognitionTracker L182
def PreservesJSymmetry L185
theorem ledger_is_minimal_recognition_tracker L188
theorem cost_to_recognition_bridge L194