Encyclopedia Foundation Foundation Absolute Scale Event Pricing Join

ARTICLE 4 claims 4 theorems

Foundation Absolute Scale Event Pricing Join

A machine-checked proof that one unit of duration and one unit of energy emerge from counting ledger steps, with no unit supplied in advance.

Verify this page

The pricing join

In Recognition Science, a framework that derives physical structure from the cost of recording events, the ledger (a discrete record of events) is the fundamental object. The absolute scale event pricing join is a module in the framework's machine-checked library of formal theorems that answers a specific question: given a single realized event, how long does it last and how much energy does it carry? The answer is not chosen freely. The module proves that both the duration and the energy scale are forced to specific values by the structure of the ledger itself.

The duration result is the simpler of the two. The framework models a physical event as a transition in the ledger, a posting step. The module defines a law stating that the duration of a realized posting is priced by the number of committed minimum-cost posting transitions that realize it. A separate committed theorem establishes that this cost is exactly one for every posting step. The proof then shows that this law forces the operational one-successor duration: each event lasts exactly one fundamental tick, the base unit of time in the framework. The argument relies on the natural-number count being rigid; no positive real unit can survive the casting into the real numbers.

The energy result is more involved. The module models energy as a multiplicative recognition channel-block attachment. Energy through disjoint independent channel blocks composes multiplicatively, a shadow of the log-additivity of the framework's core cost function. Multiplicativity forces the empty-block value to one, which is exactly the uniform event-price scale of one. A rescaled attachment fails composition because the equation scale = scale² has no positive solution except one. The self-similarity fixed point for a single channel forces its attenuation to be the reciprocal of the golden ratio, phi⁻¹. For a complete carrier of D+2 channels, the event is priced at phi⁻⁵.

The module then shows that these two laws, the duration law and the energy law, together force the coherence-event arrow and native action. It also rejects both native calibration directions: any positive duration-energy rescaling of a law-satisfying kinematics that still satisfies the law must have both scales equal to one. The canonical mechanism satisfies both laws. The stretched-duration decoy fails the duration law, and the doubled-energy decoy fails the energy law on every carrier of every dimension, because no integer power of phi equals two.

The honesty of the result is precise. The two laws themselves are supplied physical identifications, hypotheses about how the world maps onto the ledger. What is new and proved as a theorem is that the one-successor duration and the unit price scale are now forced from these parents, which carry no unit datum, and that both decoys die. The external dimensional calibration orbit remains open. The module contains no sorry, no new axiom, no SI input, and no fitted constant.

THEOREM mutationCountPricing_implies_operationalTickCount · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
mutationCountPricing_implies_operationalTickCount · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:140 
/-- Mutation-count pricing forces S19's operational one-successor duration
readout: the physical duration is the NNO tick-count interval. -/
theorem mutationCountPricing_implies_operationalTickCount
    {N : ℕ} [NeZero N]
    {kinematics : PostingEventKinematics3 N}
    (hlaw : PostingDurationPricesCommittedMutationCount3 kinematics) :
    PostingDurationReadsOperationalTickCount3 kinematics := by
  intro event
  obtain ⟨A, B, hpost, _, _, hdur⟩ := hlaw event
  rw [(postingStep_implies_legalAtomicTick hpost).2] at hdur
  calc
    kinematics.duration event.1 = 1 := by
      rw [hdur]
      norm_num
    _ = recognitionTickCount (postingEventEndTick3 event) -
        recognitionTickCount (postingEventStartTick3 N) := by
      rw [postingEventEndTick3_eq_succ]
      simp [recognitionTickCount, tickSucc]
THEOREM channelBlockEnergyLaw_forces_unit_price_scale · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
channelBlockEnergyLaw_forces_unit_price_scale · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:332 
/-- **The S18 residual closes: the uniform event-price scale is forced to
one.** Against any S18 aggregate price built from a self-similar survival on
the same carrier, a kinematics obeying the channel-block energy law reads the
price exactly, and its uniform scale representation is scale one. -/
theorem channelBlockEnergyLaw_forces_unit_price_scale
    {N : ℕ} [NeZero N]
    {physical : PostingPhysicalChannelCarrier3 N}
    {survival : PostingEventSurvival3 N}
    {price : PostingEventChannelPrice3 N}
    {channelEnergy : PostingEventChannelEnergy3 N}
    {kinematics : PostingEventKinematics3 N}
    (hself : PostingEventSurvivalSelfSimilar3 survival)
    (haggregate :
      PostingEventPriceReadsJAggregate3 physical survival price)
    (hlaw :
      PostingEnergyReadsChannelBlockEnergy3
        physical channelEnergy kinematics) :
    PostingEnergyReadsEventChannelPrice3 price kinematics ∧
      PostingEnergyHasUniformPriceScale3 1 price kinematics := by
  have hread :
      PostingEnergyReadsEventChannelPrice3 price kinematics := by
    intro event
    rw [channelBlockEnergyLaw_energy_eq_phi_zpow hlaw event,
      eventSurvivalAndAggregate_price_eq_phi_neg_dimension
        hself haggregate event]
  refine ⟨hread, ?_⟩
  intro event
  rw [hread event, one_mul]
THEOREM channelBlockEnergyLaw_energy_eq_phi_zpow · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
channelBlockEnergyLaw_energy_eq_phi_zpow · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:297 
/-- The energy law prices every event at `phi` to the negative carrier
dimension, with no residual scalar. -/
theorem channelBlockEnergyLaw_energy_eq_phi_zpow
    {N : ℕ} [NeZero N]
    {physical : PostingPhysicalChannelCarrier3 N}
    {channelEnergy : PostingEventChannelEnergy3 N}
    {kinematics : PostingEventKinematics3 N}
    (hlaw :
      PostingEnergyReadsChannelBlockEnergy3
        physical channelEnergy kinematics)
    (event : RealizedPostingEvent3 N) :
    kinematics.energy event.1 =
      Constants.phi ^
        (-(physicalPostingCarrierDimension3 physical event : ℤ)) := by
  rw [hlaw event]
  exact channelEnergy.blockEnergy_forced event _
THEOREM operationalEventPricing_kills_native_rescaling · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
operationalEventPricing_kills_native_rescaling · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:560 
/-- **The composed law kills both native rescaling directions.** If a
kinematics satisfies the join over a complete carrier and its positive
duration-energy rescaling also satisfies the join over a complete carrier,
then both scales are one. This is the event-level counterpart of the S19
two-parameter orbit: the orbit cannot move a law-satisfying kinematics. -/
theorem operationalEventPricing_kills_native_rescaling
    {kinematics : PostingEventKinematics3 3}
    {physical physical' : PostingPhysicalChannelCarrier3 3}
    {channelEnergy channelEnergy' : PostingEventChannelEnergy3 3}
    (durationScale energyScale : ℝ)
    (hdurationPos : 0 < durationScale)
    (henergyPos : 0 < energyScale)
    (hcomplete : PostingCarrierCoherenceComplete3 physical)
    (hcomplete' : PostingCarrierCoherenceComplete3 physical')
    (hjoin :
      OperationalEventPricingJoin3
        physical channelEnergy kinematics)
    (hjoinScaled :
      OperationalEventPricingJoin3
        physical' channelEnergy'
        (scalePostingEventKinematics3
          durationScale energyScale hdurationPos henergyPos
          kinematics)) :
    durationScale = 1 ∧ energyScale = 1 := by
  obtain ⟨pair, hpair⟩ := realizedPrimitivePostingPair3_exists
  have hdurBase :=
    mutationCountPricing_implies_fundamentalTick hjoin.1 pair hpair
  have hdurScaled :=
    mutationCountPricing_implies_fundamentalTick
      hjoinScaled.1 pair hpair
  have henergyBase :=
    channelBlockEnergyLaw_implies_coherenceEnergy
      hcomplete hjoin.2 pair hpair
  have henergyScaled :=
    channelBlockEnergyLaw_implies_coherenceEnergy
      hcomplete' hjoinScaled.2 pair hpair
  change
    durationScale * kinematics.duration pair =
      Constants.tau0 at hdurScaled
  change
    energyScale * kinematics.energy pair =
      Constants.E_coh at henergyScaled
  rw [hdurBase] at hdurScaled
  rw [henergyBase] at henergyScaled
  constructor
  · refine mul_right_cancel₀ (ne_of_gt Constants.tau0_pos) ?_
    rw [one_mul]
    exact hdurScaled
  · refine mul_right_cancel₀ (ne_of_gt Constants.E_coh_pos) ?_
    rw [one_mul]
    exact henergyScaled

What this page does not claim

The two pricing laws are not derived; they are supplied physical identifications. This module does not establish the external dimensional calibration of the framework. The result does not claim that the golden ratio itself is derived here; it appears as a fixed point of the self-similarity law.

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