Encyclopedia Foundation Foundation Pair Kernel Scale Breaking Source Residual Physical Attachment Attach

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Scale Breaking Source Residual Physical Attachment Attach

A machine-checked theorem pins down a specific number for a posting's source magnitude, but only if two extra physical assumptions are granted.

Verify this page

The attachment theorem

The theorem physicalAttachment_attaches_candidateB_at_actionNormalizedScale is a formal statement in the Recognition Science framework's machine-checked library of formal theorems. It says: if a realized primitive posting pair carries a physical posting magnitude attachment, and if that posting's action obeys the posting magnitude action law, then the source magnitude must equal a specific value, called Candidate B, and the pair-kernel source equation uses a Green scale fixed by that value. In plainer terms, once you commit to two extra physical assumptions, the framework's equations force a particular number for the source magnitude and no other.

The two assumptions are separate and independent. The first is that one realized primitive posting carries the native action quantum. The second is that its source coordinate is the multiplicative action dual, measured in the Euler-J action unit. Neither assumption alone selects the value. The framework proves, with explicit countermodels, that source-action duality alone admits both banked magnitudes, and that fixing the native posting action alone still leaves the source map free. Only together do the two statements single out Candidate B, which is the reciprocal native-action magnitude.

What the theorem does not claim is just as important. It does not derive those two physical statements from the framework's current premises. The framework proves the opposite: the current premises do not force the native-action dual law, and Candidate A, the other banked magnitude, satisfies every current premise while failing the new law. The theorem is a sufficiency result, not a derivation. It shows that if you add the two missing physical bits, then Candidate B follows; it does not show that the framework already implies those bits.

The theorem also carries a normalization condition. The selected posting magnitude enters the pair-kernel source equation only through realGreenScaleFromPostingMagnitude, so the action-variation factor is applied exactly once. This means the attachment is correctly normalized: the Green scale used in the source equation is the independently fixed value q / 2, not something that shifts when the action varies. The framework banks this as a scale-breaking law, one that discriminates between the two candidates and gives a unique model when combined with the current premises.

In the wider picture, this theorem is a step toward a target-blind attachment door, a way to select physical magnitudes without peeking at the target. It does not itself prove that the physical attachment holds in reality; it proves a conditional: if the two physical statements hold on a realized event, then the source magnitude is Candidate B and the source equation is correctly scaled. The remaining physical question, whether those two statements are true of the actual ledger, is left open.

THEOREM physicalAttachment_attaches_candidateB_at_actionNormalizedScale · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean
physicalAttachment_attaches_candidateB_at_actionNormalizedScale · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean:178 
/-- If the two missing physical statements are supplied on a realized event,
the source magnitude is Candidate B and its pair-kernel source equation uses
the independently fixed Green scale `q / 2`. -/
theorem physicalAttachment_attaches_candidateB_at_actionNormalizedScale
    {N : ℕ} [NeZero N]
    {postingAction sourceMagnitude : PostingPair3 N → ℝ}
    (hphysical :
      PhysicalPostingMagnitudeAttachment3
        postingAction sourceMagnitude)
    {event : PostingPair3 N}
    (hevent : event ∈ realizedPrimitivePostingPairs3 N)
    {n : ℕ}
    (w : Fin n → Fin n → ℝ)
    (e : Fin n → ℝ)
    (a b : Fin n)
    (hsymm : ∀ i j, w i j = w j i)
    (haction :
      PostingMagnitudeActionLaw
        (sourceMagnitude event) w e a b) :
    sourceMagnitude event =
        candidateB_sourceMagnitudeExpr.eval ∧
      ScaledSourceEquation w (dipole a b)
        (realGreenScaleFromPostingMagnitude
          candidateB_sourceMagnitudeExpr.eval) e := by
  have hsource :
      sourceMagnitude event =
        candidateB_sourceMagnitudeExpr.eval := by
    change sourceMagnitude event = nativeActionQuantumInv
    exact
      physicalPostingAttachment_forces_nativeActionQuantumInv
        hphysical hevent
  refine ⟨hsource, ?_⟩
  rw [← hsource]
  exact
    (postingMagnitudeActionLaw_iff_scaledSourceEquation
      (sourceMagnitude event) w e a b hsymm).1 haction
THEOREM sourceActionDuality_alone_admits_distinct_banked_magnitudes · nativePostingAction_alone_admits_distinct_source_maps · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean
sourceActionDuality_alone_admits_distinct_banked_magnitudes · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean:121 
/-- Source-action duality alone admits both banked source magnitudes. Candidate
A pairs unit source with unit action; Candidate B pairs reciprocal native
source with native action. The physical action normalization is therefore a
separate scale-breaking statement. -/
theorem sourceActionDuality_alone_admits_distinct_banked_magnitudes :
    PostingSourceIsActionDual3
        (@unitPostingActionCountermodel3 3 inferInstance)
        (@unitSourceMagnitudeCountermodel3 3 inferInstance) ∧
      PostingSourceIsActionDual3
        (@nativePostingActionCandidate3 3 inferInstance)
        (@nativeDualSourceMagnitudeCandidate3 3 inferInstance) ∧
      ∃ event : PostingPair3 3,
        event ∈ realizedPrimitivePostingPairs3 3 ∧
          unitSourceMagnitudeCountermodel3 event =
            candidateA_sourceMagnitudeExpr.eval ∧
          nativeDualSourceMagnitudeCandidate3 event =
            candidateB_sourceMagnitudeExpr.eval ∧
          unitSourceMagnitudeCountermodel3 event ≠
            nativeDualSourceMagnitudeCandidate3 event := by
  refine
    ⟨unitAssignments_satisfy_sourceActionDuality,
      nativeCandidates_source_is_actionDual, ?_⟩
  obtain ⟨event, hevent, _hcert⟩ :=
    canonicalGeneratorSource_consumer_exists
      (N := 3) (by norm_num) (Equiv.refl (Fin 3))
  have hA :
      unitSourceMagnitudeCountermodel3 event =
        candidateA_sourceMagnitudeExpr.eval := by
    change (1 : ℝ) = candidateA_sourceMagnitudeExpr.eval
    exact candidateA_sourceMagnitude_eq_one.symm
  have hB :
      nativeDualSourceMagnitudeCandidate3 event =
        candidateB_sourceMagnitudeExpr.eval := by
    rfl
  refine ⟨event, hevent, hA, hB, ?_⟩
  intro heq
  exact candidates_select_distinct_magnitudes
    (hA.symm.trans (heq.trans hB))
nativePostingAction_alone_admits_distinct_source_maps · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean:160 
/-- Even after the native posting-action assignment is fixed, a source map is
still free until the action-dual identification is supplied. -/
theorem nativePostingAction_alone_admits_distinct_source_maps :
    MinimumJPostingCarriesNativeAction3
        (@nativePostingActionCandidate3 3 inferInstance) ∧
      ∃ event : PostingPair3 3,
        event ∈ realizedPrimitivePostingPairs3 3 ∧
          unitSourceMagnitudeCountermodel3 event ≠
            nativeDualSourceMagnitudeCandidate3 event := by
  refine ⟨nativePostingActionCandidate_carries_nativeAction, ?_⟩
  obtain
    ⟨_hunitDual, _hnativeDual, event, hevent,
      _hA, _hB, hne⟩ :=
    sourceActionDuality_alone_admits_distinct_banked_magnitudes
  exact ⟨event, hevent, hne⟩
THEOREM currentPremises_do_not_force_nativeActionDualSourceLaw · nativeActionDualSourceLaw_rejects_candidateA · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean
currentPremises_do_not_force_nativeActionDualSourceLaw · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean:108 
/-- The new law is not hidden in the old package: Candidate A satisfies every
current premise and fails the native-action dual law. -/
theorem currentPremises_do_not_force_nativeActionDualSourceLaw :
    ¬ (∀ sourceMagnitude : ℝ,
      CurrentRecognitionSourcePremises sourceMagnitude →
        NativeActionDualSourceLaw sourceMagnitude) := by
  intro hforce
  exact nativeActionDualSourceLaw_rejects_candidateA
    (hforce _
      candidateA_satisfies_currentRecognitionSourcePremises)
nativeActionDualSourceLaw_rejects_candidateA · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean:77 
/-- Independent discrimination: the native-action dual law rejects the
one-act source candidate because the two banked magnitudes are distinct. -/
theorem nativeActionDualSourceLaw_rejects_candidateA :
    ¬ NativeActionDualSourceLaw
      candidateA_sourceMagnitudeExpr.eval := by
  intro hA
  exact candidates_select_distinct_magnitudes
    ((nativeActionDualSourceLaw_iff_candidateB _).1 hA)
THEOREM physicalAttachment_attaches_candidateB_at_actionNormalizedScale · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean
physicalAttachment_attaches_candidateB_at_actionNormalizedScale · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean:178 
/-- If the two missing physical statements are supplied on a realized event,
the source magnitude is Candidate B and its pair-kernel source equation uses
the independently fixed Green scale `q / 2`. -/
theorem physicalAttachment_attaches_candidateB_at_actionNormalizedScale
    {N : ℕ} [NeZero N]
    {postingAction sourceMagnitude : PostingPair3 N → ℝ}
    (hphysical :
      PhysicalPostingMagnitudeAttachment3
        postingAction sourceMagnitude)
    {event : PostingPair3 N}
    (hevent : event ∈ realizedPrimitivePostingPairs3 N)
    {n : ℕ}
    (w : Fin n → Fin n → ℝ)
    (e : Fin n → ℝ)
    (a b : Fin n)
    (hsymm : ∀ i j, w i j = w j i)
    (haction :
      PostingMagnitudeActionLaw
        (sourceMagnitude event) w e a b) :
    sourceMagnitude event =
        candidateB_sourceMagnitudeExpr.eval ∧
      ScaledSourceEquation w (dipole a b)
        (realGreenScaleFromPostingMagnitude
          candidateB_sourceMagnitudeExpr.eval) e := by
  have hsource :
      sourceMagnitude event =
        candidateB_sourceMagnitudeExpr.eval := by
    change sourceMagnitude event = nativeActionQuantumInv
    exact
      physicalPostingAttachment_forces_nativeActionQuantumInv
        hphysical hevent
  refine ⟨hsource, ?_⟩
  rw [← hsource]
  exact
    (postingMagnitudeActionLaw_iff_scaledSourceEquation
      (sourceMagnitude event) w e a b hsymm).1 haction

What this page does not claim

The theorem does not derive the two physical assumptions from the current premises. The theorem does not prove that the physical attachment actually holds in reality. The theorem does not claim that Candidate A is impossible under all circumstances, only under the added law.

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