Encyclopedia Foundation Foundation Pair Kernel Scale Bearing Self Dual Posting Law

ARTICLE 5 claims 5 theorems

Foundation Pair Kernel Scale Bearing Self Dual Posting Law

A new law in Recognition Science fixes the one scale at which a primitive event can be posted, and proves that any other scale is forbidden.

Verify this page

The posting law

The posting law is a rule for how a primitive recognition event, a single entry in the ledger, is recorded. The ledger is the framework's discrete record of events. The law combines two costs: the cost of changing the event's scale, and the cost of the event's internal field. It accepts no external parameters, no clock weight, and no lattice spacing. The scale itself, the field source, and the event's native extent all come out of this one object.

The law's action is written as Jcost(dilation) + equal-weight Weyl action. The first term, Jcost, is the framework's proved cost function. The second term is the field action at the event's clock center. The law's key variable is the dilation, a positive real number that scales the event. The law proves that the action is nonnegative, and that it is minimized at the unit dilation, where the dilation equals 1.

This is a foundational model, not a forced consequence of earlier premises. The framework does not claim that previous recognition premises forced this selection. What is proved is what follows from the model. The central theorem states that a joint ground state, a state minimizing the total action over all dilations and field variations, must have unit dilation. Another theorem states that the field ground state at any dilation is the same as the field ground state at unit dilation.

The law also fixes the native extent of an event. This extent is measured in the existing RS voxel standard. The law proves that this extent is invariant under refinement, meaning it does not depend on the refinement level. An external conversion to meters remains outside the law. The law does not weaken the present-interface length non-identifiability theorem.

The law's most striking consequence is that only the unit scale preserves the complete posting law. A theorem proves that a positive scale preserves the law if and only if the scale equals 1. A separate theorem shows that a scale of 2 does not preserve the law. This is a sharp result: the framework's own scale is the only one that works.

THEOREM scaleBearingSelfDualPostingAction27_nonneg · scaleBearingSelfDualPostingAction27_unit_le · scaleBearingSelfDualPostingAction27_unit_lt · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean
scaleBearingSelfDualPostingAction27_nonneg · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean:72 
theorem scaleBearingSelfDualPostingAction27_nonneg
    (event : RealizedPostingEvent3 3)
    (dilation : PostingDilationCoord)
    (ψ : WeylEventAmplitude27) :
    0 ≤ scaleBearingSelfDualPostingAction27 event dilation ψ :=
  add_nonneg (Cost.Jcost_nonneg dilation.2)
    (selfDualPostingWeylCost27_nonneg event ψ)
scaleBearingSelfDualPostingAction27_unit_le · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean:126 
/-- The native dilation is a global minimum for every field state. -/
theorem scaleBearingSelfDualPostingAction27_unit_le
    (event : RealizedPostingEvent3 3)
    (dilation : PostingDilationCoord)
    (ψ : WeylEventAmplitude27) :
    scaleBearingSelfDualPostingAction27
        event unitPostingDilation ψ ≤
      scaleBearingSelfDualPostingAction27 event dilation ψ := by
  unfold scaleBearingSelfDualPostingAction27
  simp only [unitPostingDilation, Cost.Jcost_unit0, zero_add]
  exact le_add_of_nonneg_left (Cost.Jcost_nonneg dilation.2)
scaleBearingSelfDualPostingAction27_unit_lt · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean:138 
/-- Every non-native positive dilation is strictly more costly, pointwise in
the field state. -/
theorem scaleBearingSelfDualPostingAction27_unit_lt
    (event : RealizedPostingEvent3 3)
    (dilation : PostingDilationCoord)
    (hdilation : dilation.1 ≠ 1)
    (ψ : WeylEventAmplitude27) :
    scaleBearingSelfDualPostingAction27
        event unitPostingDilation ψ <
      scaleBearingSelfDualPostingAction27 event dilation ψ := by
  unfold scaleBearingSelfDualPostingAction27
  simp only [unitPostingDilation, Cost.Jcost_unit0, zero_add]
  exact lt_add_of_pos_left _
    (Cost.Jcost_pos_of_ne_one dilation.1 dilation.2 hdilation)
THEOREM jointPostingGroundState27_dilation_eq_unit · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean
jointPostingGroundState27_dilation_eq_unit · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean:204 
/-- Any joint ground pair has the unique native dilation. -/
theorem jointPostingGroundState27_dilation_eq_unit
    (admissible : WeylEventAmplitude27 → Prop)
    (event : RealizedPostingEvent3 3)
    (dilation : PostingDilationCoord)
    (ψ : WeylEventAmplitude27)
    (hground :
      IsJointPostingGroundState27
        admissible event dilation ψ) :
    dilation = unitPostingDilation := by
  have hle := hground.2 unitPostingDilation ψ hground.1
  have hnonneg := Cost.Jcost_nonneg dilation.2
  have hzero : Cost.Jcost dilation.1 = 0 := by
    unfold scaleBearingSelfDualPostingAction27 at hle
    simp only [unitPostingDilation, Cost.Jcost_unit0, zero_add] at hle
    exact le_antisymm (by linarith) hnonneg
  have hdilation :
      dilation.1 = 1 :=
    (Cost.Jcost_eq_zero_iff dilation.1 dilation.2).mp hzero
  exact Subtype.ext hdilation
THEOREM positiveScalePreservesCompletePostingLaw27_iff · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean
positiveScalePreservesCompletePostingLaw27_iff · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean:409 
/-- Anti-rescaling certificate: preserving the complete new law forces the
identity rechart. -/
theorem positiveScalePreservesCompletePostingLaw27_iff
    (event : RealizedPostingEvent3 3)
    (ψ : WeylEventAmplitude27)
    (scale : ℝ) :
    PositiveScalePreservesCompletePostingLaw27
        event ψ scale ↔
      scale = 1 := by
  constructor
  · rintro ⟨_, hpreserves⟩
    have hlength := congrArg
      (fun observation : WeylEventSite27 × ℝ × ℝ =>
        observation.2.2) hpreserves
    simpa [rechartCompletePostingObservation27,
      completeScaleBearingPostingObservation27,
      nativePostingExtentResponse27,
      nativePostingExtentQuantum27,
      unitPostingDilation,
      Constants.RSNativeUnits.voxel] using hlength
  · intro hscale
    subst scale
    simp [PositiveScalePreservesCompletePostingLaw27,
      rechartCompletePostingObservation27]
THEOREM scale_two_does_not_preserve_completePostingLaw27 · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean
scale_two_does_not_preserve_completePostingLaw27 · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean:434 
theorem scale_two_does_not_preserve_completePostingLaw27
    (event : RealizedPostingEvent3 3)
    (ψ : WeylEventAmplitude27) :
    ¬ PositiveScalePreservesCompletePostingLaw27
      event ψ 2 := by
  rw [positiveScalePreservesCompletePostingLaw27_iff]
  norm_num
THEOREM nativePostingExtentAtRefinement27_invariant · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean
nativePostingExtentAtRefinement27_invariant · IndisputableMonolith/Foundation/PairKernelScaleBearingSelfDualPostingLaw.lean:353 
/-- The event extent is independent of the number of phases used to represent
the carrier. -/
theorem nativePostingExtentAtRefinement27_invariant
    (event : RealizedPostingEvent3 3)
    (N M : ℕ) :
    nativePostingExtentAtRefinement27 event N =
      nativePostingExtentAtRefinement27 event M := by
  rfl

What this page does not claim

The posting law itself is not derived from earlier Recognition premises; it is a foundational model. The law does not provide a conversion from native voxels to meters. The law does not claim that the previous recognition premises forced the selection of this definition.

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