Encyclopedia Foundation Foundation Pair Kernel Production Effect Physicality S26

ARTICLE 5 claims 5 theorems

Foundation Pair Kernel Production Effect Physicality S26

A machine-checked library proves that every operation in a discrete recognition ledger has a distinct, reversible effect, and that any physical system realizing those effects does so uniquely.

Verify this page

The effect ledger

In the Recognition Science framework, a ledger is a discrete record of events. The module named S26 concerns what happens when an operation is applied to that ledger: what its effect is, meaning the observable change it produces. The central idea is that an operation's effect is not defined by its internal mechanism, but by how it changes a fixed set of probes: the spatial axis, the tick commitment, and the balance current. These probes are the only things that matter for classifying what an operation does.

The module proves that this classification is well-behaved. Every primitive operation has a nonzero effect coordinate, meaning no operation is invisible to all probes. Reversing an operation preserves its effect class, and the effect of a finite batch of operations is the sum of their individual effects. The effect classes form a quotient with exactly five classes, and this quotient is canonically equivalent to the S22 Recognition response quotient, a previously established classification of responses. This means the new effect-based view is not a separate theory; it is the same classification seen from a different angle.

The most significant result concerns physical realization. Given any independently supplied physical response system, the module proves that a class carrying a given effect is unique whenever it exists. In plain language, if a physical system can produce a particular effect, it does so in exactly one way, as classified by the framework. The module also proves that whether every effect can be physically realized is equivalent to a condition called observable exhaustion, which is itself equivalent to earlier statements about operation selection and event transport. This is a precise boundary: the effect construction closes the question of how effects are classified and made unique, but it does not, by itself, prove that every effect must exist in a given physical system.

The proofs are carried out in a machine-checked library of formal theorems, with no unproved assumptions added. One notable consequence is that a zero-cost field does not select a spatial effect, meaning two different spatial operations can have the same exact cost yet different effect classes. This shows that cost alone is not enough to determine an operation's effect; the effect probes are doing the real work.

THEOREM everyProductionOperation_has_nontrivialEffect · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean
everyProductionOperation_has_nontrivialEffect · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean:316 
/-- Every primitive source operation changes one committed effect coordinate
by exactly one. -/
theorem everyProductionOperation_has_nontrivialEffect
    (operation : ProductionSourceOperation3) :
    ∃ probe : ProductionOperationEffectProbe3,
      productionOperationEffectObservation3 probe operation = 1 := by
  cases operation with
  | spatial spatial =>
      obtain ⟨axis, haxis⟩ :=
        realizedProductionEvent_has_spatialWitness spatial.event
      exact
        ⟨.spatialAxis axis,
          by simp [productionOperationEffectObservation3, haxis]⟩
  | tick tick =>
      refine ⟨.tickCommit, ?_⟩
      have htick :
          SuccessorTickProbe3
            (tickCommitOperationStart3 tick)
            (tickCommitOperationFinish3 tick) :=
        tickCommitOperation_is_one_successor tick
      simp [productionOperationEffectObservation3, htick]
  | balance balance =>
      refine ⟨.balanceCurrent, ?_⟩
      have hbalance :=
        balanceCurrentOperation_passes_probe balance
      simp [productionOperationEffectObservation3, hbalance]
THEOREM productionOperationEffectClass_reverse · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean
productionOperationEffectClass_reverse · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean:603 
theorem productionOperationEffectClass_reverse
    (operation : ProductionSourceOperation3) :
    productionOperationEffectClass3
        (reverseProductionSourceOperation3 operation) =
      productionOperationEffectClass3 operation := by
  apply identified_of_obsEquiv
  intro observation hobservation
  obtain ⟨probe, rfl⟩ := hobservation
  change
    productionOperationEffectObservation3 probe
        (reverseProductionSourceOperation3 operation) =
      productionOperationEffectObservation3 probe operation
  exact productionOperationEffectObservation_reverse probe operation
THEOREM productionOperationEffectClassEquivResponseQuotient3 · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean
productionOperationEffectClassEquivResponseQuotient3 · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean:484 
def productionOperationEffectClassEquivResponseQuotient3 :
    ProductionOperationEffectClass3 ≃
      RecognitionResponseQuotient3 where
  toFun := productionEffectClassToResponseQuotient3
  invFun := responseQuotientToProductionEffectClass3
  left_inv := by
    intro effectClass
    refine
      Quotient.inductionOn effectClass
        (fun operation => ?_)
    apply identified_of_obsEquiv
    intro observation hobservation
    obtain ⟨probe, rfl⟩ := hobservation
    change
      productionOperationEffectObservation3 probe
          (productionEffectOperationForResponse3
            (productionSourceOperationEffect_response3 operation)) =
        productionOperationEffectObservation3 probe operation
    rw [productionEffectOperationForResponse_observation,
      productionOperationEffectObservation_eq_responseCoordinate]
  right_inv := by
    intro responseClass
    refine
      Quotient.inductionOn responseClass
        (fun response => ?_)
    change
      proj responseCoordinateProbeFamily3
          (productionSourceOperationEffect_response3
            (productionEffectOperationForResponse3 response)) =
        proj responseCoordinateProbeFamily3 response
    rw [productionEffectOperationForResponse_response]
THEOREM productionEffect_carryingObservableClass_unique · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean
productionEffect_carryingObservableClass_unique · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean:889 
/-- No one effect can select two distinct physical observational classes.
Existence remains open, but class uniqueness is theorem-backed by S23. -/
theorem productionEffect_carryingObservableClass_unique
    (system : PostingPhysicalResponseSystem3 3)
    (target : RealizedPostingEvent3 3)
    (effect : ProductionOperationEffectClass3)
    (left right :
      ProductionObservableStateQuotient3 system target)
    (hleft :
      productionObservableClassMap3 system target left =
        productionEffectClassToResponseQuotient3 effect)
    (hright :
      productionObservableClassMap3 system target right =
        productionEffectClassToResponseQuotient3 effect) :
    left = right :=
  productionObservableClassMap_injective system target
    (hleft.trans hright.symm)
THEOREM zeroFieldCost_does_not_select_spatialEffect · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean
zeroFieldCost_does_not_select_spatialEffect · IndisputableMonolith/Foundation/PairKernelProductionEffectPhysicalityS26.lean:1030 
/-- Zero-field scalar cost is a non-discriminating probe: distinct spatial
effects can have the same zero-field cost. -/
theorem zeroFieldCost_does_not_select_spatialEffect :
    ∃ left right : SpatialEdgeActionOperation3,
      spatialEdgeActionExactCost3 left (fun _ => 0) =
        spatialEdgeActionExactCost3 right (fun _ => 0) ∧
      productionOperationEffectClass3 (.spatial left) ≠
        productionOperationEffectClass3 (.spatial right) := by
  let axis0 : Fin GapDerivation.D :=
    ⟨0, by norm_num [GapDerivation.D]⟩
  let axis1 : Fin GapDerivation.D :=
    ⟨1, by norm_num [GapDerivation.D]⟩
  let left :=
    spatialEdgeActionOperation3
      (productionSpatialEvent3 axis0)
  let right :=
    spatialEdgeActionOperation3
      (productionSpatialEvent3 axis1)
  refine ⟨left, right,
    zeroField_collapses_spatialActionCost left right, ?_⟩
  apply distinctSpatialAxes_have_distinctEffects
  intro haxis
  have hval := congrArg Fin.val haxis
  norm_num [axis0, axis1] at hval

What this page does not claim

This module does not prove that every effect is physically realized in a given system. This module does not derive the existence of physical channels from the current signature. This module does not claim that cost alone determines an operation's effect.

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/PairKernelProductionEffectPhysicalityS26.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