Foundation Pair Kernel Event Action Ancestry S14 Identity Exact Jmap Selects Nat

The identity map's selection

In the Recognition Science framework, a primitive event is a single realized posting in a double-entry ledger, a discrete record of events. The framework's library, a machine-checked collection of formal theorems, proves that every such event carries one coherence energy E_coh for one fundamental duration tau0, so its physical action, energy times duration, is exactly hbar. The question is how to convert that physical action into the ledger's own dimensionless cost scale, and the theorem identityExactJMap_selects_nativeActionCanonicalDrop answers one branch of that question.

The theorem states that if you choose the identity map, meaning you use the exact-J cost value directly as the unit of action, then the drop, the ledger cost assigned to the event, is forced to be the constant nativeActionCanonicalDrop, whose value is arcosh(1 + hbar), about 0.9865. The same choice also forces the source magnitude to be the conjugate source and the ordered source to be twice that, and it yields the relation cosh(drop) = 1 + hbar. This is a proved theorem in the framework's library, with no unproved axioms beyond the standard three.

The theorem does not claim that this identity choice is the only consistent one. The library proves a second, mathematically consistent branch: a ledger-normalized scale, hbar divided by Jlog(1), maps the raw ledger drop of 1 to the same physical action. On that branch the source is 2*sinh(1), the tangent curvature is cosh(1), and the Green scale is sinh(1)/cosh(1). The identity branch and the ledger-normalized branch are genuinely different, and the identity drop is provably not equal to 1. So the event-to-energy-time attachment alone does not select the field unit map; both branches are proved consistent.

The framework's library further shows that the identity branch is the one that leads to the S13 native source, tangent, and Green package, while the ledger-normalized branch leads to a different package. The theorem also proves that the coherent event model, with energy E_coh and duration tau0, does not make the identity ledger map work, because the scale law fails for scale 1. This is a structural result about the framework's internal consistency, not a claim about which branch is physically realized in nature.

What the theorem does not claim is that the identity map is the correct physical choice. It proves a conditional: if you take the identity exact-J action units, then the drop is forced to be nativeActionCanonicalDrop. It does not prove that the identity map is the one nature uses, nor does it derive the value of hbar itself, which is a framework constant. The theorem also does not claim that the ledger-normalized branch is inconsistent; it is proved consistent as well. The choice between the two branches remains open, and the library explicitly notes that event-to-energy-time attachment alone does not select the field unit map.

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

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

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

/-- Unit-map countermodel: a coherent-event MODEL is compatible with the
proved failure of the identity ledger conversion. -/
theorem coherentEventModel_does_not_make_identityLedgerMap :
    PrimitivePostingRealizesOneCoherenceEvent3
        (canonicalCoherenceKinematics3 3) ∧
      ¬ PrimitivePostingActionScaleLaw 1 :=
  ⟨canonicalCoherenceKinematics_satisfies_model,
    identityUnitMap_fails_nativeAction⟩

What this page does not claim

The identity map is the physically correct choice. The ledger-normalized branch is inconsistent. The value of hbar is derived in this theorem.

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: