Foundation Pair Kernel Production Operation Channel Selection S25 Spatial Action

The spatial action selector

In the Recognition Science framework, the declaration spatialActionSelector_iff_S24_spatialTransport is a formal, machine-checked theorem. It states that a specific set of three operations, a spatial edge action, a tick commit, and a balance current, together perform exactly the same event transport as the S24 event-act transport. The framework models events as discrete records in a ledger, and this theorem pins down which operations count as the production of that transport.

The theorem is not a claim about physics directly. It is a claim about the framework's own formal definitions. The three operations are data, not response labels. Their orientation, conservation, and finite-batch composition laws are theorem-backed. The theorem proves that these operations, when taken together, are exactly equivalent to the S24 event-act transport. It does not prove that any physical carrier exists, nor that the operations are complete, nor that they exhaust all possible observations.

The framework's library proves several supporting facts. A spatial edge action has a positive cost when the field differs across the edge. Reversing the operation reverses the flux but leaves the exact cost unchanged. A tick commit is a single successor step. A balance current passes a conservation probe. These are the properties that make the operations well-behaved components of the transport.

The theorem also shows that the operations are independent of any proposed response system. They coexist with both a transport-complete and an incomplete system. This means the theorem does not depend on a particular physical implementation. It is a statement about the formal structure of the operations themselves.

What the theorem does not claim is equally important. It does not construct the physical carrier. It does not prove completeness of the operations. It does not claim observational exhaustion. The first missing physical semantic is split into three operation-to-channel selectors, and their conjunction is exactly the S24 event-act transport. The theorem is a precise formal statement, and its limits are part of that precision.

/-- The same committed operation package coexists with a system that selects
all operation channels and one that does not. Hence the source operations do
not force their promotion to physical channels. -/
theorem committedOperations_admit_channelSelection_split :
    CommittedProductionOperations3 ∧
      ∃ left right : PostingPhysicalResponseSystem3.{0} 3,
        ProductionOperationsSelectPhysicalChannels3 left ∧
          ¬ ProductionOperationsSelectPhysicalChannels3 right := by
  obtain
    ⟨left, right, _hleftReads, _hrightReads,
      hleftTransport, hrightNotTransport⟩ :=
    committed_ancestry_admits_eventActTransport_split
  exact
    ⟨committedProductionOperations_hold,
      left, right,
      (productionOperationSelectors_iff_eventActTransport
        left).2 hleftTransport,
      fun hright =>
        hrightNotTransport
          ((productionOperationSelectors_iff_eventActTransport
            right).1 hright)⟩

theorem spatialEdgeActionOperation_cost_positive
    (operation : SpatialEdgeActionOperation3)
    (field : Fin (TorusCard3 3) → ℝ)
    (hdrop :
      field operation.event.1.1 -
        field operation.event.1.2 ≠ 0) :
    0 < spatialEdgeActionExactCost3 operation field := by
  have hpositive :=
    realizedPrimitivePostingPair_exactJCost_positive
      operation.event.2 field hdrop
  simpa [spatialEdgeActionExactCost3,
    spatialEdgeActionOperation_weight_eq_one] using hpositive

theorem spatialEdgeActionFlux_reverse
    (operation : SpatialEdgeActionOperation3)
    (field : Fin (TorusCard3 3) → ℝ) :
    spatialEdgeActionFlux3
        (reverseSpatialEdgeActionOperation3 operation)
        field =
      -spatialEdgeActionFlux3 operation field := by
  change
    exactJEdgeFlux
        (recognitionProductionGraph3 3)
        field operation.event.1.2
          operation.event.1.1 =
      -exactJEdgeFlux
        (recognitionProductionGraph3 3)
        field operation.event.1.1
          operation.event.1.2
  exact
    exactJEdgeFlux_antisym
      (recognitionProductionGraph3 3)
      field
      operation.event.1.2
      operation.event.1.1

theorem tickCommitOperation_is_one_successor
    (operation : TickCommitOperation3) :
    tickCommitOperationFinish3 operation =
      recognitionTimeAlgebra.succ
        (tickCommitOperationStart3 operation) :=
  postingEventEndTick3_eq_succ operation.event

theorem balanceCurrentOperation_passes_probe
    (operation : BalanceCurrentOperation3) :
    BalanceCurrentProbe3
      (balanceCurrentOperationCurrent3 operation) :=
  elementaryPosting_passes_balanceCurrentProbe
    operation.event.1.1 operation.event.1.2

What this page does not claim

The theorem does not construct any physical carrier. The theorem does not prove completeness or observational exhaustion of the operations. The theorem does not claim the operations are the only possible ones.

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/PairKernelProductionOperationChannelSelectionS25.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: