Encyclopedia Foundation Foundation Pair Kernel Physical Valuation Initiality S19 Weak Signature And Acti

ARTICLE 5 claims 4 theorems 1 hypothesis

Foundation Pair Kernel Physical Valuation Initiality S19 Weak Signature And Acti

Two different physical descriptions of the same events can have opposite duration and energy scales, and still agree on the action of every event.

Verify this page

The inverse scale freedom

In physics, a scale is the size of the unit you measure with. For a duration, the unit might be a second or a nanosecond; for an energy, a joule or an electronvolt. The declaration weak_signature_and_action_admit_inverse_scales is a formal statement in the framework's machine-checked library. It proves that two descriptions of the same set of recognition events can use different positive scales for duration and energy, and still assign the same action to every event. Action is the product of duration and energy; if one description doubles its duration unit and halves its energy unit, the product, and therefore the action, is unchanged.

The statement makes this precise. It produces two valuations, left and right, that share the same recognition data: the same physical carriers, the same survival probabilities, and the same channel prices. Yet the measure of a single tick span, the basic duration unit, differs between them, and the energy scale differs as well. Despite these differences, for every possible event pair, the action computed from the left kinematics equals the action computed from the right kinematics. The two descriptions are physically distinct in their absolute units, but indistinguishable in their action.

This result is a non-uniqueness statement. It shows that the weak structural signature, the collection of conditions a physical valuation must satisfy, does not fix absolute duration or energy scales. The framework's library also proves that any additive tick span measure is unique up to a positive scale, and that the recognition tick count, the natural-number index of a tick, is unique. What the weak signature does fix are combinatorics and dimensionless ratios, not the absolute size of the units.

The statement does not claim that absolute scales are meaningless or that all valuations are equally valid. It does not say that no stronger set of conditions could select absolute scales. It does not claim that the action equality holds for arbitrary scalings; the proof relies on the specific product structure of the action. The selection of an operational duration readout, one that reads the tick count directly, remains a hypothesis, not a proven result. The result is a precise boundary on what the weak signature can determine, not a statement about what physics must be.

THEOREM weak_signature_and_action_admit_inverse_scales · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean
weak_signature_and_action_admit_inverse_scales · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean:413 
/-- Even preserving event action does not split the two physical units:
duration scale two and energy scale one-half leave their product unchanged. -/
theorem weak_signature_and_action_admit_inverse_scales :
    ∃ left right : RecognitionPhysicalValuation3.{0} 3,
      SameRecognitionData3 left right ∧
        left.span.measure 1 ≠ right.span.measure 1 ∧
        left.energyScale ≠ right.energyScale ∧
        ∀ event : PostingPair3 3,
          postingEventAction3 left.kinematics event =
            postingEventAction3 right.kinematics event := by
  let left : RecognitionPhysicalValuation3.{0} 3 :=
    unitRecognitionPhysicalValuation3
      (parentPhysicalChannelCarrier3 3)
  let right : RecognitionPhysicalValuation3.{0} 3 :=
    scalePhysicalValuation3
      2 (1 / 2) (by norm_num) (by norm_num) left
  refine
    ⟨left, right,
      scalePhysicalValuation_sameRecognitionData
        2 (1 / 2) (by norm_num) (by norm_num) left,
      ?_, ?_, ?_⟩
  · intro heq
    norm_num [left, right, unitRecognitionPhysicalValuation3,
      unitTickSpanMeasure, scalePhysicalValuation3,
      scaleTickSpanMeasure] at heq
  · intro heq
    norm_num [left, right, unitRecognitionPhysicalValuation3,
      scalePhysicalValuation3] at heq
  · intro event
    have haction :=
      scalePhysicalValuation_eventAction
        2 (1 / 2) (by norm_num) (by norm_num) left event
    change
      postingEventAction3 left.kinematics event =
        postingEventAction3 right.kinematics event
    rw [haction]
    norm_num
THEOREM weak_signature_and_action_admit_inverse_scales · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean
weak_signature_and_action_admit_inverse_scales · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean:413 
/-- Even preserving event action does not split the two physical units:
duration scale two and energy scale one-half leave their product unchanged. -/
theorem weak_signature_and_action_admit_inverse_scales :
    ∃ left right : RecognitionPhysicalValuation3.{0} 3,
      SameRecognitionData3 left right ∧
        left.span.measure 1 ≠ right.span.measure 1 ∧
        left.energyScale ≠ right.energyScale ∧
        ∀ event : PostingPair3 3,
          postingEventAction3 left.kinematics event =
            postingEventAction3 right.kinematics event := by
  let left : RecognitionPhysicalValuation3.{0} 3 :=
    unitRecognitionPhysicalValuation3
      (parentPhysicalChannelCarrier3 3)
  let right : RecognitionPhysicalValuation3.{0} 3 :=
    scalePhysicalValuation3
      2 (1 / 2) (by norm_num) (by norm_num) left
  refine
    ⟨left, right,
      scalePhysicalValuation_sameRecognitionData
        2 (1 / 2) (by norm_num) (by norm_num) left,
      ?_, ?_, ?_⟩
  · intro heq
    norm_num [left, right, unitRecognitionPhysicalValuation3,
      unitTickSpanMeasure, scalePhysicalValuation3,
      scaleTickSpanMeasure] at heq
  · intro heq
    norm_num [left, right, unitRecognitionPhysicalValuation3,
      scalePhysicalValuation3] at heq
  · intro event
    have haction :=
      scalePhysicalValuation_eventAction
        2 (1 / 2) (by norm_num) (by norm_num) left event
    change
      postingEventAction3 left.kinematics event =
        postingEventAction3 right.kinematics event
    rw [haction]
    norm_num
THEOREM no_weak_valuation_selects_absolute_scales · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean
no_weak_valuation_selects_absolute_scales · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean:292 
/-- No inhabitant of the weak structural signature has absolute-scale
uniqueness. Scaling duration by two preserves every Recognition datum but
changes the positive one-successor unit. -/
theorem no_weak_valuation_selects_absolute_scales
    {N : ℕ} [NeZero N]
    (valuation : RecognitionPhysicalValuation3 N) :
    ¬ RecognitionDataSelectsAbsoluteScales3 valuation := by
  intro hselect
  let scaled :=
    scalePhysicalValuation3
      2 1 (by norm_num) (by norm_num) valuation
  have hsame : SameRecognitionData3 valuation scaled :=
    scalePhysicalValuation_sameRecognitionData
      2 1 (by norm_num) (by norm_num) valuation
  have hscales := (hselect scaled hsame).1
  change
    valuation.span.measure 1 =
      2 * valuation.span.measure 1 at hscales
  nlinarith [valuation.span_unit_pos]
THEOREM additiveTickSpanMeasures_unique_up_to_positive_scale · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean
additiveTickSpanMeasures_unique_up_to_positive_scale · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean:127 
/-- Any two positive additive Tick-span measures differ by one positive
scalar. This is the real-valued image of NNO generator freedom. -/
theorem additiveTickSpanMeasures_unique_up_to_positive_scale
    (left right : AdditiveTickSpanMeasure)
    (hleft : 0 < left.measure 1)
    (hright : 0 < right.measure 1) :
    ∃ scale : ℝ, 0 < scale ∧
      ∀ n : ℕ,
        right.measure n = scale * left.measure n := by
  refine
    ⟨right.measure 1 / left.measure 1,
      div_pos hright hleft, ?_⟩
  intro n
  calc
    right.measure n =
        (n : ℝ) * right.measure 1 :=
      additiveTickSpanMeasure_eq_nat_mul_unit right n
    _ = (right.measure 1 / left.measure 1) *
          ((n : ℝ) * left.measure 1) := by
      field_simp [ne_of_gt hleft]
    _ = (right.measure 1 / left.measure 1) *
          left.measure n := by
      rw [additiveTickSpanMeasure_eq_nat_mul_unit left n]
HYPOTHESIS PostingDurationReadsOperationalTickCount3 · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean
PostingDurationReadsOperationalTickCount3 · IndisputableMonolith/Foundation/PairKernelPhysicalValuationInitialityS19.lean:547 
/-- Smallest live operational duration semantic. Its statement refers only to
the Recognition Tick count and the physical duration field; it names no
physical constant or desired action. -/
def PostingDurationReadsOperationalTickCount3
    {N : ℕ} [NeZero N]
    (kinematics : PostingEventKinematics3 N) : Prop :=
  ∀ event : RealizedPostingEvent3 N,
    kinematics.duration event.1 =
      recognitionTickCount (postingEventEndTick3 event) -
        recognitionTickCount (postingEventStartTick3 N)

What this page does not claim

The theorem does not claim that all valuations with the same action are physically equivalent. The theorem does not claim that absolute duration or energy scales are unobservable in principle. The theorem does not claim that the weak signature is the only set of conditions under which this freedom appears.

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