Foundation Pair Kernel Physical Unit Map S12 Primitive Posting Action Scale Cand

The scale candidate

In the Recognition Science framework, a ledger (a discrete record of events) assigns a cost to each posting. The framework's central cost function J(x) = (x + 1/x)/2 - 1 gives a unit posting a cost of Jlog 1, a specific positive number. The question is how to convert that abstract ledger cost into a physical quantity called action, which has units of energy times time. The framework defines a linear map: action equals a scale factor multiplied by the ledger cost.

The declaration primitivePostingActionScaleCandidate_satisfies proves that a particular scale factor, the candidate, makes this map send the unit posting cost exactly to the framework's constant hbar. The candidate is defined as hbar divided by Jlog 1. A companion theorem, primitivePostingActionScaleLaw_iff, proves this candidate is the unique scale with that property. The framework's library of machine-checked theorems shows this scale is positive, and that the identity scale (scale = 1) fails the requirement.

The same module proves what happens when this scale is applied to a physical field on a three-dimensional torus. If a field carries the mapped ledger action at this scale, then the field automatically carries the native action, and the difference between two posting events equals a canonical drop value. A further theorem shows that the source magnitude, defined as the variational conjugate of the action, is forced to a specific value at that drop. The source is the derivative of the action with respect to the field difference, and the framework proves it is sinh of the canonical drop, which equals sqrt(hbar * (hbar + 2)).

In Recognition Science, this chain of theorems establishes that the scale candidate is not arbitrary: it is the unique linear factor that bridges the ledger's discrete cost and the continuous action, and it selects a specific source strength. The framework presents this as a derivation from its axioms, not a fitted parameter. The theorems are checked in the framework's machine-checked library of formal theorems, with no unproved assumptions beyond the standard logical axioms.

What the declaration does not claim is equally precise. The docstring states explicitly that no electromagnetic, length, or SI interpretation is asserted. The scale is a mathematical bridge within the framework, not a measured physical constant. The reciprocal of hbar, phi^5, is proved distinct from the exact-J conjugate source, so the framework does not conflate two different mathematical duals. The physical meaning of the source, whether it corresponds to a Gauss source or some other physical quantity, remains an explicit semantic arrow, not a proved identification.

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

theorem primitivePostingActionScaleLaw_iff
    (scale : ℝ) :
    PrimitivePostingActionScaleLaw scale ↔
      scale = primitivePostingActionScaleCandidate := by
  unfold PrimitivePostingActionScaleLaw ledgerToActionUnitMap
    primitivePostingActionScaleCandidate
  constructor
  · intro h
    apply (eq_div_iff (ne_of_gt ledgerJlogUnitCost_pos)).mpr
    simpa [mul_comm] using h
  · intro h
    subst scale
    field_simp [ne_of_gt ledgerJlogUnitCost_pos]

theorem primitivePostingActionScaleCandidate_pos :
    0 < primitivePostingActionScaleCandidate := by
  unfold primitivePostingActionScaleCandidate
  exact div_pos Constants.hbar_pos 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)

theorem nativeAction_and_exactJConjugate_force_source
    {N : ℕ} [NeZero N]
    {field : Fin (TorusCard3 N) → ℝ}
    {sourceMagnitude : PostingPair3 N → ℝ}
    (hfield : RealizedPostingFieldCarriesNativeAction3 field)
    (hsource : PostingSourceIsExactJConjugate3 field sourceMagnitude)
    {event : PostingPair3 N}
    (hevent : event ∈ realizedPrimitivePostingPairs3 N)
    (hne : event.1 ≠ event.2) :
    sourceMagnitude event = nativeExactJConjugateSource := by
  rw [hsource event hevent hne,
    realizedPostingFieldCarriesNativeAction_selects_canonicalDrop
      hfield hevent hne]
  rfl

What this page does not claim

No electromagnetic, length, or SI interpretation is asserted for the scale or the source. The reciprocal of hbar, phi^5, is not the same as the exact-J conjugate source. The physical meaning of the source as a Gauss source or other physical quantity is not proved.

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: