Encyclopedia Foundation Foundation Pair Kernel Production Effect Physicality S26 Consumer S26 S25 Operat

ARTICLE 3 claims 3 theorems

Foundation Pair Kernel Production Effect Physicality S26 Consumer S26 S25 Operat

A machine-checked package that bundles together the full source-effect result for production operations, without yet touching physical readouts.

Verify this page

The operation consumer

The declaration s26_S25_operation_consumer_compiles is a single named package in the Recognition Science framework's machine-checked library of formal theorems. It bundles one complete theorem, productionEffect_source_consumer, which states that the five-class source effect quotient for production operations exists, that every operation has a probe observing it, that the coordinate representation is injective, and that the quotient satisfies a universal property. In plain terms: the framework proves that production operations can be organized into exactly five distinct effect classes, with no two operations sharing a class unless they are genuinely equivalent, and that any map respecting the invariant structure factors uniquely through the quotient.

This is a recognition claim, meaning it concerns how the framework's discrete ledger of events classifies operations by their observable effects. The theorem is fully proved in the framework's library, with no unproved assumptions. It is a structural result about the source-effect quotient, not a physical one. The package is named a consumer because it consumes, or packages, the complete source-effect result as one unit for later stages of the framework's forcing chain.

The declaration does not establish physical readouts. The docstring is explicit: physical readouts compile only under the exact effect realization arrow, which S26 proves equivalent to S25 selectors, S24 transport, and S23 exhaustion. A separate theorem in the same file, effectRealizedProduction_scaleCovariant_consumer_exists, shows that physical readouts do exist once a system supplies the realization arrow, but that theorem is not part of this declaration. The operation consumer package is the structural prerequisite, not the physical payoff.

In Recognition Science, this distinction matters because the framework's chain of theorems moves from pure structure to physical content in stages. The operation consumer establishes the classification of operations by effects, which is a necessary foundation. The physical readouts, with their scale covariance and channel prices, come only after the realization arrow is supplied. This declaration is the classification step, and it is complete on its own terms.

THEOREM productionEffect_source_consumer · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26Consumer.lean
productionEffect_source_consumer · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26Consumer.lean:40 
/-- The complete source-effect result consumed as one package. -/
theorem productionEffect_source_consumer :
    Fintype.card ProductionOperationEffectClass3 = 5 ∧
      (∀ operation : ProductionSourceOperation3,
        ∃ probe : ProductionOperationEffectProbe3,
          productionOperationEffectObservation3 probe operation = 1) ∧
      Function.Injective
        productionOperationEffectCoordinateRepresentation3 ∧
      (∀ {β : Type*}
          (map : ProductionSourceOperation3 → β),
        ProductionOperationEffectInvariantMap3 map →
          ∃! descended :
              ProductionOperationEffectClass3 → β,
            ∀ operation,
              descended
                  (productionOperationEffectClass3 operation) =
                map operation) :=
  ⟨productionOperationEffectClass_card_eq_five,
    everyProductionOperation_has_nontrivialEffect,
    productionOperationEffectCoordinateRepresentation_injective,
    productionOperationEffectInvariantMap_factors_unique⟩
THEOREM s26_S25_operation_consumer_compiles · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26Consumer.lean
s26_S25_operation_consumer_compiles · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26Consumer.lean:119 
def s26_S25_operation_consumer_compiles :=
  productionOperations_source_consumer
THEOREM effectRealizedProduction_scaleCovariant_consumer_exists · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26Consumer.lean
effectRealizedProduction_scaleCovariant_consumer_exists · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26Consumer.lean:62 
/-- S17-S20 physical readouts compile once the exact effect-to-channel
realization arrow is supplied. -/
theorem effectRealizedProduction_scaleCovariant_consumer_exists
    (system : PostingPhysicalResponseSystem3.{0} 3)
    (hrealize :
      ProductionEffectsRealizePhysicalChannels3 system) :
    ∃ event : RealizedPostingEvent3 3,
      normalizedPostingDuration3
          (observableProductionScaleCovariantPostingReadoutSemantics3
            system
            ((productionOperationSelectors_iff_observableExhaustion
              system).1
              ((productionEffectsRealizeChannels_iff_operationSelectors
                system).1 hrealize)))
          event.1 = 1 ∧
        normalizedPostingEnergy3
          (observableProductionScaleCovariantPostingReadoutSemantics3
            system
            ((productionOperationSelectors_iff_observableExhaustion
              system).1
              ((productionEffectsRealizeChannels_iff_operationSelectors
                system).1 hrealize)))
          event.1 =
            canonicalPostingEventChannelPrice3 event ∧
        normalizedPostingAction3
          (observableProductionScaleCovariantPostingReadoutSemantics3
            system
            ((productionOperationSelectors_iff_observableExhaustion
              system).1
              ((productionEffectsRealizeChannels_iff_operationSelectors
                system).1 hrealize)))
          event.1 =
            canonicalPostingEventChannelPrice3 event ∧
        physicalPostingCarrierDimension3
          (observableProductionPhysicalChannelCarrier3
            system
            ((productionOperationSelectors_iff_observableExhaustion
              system).1
              ((productionEffectsRealizeChannels_iff_operationSelectors
                system).1 hrealize)))
          event = 5 ∧
        PostingCarrierResponseObservability3
          (observableProductionResponseSystem3
            system
            ((productionOperationSelectors_iff_observableExhaustion
              system).1
              ((productionEffectsRealizeChannels_iff_operationSelectors
                system).1 hrealize))) := by
  exact
    operationSelectedProduction_scaleCovariant_consumer_exists
      system
      ((productionEffectsRealizeChannels_iff_operationSelectors
        system).1 hrealize)

What this page does not claim

The declaration does not prove that any physical system satisfies the realization arrow. The declaration does not establish the values of normalized posting duration, energy, or action. The declaration does not claim that the five classes correspond to any measured physical quantities.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26Consumer.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND