IndisputableMonolith.RecognitionCore

   1import IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.QuotientSelection
   2import IndisputableMonolith.Foundation.RecognitionSignatureGauge
   3import IndisputableMonolith.Foundation.ObserverFromRecognition
   4import IndisputableMonolith.Foundation.RecognizerInducesLogic
   5import IndisputableMonolith.Foundation.MultiplicativeRecognizerL4
   6import IndisputableMonolith.Foundation.RecognitionLatticeFromRecognizer
   7import IndisputableMonolith.RecogGeom.Composition
   8import IndisputableMonolith.RecogGeom.FiniteResolution
   9
  10/-!
  11# Recognition Core — the shape of logic at the recognizer / signature layer
  12
  13This public aggregator exposes the recognition-geometry core that sits at the
  14T0 / T4 layer of the forcing chain: the recognizer, its indistinguishability
  15quotient, the full recognition signature, and the completeness condition under
  16which the signature determines all physically relevant states.
  17
  18It is the formal answer to "a single Boolean observable is atomic, not complete;
  19the physical content is carried by the admitted recognizer family." Every
  20declaration below is proved in Lean with no `sorry` and no project-local axiom.
  21
  22## Public citation targets
  23
  24* `forced_quotient_iff` — the full signature determines the state up to the
  25  indistinguishability quotient (unconditional).
  26* `gauge_from_indistinguishability` — the physically forced quotient is exactly
  27  indistinguishability under the admitted family; gauge is the absence of a
  28  distinguishing recognition act.
  29* `signature_complete_iff_separating` — completeness (injective physical
  30  quotient) holds iff the family separates points. Necessary and sufficient.
  31* `one_bit_not_complete_boundary` — one Boolean coordinate is atomic, not
  32  complete; a separating family reconstructs the state; scalar-cost completeness
  33  is a separate hypothesis.
  34* `recognizer_refinement` — composing recognizers refines the quotient; more
  35  recognizers give a finer observable structure.
  36* `recognizer_forces_observer` — non-trivial recognition forces a primitive
  37  observer.
  38* `recognizer_induces_logic` — a recognizer supplies the three definitional
  39  Aristotelian conditions plus the primitive observer for free.
  40* `multiplicative_recognizer_L4` — composition consistency (the d'Alembert law)
  41  is derived, not assumed, on the multiplicative event space.
  42* `recognition_lattice` — a recognizer's kernel classes are the first
  43  recognition lattice; same-kernel interfaces give canonically equivalent
  44  lattices.
  45-/
  46
  47namespace IndisputableMonolith
  48namespace RecognitionCore
  49
  50/-! ## Signature, quotient, and completeness -/
  51
  52/-- The full recognition signature determines the state up to the
  53indistinguishability quotient, with no hypothesis. -/
  54abbrev forced_quotient_iff :=
  55  @Foundation.PrimitiveRecognitionCalculus.QuotientSelection.forced_iff
  56
  57/-- The physically forced quotient is exactly indistinguishability under the
  58admitted observable family; observables descend; a separating family collapses
  59the quotient to the identity. -/
  60abbrev gauge_from_indistinguishability :=
  61  @Foundation.PrimitiveRecognitionCalculus.QuotientSelection.gauge_from_indistinguishability
  62
  63/-- Signature equality is the physical quotient. -/
  64abbrev signature_forced_quotient_iff :=
  65  @Foundation.RecognitionSignatureGauge.signature_forced_quotient_iff
  66
  67/-- Completeness: a separating recognition signature gives an injective physical
  68quotient. This is the exact necessary-and-sufficient completeness condition. -/
  69abbrev signature_complete_iff_separating :=
  70  @Foundation.RecognitionSignatureGauge.signature_projection_injective_of_separating
  71
  72/-- The corrected T0 boundary: one Boolean coordinate is atomic not complete; a
  73separating family reconstructs the state; scalar-cost completeness needs an extra
  74hypothesis. -/
  75abbrev one_bit_not_complete_boundary :=
  76  Foundation.RecognitionSignatureGauge.booleanShadowCompletenessBoundary_holds
  77
  78/-! ## Recognizer family: generation and refinement -/
  79
  80/-- Composing recognizers refines the quotient: more recognizers give a finer
  81observable structure. -/
  82abbrev recognizer_refinement :=
  83  @RecogGeom.refinement_theorem
  84
  85/-- Non-trivial recognition forces a primitive observer (finite interface). -/
  86abbrev recognizer_forces_observer :=
  87  Foundation.ObserverFromRecognition.observerFromRecognitionCert
  88
  89/-- A recognizer supplies the three definitional Aristotelian conditions plus
  90the primitive observer automatically on its event space. -/
  91abbrev recognizer_induces_logic :=
  92  @Foundation.RecognizerInducesLogic.unification
  93
  94/-- Composition consistency (the d'Alembert law) is derived, not assumed, on the
  95positive multiplicative event space. -/
  96abbrev multiplicative_recognizer_L4 :=
  97  @Foundation.MultiplicativeRecognizerL4.MultiplicativeRecognizer.l4DerivableCert_inhabited
  98
  99/-- A recognizer's kernel classes are the first recognition lattice. -/
 100abbrev recognition_lattice :=
 101  @Foundation.RecognitionLatticeFromRecognizer.recognitionLatticeCert_inhabited
 102
 103end RecognitionCore
 104end IndisputableMonolith
 105