Encyclopedia Foundation Foundation Absolute Scale Event Pricing Join Channel Block Energy Law Implies Co

ARTICLE 5 claims 5 theorems

Foundation Absolute Scale Event Pricing Join Channel Block Energy Law Implies Co

A new theorem in a machine-checked library forces the energy of a single event to a specific value, and rules out the obvious alternative.

Verify this page

The energy law

In physics, an event is something that happens at a place and a time. A flash of light, a particle decaying, a ledger entry being written: each is an event. The question at stake here is whether the energy of such an event is a free parameter or a forced quantity. The theorem channelBlockEnergyLaw_implies_coherenceEnergy states that if a physical system obeys a specific energy-composition law, then the energy of a realized posting is not arbitrary: it must equal the value that the framework's coherence invariant requires.

The law in question is a composition rule. It says that the energy of a posting through two independent channel blocks is the product of the energies through each block. This is the same multiplicative structure that appears in the J-cost's log-additivity shadow. The theorem proves that this law, together with the condition that the carrier is complete, forces the energy of a realized posting to be exactly phi to the power of the negative carrier dimension. For a single channel, this is phi to the minus one, about 0.618. For the full D+2 carrier, the energy is phi to the minus five, about 0.0902.

The proof does not start from a desired answer. The energy law does not name a price field, a scale field, or any constant like hbar. The constants appear only in the derived conclusion. The theorem shows that the law itself is enough to pin down the energy. It also shows that the obvious decoy fails: a doubled-energy kinematics cannot satisfy the law on any carrier, because no integer power of phi equals two. The law rejects the rescaling, and the join with the duration law forces both scales to one.

What the theorem does not claim is important. The energy law is a supplied physical identification, a hypothesis about how energy attaches to channel blocks. The theorem proves what follows from that hypothesis, not the hypothesis itself. The external dimensional calibration orbit remains open. The theorem also does not claim that the framework derives the fine-structure constant or any other measured coupling. It is a structural result about the consequences of a chosen law.

The consequence is concrete. The framework's account of a single event now has a forced energy, not a fitted one. The reader can see that the energy of an event is not a free parameter in this account, but a number that the composition law itself selects. That is the difference between a model with a dial and a model with a proof.

THEOREM channelBlockEnergyLaw_implies_coherenceEnergy · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
channelBlockEnergyLaw_implies_coherenceEnergy · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:314 
/-- With a coherence-complete carrier, the energy law forces the coherence
energy per event. `E_coh` appears only in the conclusion. -/
theorem channelBlockEnergyLaw_implies_coherenceEnergy
    {N : ℕ} [NeZero N]
    {physical : PostingPhysicalChannelCarrier3 N}
    {channelEnergy : PostingEventChannelEnergy3 N}
    {kinematics : PostingEventKinematics3 N}
    (hcomplete : PostingCarrierCoherenceComplete3 physical)
    (hlaw :
      PostingEnergyReadsChannelBlockEnergy3
        physical channelEnergy kinematics) :
    RealizedPostingCarriesCoherenceEnergy3 kinematics := by
  intro event hevent
  let realized : RealizedPostingEvent3 N := ⟨event, hevent⟩
  rw [channelBlockEnergyLaw_energy_eq_phi_zpow hlaw realized,
    completeCarrier_dimension_eq_configDim hcomplete realized]
  exact GapDerivation.Constants_E_coh_eq_configDim.symm
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 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 channelBlockEnergyLaw_implies_coherenceEnergy · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
channelBlockEnergyLaw_implies_coherenceEnergy · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:314 
/-- With a coherence-complete carrier, the energy law forces the coherence
energy per event. `E_coh` appears only in the conclusion. -/
theorem channelBlockEnergyLaw_implies_coherenceEnergy
    {N : ℕ} [NeZero N]
    {physical : PostingPhysicalChannelCarrier3 N}
    {channelEnergy : PostingEventChannelEnergy3 N}
    {kinematics : PostingEventKinematics3 N}
    (hcomplete : PostingCarrierCoherenceComplete3 physical)
    (hlaw :
      PostingEnergyReadsChannelBlockEnergy3
        physical channelEnergy kinematics) :
    RealizedPostingCarriesCoherenceEnergy3 kinematics := by
  intro event hevent
  let realized : RealizedPostingEvent3 N := ⟨event, hevent⟩
  rw [channelBlockEnergyLaw_energy_eq_phi_zpow hlaw realized,
    completeCarrier_dimension_eq_configDim hcomplete realized]
  exact GapDerivation.Constants_E_coh_eq_configDim.symm
THEOREM doubledEnergy_not_channelBlockEnergy · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean
doubledEnergy_not_channelBlockEnergy · IndisputableMonolith/Foundation/AbsoluteScaleEventPricingJoin.lean:395 
/-- Energy decoy rejection, strong form: the doubled-energy kinematics fails
the channel-block energy law on **every** carrier of every dimension and
every attachment, because no integer power of `phi` equals two. -/
theorem doubledEnergy_not_channelBlockEnergy
    (physical : PostingPhysicalChannelCarrier3 3)
    (channelEnergy : PostingEventChannelEnergy3 3) :
    ¬ PostingEnergyReadsChannelBlockEnergy3
      physical channelEnergy (doubledEnergyKinematics3 3) := by
  intro hlaw
  obtain ⟨pair, hpair⟩ := realizedPrimitivePostingPair3_exists
  have h :=
    channelBlockEnergyLaw_energy_eq_phi_zpow hlaw ⟨pair, hpair⟩
  set n : ℕ :=
    physicalPostingCarrierDimension3 physical ⟨pair, hpair⟩ with hn
  change 2 * Constants.E_coh = Constants.phi ^ (-(n : ℤ)) at h
  rw [GapDerivation.Constants_E_coh_eq_configDim,
    GapDerivation.configDim_at_D3] at h
  have hcast : (((5 : ℕ) : ℤ)) = (5 : ℤ) := by norm_num
  rw [hcast] at h
  have h2 : Constants.phi ^ (-(n : ℤ) + 5) = 2 := by
    calc
      Constants.phi ^ (-(n : ℤ) + 5) =
          Constants.phi ^ (-(n : ℤ)) *
            Constants.phi ^ (5 : ℤ) :=
        zpow_add₀ Constants.phi_ne_zero _ _
      _ = (2 * Constants.phi ^ (-(5 : ℤ))) *
            Constants.phi ^ (5 : ℤ) := by
        rw [← h]
      _ = 2 * Constants.phi ^ (-(5 : ℤ) + 5) := by
        rw [mul_assoc, ← zpow_add₀ Constants.phi_ne_zero]
      _ = 2 := by
        rw [show (-(5 : ℤ) + 5) = 0 by norm_num, zpow_zero, mul_one]
  exact phi_zpow_ne_two (-(n : ℤ) + 5) h2

What this page does not claim

The energy-composition law itself is a supplied physical identification, not a theorem. The theorem does not derive the fine-structure constant or any other measured coupling. The external dimensional calibration orbit remains open, not settled 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