Encyclopedia Foundation Foundation Pair Kernel Scale Covariant Observables S20 Consumer Canonical Elapse

ARTICLE 4 claims 3 theorems 1 model

Foundation Pair Kernel Scale Covariant Observables S20 Consumer Canonical Elapse

A machine-checked definition pins down the framework's standard way of reading elapsed time, and a theorem shows it counts eight ticks exactly.

Verify this page

The canonical time readout

In the Recognition Science framework, time is not a background dial but a property of recognition events: discrete records of change that reality keeps. The declaration canonicalElapsedTimeObservable defines the standard way to read elapsed time from such a ledger. It is a MODEL, a definitional choice, not a physical law. The choice fixes the unit of time as a single tick, the smallest meaningful span in the framework's discrete record, and it makes that unit positive, so elapsed time always runs forward.

The definition lives inside a larger consumer that reorganizes how physical quantities are exposed after absolute duration and energy units have been moved to explicit boundary inputs. The observable itself is simple: it takes a span and reports it in tick units. The surrounding consumer also defines how posting events, the individual entries in the ledger, carry duration, energy, and action, and it divides out the boundary units so that only dimensionless ratios survive.

A theorem in the same file, canonicalScaleCovariantConsumer_exists, proves that a realized posting event exists whose normalized elapsed tick count is exactly 8. That is the eight-tick recognition cycle appearing as a concrete instance: the framework's canonical time readout, applied to a realized event, counts eight ticks. The theorem also shows the event has carrier dimension 5 and that its normalized duration, energy, and action all match the posting event's channel price.

The framework's library, a machine-checked collection of formal theorems, also proves prediction-ready ratios for the exact-J Green function, the source-curvature relation that underpins the framework's cost law. Those ratios are dimensionless: they survive the unit quotient. What does not survive is equality between a physical event's absolute action and the dimensionless RS constant hbar = phi^-5. The quotient result is intentionally asymmetric: action ratios survive, absolute action equality does not.

What the declaration does not claim is broader than what it does. It does not claim that elapsed time in the physical world is discrete; that is a modeling choice, not a measured fact. It does not claim that the eight-tick count is the only possible count; the theorem shows existence of one event, not uniqueness. And it does not claim that the canonical observable is the only way to read time; it is the canonical representative of an interface, a convention the framework chooses.

MODEL canonicalElapsedTimeObservable · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20Consumer.lean
canonicalElapsedTimeObservable · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20Consumer.lean:35 
def canonicalElapsedTimeObservable :
    PositiveElapsedTimeObservable where
  span := unitTickSpanMeasure
  unit_pos := by
    norm_num [unitTickSpanMeasure]
THEOREM canonicalScaleCovariantConsumer_exists · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20Consumer.lean
canonicalScaleCovariantConsumer_exists · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20Consumer.lean:62 
/-- MODEL consumer: the canonical representative inhabits the
scale-covariant interface, while every exported numeric statement has had its
duration and energy boundary units divided out. -/
theorem canonicalScaleCovariantConsumer_exists :
    ∃ event : RealizedPostingEvent3 3,
      normalizedPostingDuration3
          canonicalScaleCovariantPostingReadoutSemantics3
          event.1 = 1 ∧
        normalizedPostingEnergy3
          canonicalScaleCovariantPostingReadoutSemantics3
          event.1 =
            canonicalPostingEventChannelPrice3 event ∧
        normalizedPostingAction3
          canonicalScaleCovariantPostingReadoutSemantics3
          event.1 =
            canonicalPostingEventChannelPrice3 event ∧
        physicalPostingCarrierDimension3
          (parentPhysicalChannelCarrier3 3) event = 5 ∧
        normalizedElapsedTickCount
          canonicalElapsedTimeObservable 8 = 8 := by
  obtain ⟨pair, hpair⟩ :=
    realizedPrimitivePostingPair3_exists
  let event : RealizedPostingEvent3 3 :=
    ⟨pair, hpair⟩
  refine
    ⟨event,
      normalizedPostingDuration_eq_one
        canonicalScaleCovariantPostingReadoutSemantics3 event,
      normalizedPostingEnergy_eq_price
        canonicalScaleCovariantPostingReadoutSemantics3 event,
      normalizedPostingAction_eq_price
        canonicalScaleCovariantPostingReadoutSemantics3 event,
      ?_,
      elapsedTime_octave_ratio
        canonicalElapsedTimeObservable⟩
  exact
    scaleCovariantReadout_dimension_eq_five
      canonicalScaleCovariantPostingReadoutSemantics3 event
THEOREM canonicalScaleCovariantConsumer_exists · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20Consumer.lean
canonicalScaleCovariantConsumer_exists · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20Consumer.lean:62 
/-- MODEL consumer: the canonical representative inhabits the
scale-covariant interface, while every exported numeric statement has had its
duration and energy boundary units divided out. -/
theorem canonicalScaleCovariantConsumer_exists :
    ∃ event : RealizedPostingEvent3 3,
      normalizedPostingDuration3
          canonicalScaleCovariantPostingReadoutSemantics3
          event.1 = 1 ∧
        normalizedPostingEnergy3
          canonicalScaleCovariantPostingReadoutSemantics3
          event.1 =
            canonicalPostingEventChannelPrice3 event ∧
        normalizedPostingAction3
          canonicalScaleCovariantPostingReadoutSemantics3
          event.1 =
            canonicalPostingEventChannelPrice3 event ∧
        physicalPostingCarrierDimension3
          (parentPhysicalChannelCarrier3 3) event = 5 ∧
        normalizedElapsedTickCount
          canonicalElapsedTimeObservable 8 = 8 := by
  obtain ⟨pair, hpair⟩ :=
    realizedPrimitivePostingPair3_exists
  let event : RealizedPostingEvent3 3 :=
    ⟨pair, hpair⟩
  refine
    ⟨event,
      normalizedPostingDuration_eq_one
        canonicalScaleCovariantPostingReadoutSemantics3 event,
      normalizedPostingEnergy_eq_price
        canonicalScaleCovariantPostingReadoutSemantics3 event,
      normalizedPostingAction_eq_price
        canonicalScaleCovariantPostingReadoutSemantics3 event,
      ?_,
      elapsedTime_octave_ratio
        canonicalElapsedTimeObservable⟩
  exact
    scaleCovariantReadout_dimension_eq_five
      canonicalScaleCovariantPostingReadoutSemantics3 event
THEOREM actionQuotient_consumer · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20Consumer.lean
actionQuotient_consumer · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20Consumer.lean:134 
/-- The quotient result is intentionally asymmetric: dimensionless action
ratios survive, while equality between a physical event's absolute action and
the dimensionless RS `hbar = phi^-5` numeral does not survive the full
duration-energy unit quotient. The numeral and its D+2 exponent do survive. -/
theorem actionQuotient_consumer :
    (∃ left right : RecognitionPhysicalValuation3.{0} 3,
      SameRecognitionData3 left right ∧
        ∃ event : RealizedPostingEvent3 3,
          postingEventAction3 left.kinematics event.1 ≠
            postingEventAction3 right.kinematics event.1) ∧
      (∀ left right : RecognitionPhysicalValuation3.{0} 3,
        SameRecognitionData3 left right →
          ∀ first second : RealizedPostingEvent3 3,
            postingEventAction3 left.kinematics first.1 *
                postingEventAction3 right.kinematics second.1 =
              postingEventAction3 left.kinematics second.1 *
                postingEventAction3 right.kinematics first.1) :=
  ⟨absolute_eventAction_not_unit_invariant,
    fun _ _ hsame =>
      unitEquivalent_action_ratio_invariant hsame⟩

What this page does not claim

The discreteness of physical time is a modeling choice, not a measured fact. The eight-tick count is an existence result, not a uniqueness claim. The canonical observable is the canonical representative of an interface, not the only possible time readout.

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