Foundation Pair Kernel Physical Posting Attachment S10 Physical Posting Magnitud

The relabeling invariance

A ledger, a discrete record of events, must assign a magnitude to each of its elementary postings. The theorem physicalPostingMagnitude_account_relabeling_invariant states that if a posting magnitude assignment satisfies two conditions, then the magnitude is the same for every realized primitive posting event. The two conditions are that the posting carries the native action quantum and that the source magnitude is the action-dual of the posting action. The result is established in the machine-checked library of formal theorems, meaning the conclusion follows from the kernel's logic alone.

The theorem does not claim that the two conditions are actually met by any physical posting. The library leaves open whether a posting carries the native action quantum, and whether the source coordinate is the action-dual. Those two identifications remain OPEN targets. The theorem is conditional: if the conditions hold, then the magnitude is invariant. The numerical consequence, that the magnitude is phi to the fifth power, is a conditional theorem, not an unconditional fact.

This invariance is a consistency property. It says that the framework's account of physical posting magnitudes is not sensitive to the arbitrary choice of which event is called first. This is a necessary property for any coherent ledger, but it is not by itself a derivation of the magnitude's value. The value follows only when the two identification conditions are supplied.

/-- The attached source magnitude is invariant under account/event relabeling:
every realized posting receives the same value. -/
theorem physicalPostingMagnitude_account_relabeling_invariant
    {N : ℕ} [NeZero N]
    {postingAction sourceMagnitude : PostingPair3 N → ℝ}
    (hattach :
      PhysicalPostingMagnitudeAttachment3 postingAction sourceMagnitude)
    {event₁ event₂ : PostingPair3 N}
    (h₁ : event₁ ∈ realizedPrimitivePostingPairs3 N)
    (h₂ : event₂ ∈ realizedPrimitivePostingPairs3 N) :
    sourceMagnitude event₁ = sourceMagnitude event₂ := by
  rw [physicalPostingAttachment_forces_nativeActionQuantumInv
      hattach h₁,
    physicalPostingAttachment_forces_nativeActionQuantumInv
      hattach h₂]

/-- Exact S10 physical attachment residual. Both semantic arrows must be
supplied: event to action, then source coordinate to the dual action unit. -/
def PhysicalPostingMagnitudeAttachment3
    {N : ℕ} [NeZero N]
    (postingAction sourceMagnitude : PostingPair3 N → ℝ) : Prop :=
  MinimumJPostingCarriesNativeAction3 postingAction ∧
    PostingSourceIsActionDual3 postingAction sourceMagnitude

What this page does not claim

The theorem does not assert that the two identification conditions are satisfied by any physical posting. The theorem does not derive the numerical value of the posting magnitude unconditionally. The theorem does not establish that the posting magnitude is the same for non-realized posting events.

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