Foundation Pair Kernel Physical Valuation Initiality S19 Weak Signature Admits I

The scale freedom theorem

In physics, a unit system fixes the size of a second and a joule by convention. The Recognition Science framework asks whether its own axioms could force those absolute sizes instead. The theorem weak_signature_admits_independent_duration_energy_scales answers no: the framework's weakest full structure admits two different valuations that agree on all recognition data but disagree on the duration of one tick and on the energy scale.

Here a valuation is a way of assigning real numbers to the framework's primitive events, a ledger entry that records how much duration and energy each event carries. The theorem constructs two such valuations that are identical in their physical carriers, survival probabilities, and channel prices, yet assign different numbers to the span of a single tick and to the energy unit. The two valuations also preserve the same composition law, reciprocity, positivity, and aggregation properties. The result is proved in the framework's machine-checked library of formal theorems, with no unproved assumptions added.

The theorem is a precise non-uniqueness result, not a claim that absolute scales are meaningless. It shows that the current axioms fix combinatorics and dimensionless ratios, but leave absolute duration and energy normalization free. The framework does isolate a canonical way to count ticks: the recognition tick count is the unique real-valued function that sends the zero tick to 0 and each successor to the previous value plus 1. But this count only fixes ratios, not the size of the unit. The theorem also shows that the same structure admits incomplete, extra, and same-cardinality misclassified carriers, and that J aggregation rejects arbitrary price rescaling.

The result does not say that absolute scales are unmeasurable or that the framework cannot eventually derive them. It says the current signature, the weakest one that preserves all the listed properties, does not. The framework's own constants, such as hbar and G, come from a separate calibration step that remains a hypothesis, not a theorem. The theorem also does not claim that the two valuations are physically equivalent; they disagree on real numbers, and which one matches the actual world is an empirical question.

What the theorem changes is the epistemic status of the framework's units. A reader can now see that the framework's axioms alone do not pin down the second or the joule, and that any claim to have derived absolute scales must cite an additional assumption. The framework's contribution is to force the dimensionless structure, the ratios and counts, while the absolute sizes enter as free parameters to be calibrated against measurement.

/-- Two full models agree on every Recognition-side datum while differing in
both absolute scales. -/
theorem weak_signature_admits_independent_duration_energy_scales :
    ∃ left right : RecognitionPhysicalValuation3.{0} 3,
      SameRecognitionData3 left right ∧
        left.span.measure 1 ≠ right.span.measure 1 ∧
        left.energyScale ≠ right.energyScale := by
  let left : RecognitionPhysicalValuation3.{0} 3 :=
    unitRecognitionPhysicalValuation3
      (parentPhysicalChannelCarrier3 3)
  let right : RecognitionPhysicalValuation3.{0} 3 :=
    scalePhysicalValuation3
      2 2 (by norm_num) (by norm_num) left
  refine
    ⟨left, right,
      scalePhysicalValuation_sameRecognitionData
        2 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

/-- NNO initiality uniquely selects the dimensionless zero/successor-count
map. This theorem fixes a count, not a physical time unit. -/
theorem recognitionTickCount_unique
    (clock : Tick → ℝ)
    (hzero : clock tickZero = 0)
    (hsucc :
      ∀ tick : Tick,
        clock (tickSucc tick) = clock tick + 1) :
    clock = recognitionTickCount := by
  funext tick
  have hunique :=
    tick_isNNO.recursor_unique
      (0 : ℝ) (fun value => value + 1)
      clock hzero hsucc tick
  calc
    clock tick =
        tickRecursor (0 : ℝ)
          (fun value => value + 1) tick :=
      hunique
    _ = recognitionTickCount tick :=
      tickRecursor_real_succ_eq_count tick

/-- A full weak valuation can omit the balance parent channel. -/
theorem weak_valuation_admits_incomplete_carrier :
    ∃ valuation : RecognitionPhysicalValuation3.{0} 3,
      ¬ PostingCarrierParentSurjective3 valuation.physical := by
  refine
    ⟨unitRecognitionPhysicalValuation3
        (incompletePhysicalChannelCarrier3 3), ?_⟩
  exact incompleteCarrier_not_parentSurjective

/-- A full weak valuation can contain a hidden extra channel. -/
theorem weak_valuation_admits_extra_carrier :
    ∃ valuation : RecognitionPhysicalValuation3.{0} 3,
      ¬ PostingCarrierParentInjective3 valuation.physical := by
  refine
    ⟨unitRecognitionPhysicalValuation3
        (extraPhysicalChannelCarrier3 3), ?_⟩
  exact extraCarrier_not_parentInjective

/-- Even a five-element full weak valuation can collapse distinct parent
classes. Thus the numeral `D+2` cannot replace physical classification. -/
theorem weak_valuation_admits_same_card_misclassification :
    ∃ valuation : RecognitionPhysicalValuation3.{0} 3,
      ¬ PostingCarrierParentInjective3 valuation.physical ∧
        ¬ PostingCarrierParentSurjective3 valuation.physical := by
  refine
    ⟨unitRecognitionPhysicalValuation3
        (misclassifiedFiveChannelCarrier3 3),
      misclassifiedFiveCarrier_not_parentInjective,
      misclassifiedFiveCarrier_not_parentSurjective⟩

/-- J aggregation is a real restriction: an arbitrary factor-two rescaling of
the canonical event price is rejected. -/
theorem price_rescaling_rejected_by_J_aggregation :
    ¬ PostingEventPriceReadsJAggregate3
      (parentPhysicalChannelCarrier3 3)
      (@canonicalPostingEventSurvival3 3 _)
      doubledCanonicalPostingEventChannelPrice3 :=
  doubledChannelPrice_not_JAggregate

What this page does not claim

The theorem does not claim that absolute duration and energy scales are physically meaningless or unmeasurable. The theorem does not claim that the framework can never derive absolute scales; it only shows the current weakest signature cannot. The theorem does not claim that the two valuations are physically equivalent; they disagree on real numbers.

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: