module module

`IndisputableMonolith.Foundation.RecognitionSignatureGauge`

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.RecognitionCore module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientSelection module_import

declarations in this module (20)

def SameRecognitionSignature L41
theorem signature_forced_quotient_iff L46
theorem signature_observable_descends L52
theorem signature_projection_injective_of_separating L58
structure RecognitionSignatureGaugeCertificate L66
theorem recognitionSignatureGaugeCertificate_holds L76
def ScalarCostCompleteFor L87
theorem scalar_cost_kernel_eq_signature_of_complete L93
abbrev PairBoolState L103
def firstBit L106
def secondBit L109
def firstBitFamily L112
def pairBitFamily L115
theorem one_boolean_coordinate_not_complete L120
def firstBitScalarCost L132
theorem first_bit_scalar_cost_not_complete L137
theorem pairBitFamily_separating L144
theorem pairBitFamily_projection_injective L161
structure BooleanShadowCompletenessBoundary L166
theorem booleanShadowCompletenessBoundary_holds L185