Encyclopedia Foundation Foundation Absolute Scale Event Pricing Join Doubled Coherent Valuation Kinemati

ARTICLE 4 claims 3 theorems 1 hypothesis

Foundation Absolute Scale Event Pricing Join Doubled Coherent Valuation Kinemati

A proposed alternative to the standard pricing rule fails a basic consistency test, and the reason is that no power of the golden ratio equals two.

Verify this page

The doubled-energy decoy

The golden ratio, often written φ, is the number that solves r² = r + 1, approximately 1.618. It appears throughout mathematics, from the geometry of pentagons to the growth of Fibonacci sequences. In the Recognition Science framework, this constant is not just a geometric curiosity; it is the unique self-similar scaling forced by the framework's core cost function. The framework's library, a machine-checked collection of formal theorems, proves that any rule for assigning energy to an event must be built from powers of φ.

One proposed alternative, called the doubled-energy kinematics, tries to assign twice the standard energy to each event. The declaration doubledCoherentValuation_kinematics_fails_join is a formal theorem stating that this alternative fails a fundamental consistency requirement. The requirement, called the event pricing join, has two parts. First, the duration of an event must be priced by the number of underlying ledger mutations, a discrete count. Second, the energy of an event must be priced by a multiplicative rule across independent channel blocks, where each block attenuates by the reciprocal self-similarity fixed point, which is 1/φ.

The doubled-energy alternative fails the energy law. The proof hinges on a simple fact: no integer power of φ equals two. Since the energy of a carrier with D+2 channels must be φ to the power of -(D+2), the doubled value would require a power of φ equal to two, which is impossible. The theorem phi_zpow_ne_two establishes this directly. The doubled-energy decoy therefore dies on every carrier of every dimension.

This failure is not a flaw in the framework but a feature. It demonstrates that the pricing rules are rigid: they cannot be rescaled arbitrarily. The theorem operationalEventPricing_kills_native_rescaling proves that any positive rescaling of both duration and energy that still satisfies the join must have both scales equal to one. The only consistent pricing is the canonical one, where the one-successor duration is a single fundamental tick and the unit price scale is one.

The honesty of the result matters. The two laws themselves, that duration prices mutation count and energy prices channel blocks, are supplied physical identifications, not derived from first principles. They are hypotheses about how the framework connects to physics. What is proved is that given those laws, the doubled-energy alternative is impossible, and the canonical pricing is forced. The framework does not claim to derive the external dimensional calibration orbit, which remains an open target.

THEOREM doubledCoherentValuation_kinematics_fails_join · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
doubledCoherentValuation_kinematics_fails_join · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:539 
/-- The doubled-action valuation's kinematics fails the composed law on every
carrier and every attachment: its duration contradicts the unit mutation
count. -/
theorem doubledCoherentValuation_kinematics_fails_join
    (physical : PostingPhysicalChannelCarrier3 3)
    (channelEnergy : PostingEventChannelEnergy3 3) :
    ¬ OperationalEventPricingJoin3
      physical channelEnergy
      doubledCoherentActionValuation3.kinematics := by
  rintro ⟨hduration, _⟩
  obtain ⟨pair, hpair⟩ := realizedPrimitivePostingPair3_exists
  obtain ⟨A, B, hpost, _, _, hdur⟩ :=
    hduration ⟨pair, hpair⟩
  rw [(postingStep_implies_legalAtomicTick hpost).2] at hdur
  norm_num [doubledCoherentActionValuation3, coherentEventValuation3,
    scalePhysicalValuation3, scalePostingEventKinematics3,
    unitRecognitionPhysicalValuation3, unitPostingEventKinematics3,
    Constants.tau0, Constants.tick] at hdur
THEOREM phi_zpow_ne_two · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
phi_zpow_ne_two · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:86 
/-- No integer power of `phi` equals two. This is the arithmetic wall that
kills the doubled-energy decoy on every carrier dimension. -/
theorem phi_zpow_ne_two (k : ℤ) : Constants.phi ^ k ≠ 2 := by
  intro hk
  rcases le_or_gt k 1 with hle | hgt
  · have hbound : Constants.phi ^ k ≤ Constants.phi ^ (1 : ℤ) :=
      zpow_le_zpow_right₀ (le_of_lt Constants.one_lt_phi) hle
    rw [zpow_one, hk] at hbound
    linarith [Constants.phi_lt_onePointSixTwo]
  · have h2le : (2 : ℤ) ≤ k := by omega
    have hbound : Constants.phi ^ (2 : ℤ) ≤ Constants.phi ^ k :=
      zpow_le_zpow_right₀ (le_of_lt Constants.one_lt_phi) h2le
    have hphi2 : Constants.phi ^ (2 : ℤ) =
        Constants.phi * Constants.phi := by
      rw [show (2 : ℤ) = 1 + 1 by norm_num,
        zpow_add₀ Constants.phi_ne_zero, zpow_one]
    rw [hphi2, hk] at hbound
    nlinarith [Constants.phi_gt_onePointSixOne]
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
HYPOTHESIS PostingDurationPricesCommittedMutationCount3 · PostingEnergyReadsChannelBlockEnergy3 · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
PostingDurationPricesCommittedMutationCount3 · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:107 
/-- Target-blind operational clock law. The physical duration of one realized
posting equals the real image of the ledger mutation count of one underlying
committed minimum-J posting transition realizing it, with the event's
double-entry conservation witness carried alongside. The right-hand side is
a natural-number count produced by the committed production constructor. No
named time constant, coherence energy, action quantum, or desired readout
equality occurs in this definition. -/
def PostingDurationPricesCommittedMutationCount3
    {N : ℕ} [NeZero N]
    (kinematics : PostingEventKinematics3 N) : Prop :=
  ∀ event : RealizedPostingEvent3 N,
    ∃ A B : LedgerPostingAdjacency.LedgerState 3,
      PostingStep A B ∧
        JMinimalPostingStep A B ∧
        (∑ k : Fin (TorusCard3 N),
          divF (elementaryPosting event.1.1 event.1.2) k) = 0 ∧
        kinematics.duration event.1 =
          (ledgerL1Cost A B : ℝ)
PostingEnergyReadsChannelBlockEnergy3 · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:284 
/-- Target-blind physical energy law. One realized posting's energy is its
multiplicative self-similar channel-block energy through its classified
physical carrier. No `E_coh`, `hbar`, price field, or scale field occurs. -/
def PostingEnergyReadsChannelBlockEnergy3
    {N : ℕ} [NeZero N]
    (physical : PostingPhysicalChannelCarrier3 N)
    (channelEnergy : PostingEventChannelEnergy3 N)
    (kinematics : PostingEventKinematics3 N) : Prop :=
  ∀ event : RealizedPostingEvent3 N,
    kinematics.energy event.1 =
      channelEnergy.blockEnergy event
        (physicalPostingCarrierDimension3 physical event)

What this page does not claim

The doubled-energy kinematics is the only alternative that fails the join. The framework derives the physical laws of duration and energy pricing from first principles. The external dimensional calibration orbit is closed by this result.

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