Encyclopedia Foundation Foundation Pair Kernel Scale Breaking Source Residual Current Premises Do Not Fo

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Scale Breaking Source Residual Current Premises Do Not Fo

The framework's own theorems prove that its current starting assumptions do not yet determine which of two possible source magnitudes nature uses.

Verify this page

What the current premises leave open

The Recognition Science framework keeps a discrete record of recognition events, a ledger. Each primitive posting in that ledger carries a magnitude, a number that enters the framework's core equations. The framework's current premises, the assumptions it has committed to so far, admit two distinct banked posting magnitudes, called Candidate A and Candidate B. The declaration currentPremises_do_not_force_nativeActionDualSourceLaw is a proved theorem stating that those premises do not force the choice.

Concretely, the theorem proves there is no way, from the current premises alone, to derive the statement that one physical posting carries the native action quantum and that its source coordinate is the multiplicative action dual. That statement, called NativeActionDualSourceLaw, would select Candidate B. The theorem shows that Candidate A satisfies every current premise yet fails this law, so the premises cannot imply it. This is a theorem about the framework's own logical reach: it is a proved limitation, not a gap in the proof checker.

The declaration also establishes that the two missing physical bits are independent. Source-action duality alone admits both banked magnitudes, and fixing the native posting-action assignment alone still leaves the source map free. Each statement must be supplied separately. The module banks the discrimination power of the combined law: with both statements added, the framework has exactly one model, and the source magnitude is Candidate B, whose value enters the pair-kernel source equation through the independently fixed Green scale.

What the declaration does not claim is equally precise. It does not assert that NativeActionDualSourceLaw is false, nor that it is derivable from the current premises. It does not say the framework is broken or incomplete in a way that invalidates its other results. It simply marks the boundary of what the committed premises can prove, and names the exact additional physical statements needed to proceed. The law itself is a hypothesis, not a theorem, and the declaration is the honest statement that the framework has not yet earned it.

THEOREM currentPremises_do_not_force_nativeActionDualSourceLaw · 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)
THEOREM nativeActionDualSourceLaw_rejects_candidateA · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean
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 sourceActionDuality_alone_admits_distinct_banked_magnitudes · 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))
THEOREM nativeActionDualSourceLaw_is_scaleBreaking · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean
nativeActionDualSourceLaw_is_scaleBreaking · IndisputableMonolith/Foundation/PairKernelScaleBreakingSourceResidual.lean:94 
/-- The named law is strong enough to satisfy the formal scale-breaking
criterion: current premises plus this extra law have exactly one model. -/
theorem nativeActionDualSourceLaw_is_scaleBreaking :
    IsScaleBreakingAttachmentLaw NativeActionDualSourceLaw := by
  refine
    ⟨candidateB_sourceMagnitudeExpr.eval,
      ⟨candidateB_satisfies_currentRecognitionSourcePremises,
        candidateB_satisfies_nativeActionDualSourceLaw⟩,
      ?_⟩
  intro sourceMagnitude hsource
  exact
    (nativeActionDualSourceLaw_iff_candidateB sourceMagnitude).1
      hsource.2

What this page does not claim

The native-action dual law is true. The current premises are inconsistent. The framework's other theorems are invalidated by this limitation. The two missing physical statements are derivable from the current premises.

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