Encyclopedia Foundation Foundation Pair Kernel Scale Covariant Observables S20 Elapsed Time Unique Up To

ARTICLE 5 claims 5 theorems

Foundation Pair Kernel Scale Covariant Observables S20 Elapsed Time Unique Up To

Any way of measuring elapsed time in this framework is just another way of counting ticks, up to the choice of a positive unit.

Verify this page

The unit ambiguity

In ordinary physics, the same interval of time can be written as 60 seconds, 1 minute, or 0.0167 hours. The number changes, the duration does not. Recognition Science formalizes that everyday fact as a theorem about its own model of time, which counts discrete recognition events, called ticks. A ledger, a discrete record of events, assigns to each natural number n a measure of how much time has passed after n ticks. The theorem named elapsedTime_unique_up_to_positive_boundary_unit proves that any two such time measurements are related by a single positive multiplier: if one observable says the span for n ticks is L(n), the other says it is s times L(n), where s is the ratio of their values at one tick. In plain language, the only freedom in measuring elapsed time is which positive unit you start with.

The proof rests on additivity. A positive elapsed time observable assigns to n ticks exactly n times its value at one tick, a fact proved separately as elapsedTime_factors_through_Tick_count. That linearity leaves no room for a quadratic term, a parity effect, or any other distortion: the framework proves that a quadratic function of tick count and a parity-dependent function both fail the additivity test. So the uniqueness result is not a convention imposed by hand; it follows from the definition of what counts as a time measurement in this model. The same forcing appears at the level of full physical valuations: two valuations with the same carrier, survival, and cost structure differ only by positive duration and energy scales, as the companion theorem observablePackage_unique_up_to_positive_units states.

What the declaration does not claim is just as important. It does not select any absolute unit: no second, no hydrogen transition, no Planck time is singled out. It does not say that the ratio between two units is physically meaningful in itself; only normalized tick ratios, where each span is divided by the one-tick span, are invariant across unit choices. And it does not claim that any particular physical system realizes the abstract observables. The theorem lives in the formal structure; the step from that structure to a concrete detector that responds distinctly to each channel remains a hypothesis, not a proved result. The framework's own documentation marks that boundary explicitly: the parent-response catalog is theorem, its physical realization is not.

THEOREM elapsedTime_unique_up_to_positive_boundary_unit · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean
elapsedTime_unique_up_to_positive_boundary_unit · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean:101 
/-- Any two elapsed-time observables differ by a unique positive unit ratio at
the level of all Tick spans. Existence is the physical scale-covariance
statement; the ratio is fixed by the one-Tick boundary values. -/
theorem elapsedTime_unique_up_to_positive_boundary_unit
    (left right : PositiveElapsedTimeObservable) :
    ∃ scale : ℝ, 0 < scale ∧
      scale = right.span.measure 1 / left.span.measure 1 ∧
      ∀ n : ℕ,
        right.span.measure n =
          scale * left.span.measure n := by
  obtain ⟨scale, hscale, hspan⟩ :=
    additiveTickSpanMeasures_unique_up_to_positive_scale
      left.span right.span left.unit_pos right.unit_pos
  refine
    ⟨scale, hscale, ?_, hspan⟩
  have hunit := hspan 1
  change
    right.span.measure 1 =
      scale * left.span.measure 1 at hunit
  apply (eq_div_iff left.unit_pos.ne').2
  nlinarith
THEOREM elapsedTime_factors_through_Tick_count · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean
elapsedTime_factors_through_Tick_count · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean:80 
/-- Every positive elapsed-time observable is Tick count times its one-Tick
boundary unit. -/
theorem elapsedTime_factors_through_Tick_count
    (observable : PositiveElapsedTimeObservable)
    (n : ℕ) :
    observable.span.measure n =
      (n : ℝ) * observable.span.measure 1 :=
  additiveTickSpanMeasure_eq_nat_mul_unit observable.span n
THEOREM quadraticTickObservable_not_additive · parityTickObservable_not_additive · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean
quadraticTickObservable_not_additive · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean:204 
theorem quadraticTickObservable_not_additive :
    ¬ ∀ m n : ℕ,
      quadraticTickObservable (m + n) =
        quadraticTickObservable m +
          quadraticTickObservable n := by
  intro hadd
  have h := hadd 1 1
  norm_num [quadraticTickObservable] at h
parityTickObservable_not_additive · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean:216 
theorem parityTickObservable_not_additive :
    ¬ ∀ m n : ℕ,
      parityTickObservable (m + n) =
        parityTickObservable m +
          parityTickObservable n := by
  intro hadd
  have h := hadd 1 1
  norm_num [parityTickObservable] at h
THEOREM observablePackage_unique_up_to_positive_units · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean
observablePackage_unique_up_to_positive_units · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean:566 
/-- Two representatives of one observable class differ by exactly one
positive duration unit and one positive energy unit. -/
theorem observablePackage_unique_up_to_positive_units
    {N : ℕ} [NeZero N]
    {left right : RecognitionPhysicalValuation3 N}
    (hsame : SameRecognitionData3 left right) :
    ∃ durationScale energyScale : ℝ,
      0 < durationScale ∧
        0 < energyScale ∧
        (∀ n : ℕ,
          right.span.measure n =
            durationScale * left.span.measure n) ∧
        right.energyScale =
          energyScale * left.energyScale ∧
        (∀ event : RealizedPostingEvent3 N,
          right.kinematics.duration event.1 =
            durationScale *
              left.kinematics.duration event.1) ∧
        (∀ event : RealizedPostingEvent3 N,
          right.kinematics.energy event.1 =
            energyScale *
              left.kinematics.energy event.1) ∧
        (∀ event : RealizedPostingEvent3 N,
          postingEventAction3 right.kinematics event.1 =
            (durationScale * energyScale) *
              postingEventAction3
                left.kinematics event.1) := by
  let durationScale :=
    right.span.measure 1 / left.span.measure 1
  let energyScale :=
    right.energyScale / left.energyScale
  have hdurationScale :
      0 < durationScale :=
    div_pos right.span_unit_pos left.span_unit_pos
  have henergyScale :
      0 < energyScale :=
    div_pos right.energyScale_pos left.energyScale_pos
  have hspan :
      ∀ n : ℕ,
        right.span.measure n =
          durationScale * left.span.measure n := by
    intro n
    calc
      right.span.measure n =
          (n : ℝ) * right.span.measure 1 :=
        additiveTickSpanMeasure_eq_nat_mul_unit
          right.span n
      _ = durationScale *
          ((n : ℝ) * left.span.measure 1) := by
        dsimp [durationScale]
        field_simp [left.span_unit_pos.ne']
      _ = durationScale *
          left.span.measure n := by
        rw [additiveTickSpanMeasure_eq_nat_mul_unit
          left.span n]
  have henergyScaleEq :
      right.energyScale =
        energyScale * left.energyScale := by
    dsimp [energyScale]
    field_simp [left.energyScale_pos.ne']
  have hduration :
      ∀ event : RealizedPostingEvent3 N,
        right.kinematics.duration event.1 =
          durationScale *
            left.kinematics.duration event.1 := by
    intro event
    calc
      right.kinematics.duration event.1 =
          right.span.measure 1 :=
        tickSpanFactorization_eventDuration_eq_unit
          right.duration_factors event
      _ = durationScale * left.span.measure 1 :=
        hspan 1
      _ = durationScale *
          left.kinematics.duration event.1 := by
        rw [tickSpanFactorization_eventDuration_eq_unit
          left.duration_factors event]
  have hprice :
      right.price = left.price :=
    hsame.2.2.symm
  have henergy :
      ∀ event : RealizedPostingEvent3 N,
        right.kinematics.energy event.1 =
          energyScale *
            left.kinematics.energy event.1 := by
    intro event
    calc
      right.kinematics.energy event.1 =
          right.energyScale * right.price event :=
        right.energy_scaled event
      _ = (energyScale * left.energyScale) *
          left.price event := by
        rw [henergyScaleEq, hprice]
      _ = energyScale *
          left.kinematics.energy event.1 := by
        rw [left.energy_scaled event]
        ring
  refine
    ⟨durationScale, energyScale,
      hdurationScale, henergyScale,
      hspan, henergyScaleEq,
      hduration, henergy, ?_⟩
  intro event
  unfold postingEventAction3
  rw [hduration event, henergy event]
  ring
THEOREM normalizedElapsedTickCount_invariant · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean
normalizedElapsedTickCount_invariant · IndisputableMonolith/Foundation/PairKernelScaleCovariantObservablesS20.lean:140 
/-- All dimensionless time ratios are invariant under the choice of positive
boundary unit. -/
theorem normalizedElapsedTickCount_invariant
    (left right : PositiveElapsedTimeObservable)
    (n : ℕ) :
    normalizedElapsedTickCount left n =
      normalizedElapsedTickCount right n := by
  rw [normalizedElapsedTickCount_eq_count,
    normalizedElapsedTickCount_eq_count]

What this page does not claim

No absolute time unit, such as the SI second, is selected or derived. The theorem does not claim that any concrete physical detector realizes the abstract observables. The additivity property alone, without the positivity condition, does not force the linear form.

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