Foundation Pair Kernel Physical Unit Map S12 Ledger Mapped Posting Action3 Accou

A constant action per ledger event

The declaration establishes that the mapped action attached to a posting event is a constant, independent of which specific pair of ledger entries the event involves. In the framework's terms, a ledger, a discrete record of events, assigns each posting a cost. The theorem ledgerMappedPostingAction3_account_invariant proves that this mapped cost is the same for any two posting pairs, for any chosen scale. It is a statement of uniformity: the ledger does not privilege one event over another at this stage of the construction.

The proof is immediate from the definition. The mapped action is the product of a scale factor and the cost of a single unit posting, and that unit cost is itself a fixed number. The theorem's content is therefore not that some particular scale is correct, but that the mapping from ledger cost to action is a linear rule with a single adjustable constant. The scale is not yet fixed by this theorem alone.

In Recognition Science, this uniformity is a step toward connecting the ledger to physical quantities. A separate theorem shows that a specific scale, the primitive posting action scale candidate, makes the mapped action equal to the framework's constant hbar. Another theorem shows that the identity scale, scale equal to one, fails to do so. The invariant thus prepares the ground for choosing a scale, but it does not itself make that choice.

The declaration does not claim that any particular scale is the physically correct one. It does not assert that the ledger cost of a unit posting equals hbar; that is a separate condition, the primitive posting action scale law, which is not part of this theorem. It also does not claim that the mapped action is the native action, the action expressed directly in the framework's own units, without the intervening scale. The invariant is a statement about the form of the mapping, not about its numerical value.

/-- Scalar unit maps are account-label invariant for every scale. This
invariance transports a selected map but cannot select its scale. -/
theorem ledgerMappedPostingAction3_account_invariant
    {N : ℕ} [NeZero N]
    (scale : ℝ)
    (left right : PostingPair3 N) :
    ledgerMappedPostingAction3 scale left =
      ledgerMappedPostingAction3 scale right := rfl

/-- Scalar unit maps are account-label invariant for every scale. This
invariance transports a selected map but cannot select its scale. -/
theorem ledgerMappedPostingAction3_account_invariant
    {N : ℕ} [NeZero N]
    (scale : ℝ)
    (left right : PostingPair3 N) :
    ledgerMappedPostingAction3 scale left =
      ledgerMappedPostingAction3 scale right := rfl

/-- Event action obtained by applying one scalar unit map to the integer
posting cost. -/
def ledgerMappedPostingAction3
    {N : ℕ} [NeZero N]
    (scale : ℝ) (_event : PostingPair3 N) : ℝ :=
  ledgerToActionUnitMap scale (Cost.Jlog 1)

theorem primitivePostingActionScaleCandidate_satisfies :
    PrimitivePostingActionScaleLaw
      primitivePostingActionScaleCandidate := by
  unfold PrimitivePostingActionScaleLaw ledgerToActionUnitMap
    primitivePostingActionScaleCandidate
  field_simp [ne_of_gt ledgerJlogUnitCost_pos]

/-- Identity conversion is ruled out by S11. -/
theorem identityUnitMap_fails_nativeAction :
    ¬ PrimitivePostingActionScaleLaw 1 := by
  intro h
  unfold PrimitivePostingActionScaleLaw ledgerToActionUnitMap at h
  exact ledgerJlogUnitCost_ne_constants_hbar (by simpa using h)

What this page does not claim

The declaration does not claim that any particular scale is the physically correct one. It does not assert that the ledger cost of a unit posting equals hbar. It does not claim that the mapped action is the native action without an intervening scale.

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/PairKernelPhysicalUnitMapS12.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: