Foundation Pair Kernel Gap2a Phase Bearing Transaction Residual Phase Bearing Ti

The one-tick span

A ledger, a discrete record of events, needs a way to mark when an event happens. In the Recognition Science framework, the tick, the smallest unit of time in the record, is that mark. The declaration phaseBearingTickCommitEvent3_span_eq_one states a simple fact about the framework's eight-phase transaction cycle: each phase's commit event spans exactly one tick. The theorem is proved for every one of the eight phases, so the entire cycle, taken as a sequence of commits, covers exactly eight ticks.

The construction behind this fact is a Gray code, a sequence of binary states where consecutive states differ by a single bit. The framework uses a three-bit Gray cycle to order its eight phases. Each phase carries a posting event, a record of a change in the ledger, and the theorem ties that event to a single tick. The proof is short: it follows directly from a more general fact about posting events and their tick spans. This is a formal theorem, a statement checked by a machine, with no gaps and no extra assumptions.

The theorem does not claim anything about physical time. The tick is a unit in the ledger's own accounting, not a second or a Planck time. The framework explicitly states that the Gray state and its period are dimensionless data. The theorem also does not select a physical action scale, the size of the change associated with a posting. Two different representatives of the same observable class can have different actions, and the framework proves that no selector can recover an absolute action from the phase data alone. The complete-orbit Green aggregate, the sum of the posting magnitudes over all eight phases, is stated separately and equals four times a constant per-posting magnitude, but identifying that aggregate with a static continuum source is additional physical content, not part of this theorem.

What the theorem buys is a precise, machine-checked anchor for the cycle's period. The eight-phase transaction returns to its starting state after eight commits, and the one-tick span per phase makes that period exact in the ledger's own time. This is a construction, not a physical selection theorem. The no-go results about action and scale are theorems; the Gray schedule itself is a definitional choice. The framework's library proves the transaction cannot return sooner, and it proves the span of each commit, but it leaves the physical interpretation of the tick to further work.

theorem phaseBearingTickCommitEvent3_span_eq_one
    (phase : Fin 8) :
    postingEventTickSpan3
      (phaseBearingTickCommitEvent3 phase) = 1 :=
  postingEventTickSpan3_eq_one _

theorem phaseBearingTickCommitEvent3_span_eq_one
    (phase : Fin 8) :
    postingEventTickSpan3
      (phaseBearingTickCommitEvent3 phase) = 1 :=
  postingEventTickSpan3_eq_one _

/-- Even on the exact eight-phase actual transaction, absolute posting action
does not descend through the current observable quotient. -/
theorem no_phaseTransaction_selector_recovers_absolutePostingAction :
    ¬ ∃ selector : PhaseTransactionAbsoluteActionSelector3,
      SelectsAllPhaseRepresentativeActions3 selector := by
  rintro ⟨selector, hselector⟩
  let left : RecognitionPhysicalValuation3.{0} 3 :=
    unitRecognitionPhysicalValuation3
      (parentPhysicalChannelCarrier3 3)
  let right : RecognitionPhysicalValuation3.{0} 3 :=
    scalePhysicalValuation3
      2 1 (by norm_num) (by norm_num) left
  let phase : Fin 8 := 0
  have hsame : SameRecognitionData3 left right := by
    dsimp [right]
    exact scalePhysicalValuation_sameRecognitionData
      2 1 (by norm_num) (by norm_num) left
  have hclass :
      physicalObservableClass3 left =
        physicalObservableClass3 right :=
    sameRecognitionData_sameObservableClass hsame
  have hleft := hselector left phase
  have hright := hselector right phase
  rw [← hclass] at hright
  have hequal :
      postingEventAction3 left.kinematics
          (phaseBearingPostingEvent3 phase).1 =
        postingEventAction3 right.kinematics
          (phaseBearingPostingEvent3 phase).1 :=
    hleft.symm.trans hright
  have hscaled :
      postingEventAction3 right.kinematics
          (phaseBearingPostingEvent3 phase).1 =
        2 *
          postingEventAction3 left.kinematics
            (phaseBearingPostingEvent3 phase).1 := by
    dsimp [right]
    simpa using
      (scalePhysicalValuation_eventAction
        2 1 (by norm_num) (by norm_num) left
        (phaseBearingPostingEvent3 phase).1)
  have hpositive :
      0 <
        postingEventAction3 left.kinematics
          (phaseBearingPostingEvent3 phase).1 :=
    mul_pos
      (left.kinematics.energy_pos _)
      (left.kinematics.duration_pos _)
  rw [hscaled] at hequal
  nlinarith

What this page does not claim

The theorem does not assign a physical duration to a tick. The theorem does not select a physical action scale for the posting events. The theorem does not identify the complete-orbit Green aggregate with a static continuum source.

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