Encyclopedia Foundation Foundation Pair Kernel Event Action Ancestry S14 Event Derived Ledger Action Sca

ARTICLE 5 claims 4 theorems 1 model

Foundation Pair Kernel Event Action Ancestry S14 Event Derived Ledger Action Sca

A single number, the ratio of a physical event's action to its ledger cost, defines the scale that connects discrete accounting to continuous physics.

Verify this page

The event-derived ledger scale

The declaration eventDerivedLedgerActionScale defines a scale: the ratio of a physical event's action (energy multiplied by duration) to its exact ledger cost Jlog(1). In plain terms, it answers the question: if a primitive event in the ledger has a certain cost, what physical action does that cost correspond to? The scale is not chosen freely; it is derived from the event's own action and the fixed cost of a single posting.

The framework's library proves that every realized primitive posting pair has a minimal-cost posting step, a legal atomic tick, unit ledger cost, and exact ledger cost Jlog(1). This is a theorem: realizedPrimitivePostingPair_has_legalAtomicTick_and_cost. The same library proves that a primitive coherence event, one carrying a single coherence energy for one fundamental duration, has action equal to hbar (the reduced Planck constant). These two facts, the cost and the action, combine to define the scale: action divided by cost.

Two mathematically consistent branches follow from this definition. The identity branch maps the exact-J action units directly, selecting a drop of arcosh(1 + hbar). The ledger-normalized branch instead maps the raw ledger drop of 1 to the same physical action, using the scale hbar / Jlog(1). The two branches are not equivalent: the identity drop is not equal to 1. The framework proves that the identity branch forces the S13 native source, tangent, and Green package, while the ledger-normalized branch has source 2*sinh(1), tangent curvature cosh(1), and Green scale sinh(1)/cosh(1).

What the declaration does not claim is as important as what it proves. The event-to-energy-time attachment alone does not select the field unit map. Both branches are mathematically consistent, and the framework does not prove which one is physically realized. The declaration does not claim that the ledger scale is the only possible scale, nor that it is the physically correct one. It also does not claim that the physical action is identical to the dimensionless exact-J cost; they remain separate, connected only by the explicit linear conversion map.

In Recognition Science, this declaration is a stepping stone. It establishes that a scale exists and is well-defined, but it leaves open which branch of the two is the one the world uses. The choice between identity and ledger-normalized branches is a target for future derivation, not a settled result. The framework's library proves the consistency of both, but the physical selection remains open.

MODEL eventDerivedLedgerActionScale · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean
eventDerivedLedgerActionScale · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean:183 
/-- Per-event conversion ratio from the dimensionless unit posting cost to
physical energy-time action. The denominator is independently fixed by the
committed ledger constructor. -/
def eventDerivedLedgerActionScale
    {N : ℕ} [NeZero N]
    (kinematics : PostingEventKinematics3 N)
    (event : PostingPair3 N) : ℝ :=
  postingEventAction3 kinematics event / Cost.Jlog 1
THEOREM realizedPrimitivePostingPair_has_legalAtomicTick_and_cost · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean
realizedPrimitivePostingPair_has_legalAtomicTick_and_cost · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean:59 
/-- A realized primitive spatial event is an actual legal atomic ledger tick,
has the exact ledger cost `Jlog 1`, and is double-entry conserved. This is the
strongest committed ancestry before physical energy and duration are added. -/
theorem realizedPrimitivePostingPair_has_legalAtomicTick_and_cost
    {N : ℕ} [NeZero N]
    (event : PostingPair3 N)
    (hevent : event ∈ realizedPrimitivePostingPairs3 N) :
    ∃ A B : LedgerPostingAdjacency.LedgerState 3,
      PostingStep A B ∧
        LegalAtomicTick A B ∧
        JMinimalPostingStep A B ∧
        ledgerL1Cost A B = 1 ∧
        ledgerJlogCost A B = Cost.Jlog 1 ∧
        (∑ k : Fin (TorusCard3 N),
          divF (elementaryPosting event.1 event.2) k) = 0 := by
  obtain ⟨A, B, hpost, hmin, hdiv⟩ :=
    realizedPrimitivePostingPair_has_ledger_event event hevent
  have hlegal : LegalAtomicTick A B :=
    postingStep_implies_legalAtomicTick hpost
  refine ⟨A, B, hpost, hlegal, hmin, hlegal.2, ?_, hdiv⟩
  exact ledgerJlogCost_eq_Jlog1_of_postingStep hpost
THEOREM primitiveCoherenceEvent_action_eq_forced_configExponent · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean
primitiveCoherenceEvent_action_eq_forced_configExponent · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean:155 
/-- The exponent ancestry transports to the event action once the physical
event arrow is supplied. -/
theorem primitiveCoherenceEvent_action_eq_forced_configExponent
    {N : ℕ} [NeZero N]
    {kinematics : PostingEventKinematics3 N}
    (hcoherence :
      PrimitivePostingRealizesOneCoherenceEvent3 kinematics)
    {event : PostingPair3 N}
    (hevent : event ∈ realizedPrimitivePostingPairs3 N) :
    postingEventAction3 kinematics event =
      Constants.phi ^
        (-(GapDerivation.configDim GapDerivation.D : ℤ)) := by
  rw [primitiveCoherenceEvent_action_eq_hbar hcoherence hevent]
  exact GapDerivation.hbar_exponent_eq_configDim
THEOREM identityExactJMap_forces_S13_native_package · ledgerScaleExactJMap_forces_dropOne_package · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean
identityExactJMap_forces_S13_native_package · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean:333 
theorem identityExactJMap_forces_S13_native_package
    {N : ℕ} [NeZero N]
    {kinematics : PostingEventKinematics3 N}
    {drop sourceMagnitude : PostingPair3 N → ℝ}
    (hcoherence :
      PrimitivePostingRealizesOneCoherenceEvent3 kinematics)
    (hmap :
      MappedExactJDropRepresentsEventAction3 1 kinematics drop)
    (hsource :
      EventDropSourceIsExactJConjugate3 drop sourceMagnitude)
    {event : PostingPair3 N}
    (hevent : event ∈ realizedPrimitivePostingPairs3 N) :
    drop event = nativeActionCanonicalDrop ∧
      sourceMagnitude event = nativeExactJConjugateSource ∧
      2 * sourceMagnitude event = nativeOrderedExactJSource ∧
      Real.cosh (drop event) = 1 + Constants.hbar := by
  have hdrop :=
    identityExactJMap_selects_nativeActionCanonicalDrop
      hcoherence hmap hevent
  refine ⟨hdrop, ?_, ?_, ?_⟩
  · rw [hsource event hevent, hdrop]
    rfl
  · rw [hsource event hevent, hdrop]
    rfl
  · rw [hdrop]
    exact nativeActionCanonicalDrop_cosh
ledgerScaleExactJMap_forces_dropOne_package · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean:373 
theorem ledgerScaleExactJMap_forces_dropOne_package
    {N : ℕ} [NeZero N]
    {scale : ℝ}
    {kinematics : PostingEventKinematics3 N}
    {drop sourceMagnitude : PostingPair3 N → ℝ}
    (hcoherence :
      PrimitivePostingRealizesOneCoherenceEvent3 kinematics)
    (hscale : PrimitivePostingActionScaleLaw scale)
    (hmap :
      MappedExactJDropRepresentsEventAction3 scale kinematics drop)
    (hsource :
      EventDropSourceIsExactJConjugate3 drop sourceMagnitude)
    {event : PostingPair3 N}
    (hevent : event ∈ realizedPrimitivePostingPairs3 N) :
    drop event = 1 ∧
      sourceMagnitude event = exactJVariationalSource 1 ∧
      2 * sourceMagnitude event =
        ledgerNormalizedOrderedExactJSource ∧
      Real.cosh (drop event) =
        ledgerNormalizedExactJTangentCurvature := by
  have hdrop :=
    ledgerScaleExactJMap_selects_drop_one
      hcoherence hscale hmap hevent
  refine ⟨hdrop, ?_, ?_, ?_⟩
  · rw [hsource event hevent, hdrop]
  · rw [hsource event hevent, hdrop]
    rfl
  · rw [hdrop]
    rfl
THEOREM identityDrop_ne_ledgerNormalizedDrop · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean
identityDrop_ne_ledgerNormalizedDrop · IndisputableMonolith/Foundation/PairKernelEventActionAncestryS14.lean:315 
/-- The unit convention fork is nontrivial: the identity-map native drop and
the ledger-normalized drop are provably distinct. -/
theorem identityDrop_ne_ledgerNormalizedDrop :
    nativeActionCanonicalDrop ≠ 1 :=
  nativeActionCanonicalDrop_ne_ledgerUnit

What this page does not claim

The declaration does not claim that the identity branch is the physically realized one. The declaration does not claim that the ledger-normalized branch is the physically realized one. The declaration does not claim that the physical action is identical to the dimensionless exact-J cost without a conversion map.

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