Foundation Pair Kernel Gap2a Production Orbit Residual No Fixed Production Orbit

The action dual gap

In the Recognition Science framework, a production orbit is a finite, repeating schedule of production acts, each tied to a witnessed posting event. The framework models these as a closed cycle: the schedule repeats forever, and the set of acts it covers must include every committed recognition response. Think of a factory floor where each shift must produce at least one of every part in the catalog, and the shifts repeat in a fixed order. The theorem in question concerns an action dual, which in this setting means a positive real number assigned to each event such that multiplying it by the event's posting action yields a fixed unit of action, the eulerJActionUnit.

The theorem, no_fixed_productionOrbit_sourceSelector_is_actionDual_for_all_representatives, proves that for any such closed production orbit, there is no selector function that assigns an action dual to every representative event in the orbit. The selector is a function from physical observable classes and production orbit events to real numbers, and the theorem states that no such function can satisfy the dual condition for all representatives. This is a no-go result: it establishes a structural impossibility, not a mere absence of a convenient choice.

This result is one of several in the module that together show a specific gap in the framework's construction. A simpler five-period orbit exists, and an eight-period orbit also exists, but neither closes the physical joins. The theorem is proved in the framework's machine-checked library of formal theorems, with no unproved assumptions and no new axioms. It is a theorem about the framework's own definitions, not a claim about the physical world directly.

What the theorem does not claim is equally important. It does not claim that action duals are impossible in general, only that no fixed orbit can provide them for all representatives. It does not claim that the framework is inconsistent or that the gap cannot be closed; the module explicitly notes that a future closing object must carry phase data beyond the five response classes and couple that data to physical action. The theorem is a precise boundary marker, not a dead end.

/-- The multiplicative action-dual source also fails to descend after the
whole fixed closed production orbit is adjoined. -/
theorem no_fixed_productionOrbit_sourceSelector_is_actionDual_for_all_representatives
    (orbit : ClosedProductionResponseOrbit3) :
    ¬ ∃ selector : ProductionOrbitActionDualSourceSelector3 orbit,
      IsActionDualForAllProductionOrbitRepresentatives3
        orbit selector := by
  rintro ⟨selector, hselector⟩
  obtain ⟨left, right, hsame, event, hne⟩ :=
    absolute_eventAction_not_unit_invariant
  have hclass :
      physicalObservableClass3 left =
        physicalObservableClass3 right :=
    sameRecognitionData_sameObservableClass hsame
  have hleft := hselector left event
  have hright := hselector right event
  have hsource :
      selector (physicalObservableClass3 left) event =
        selector (physicalObservableClass3 right) event :=
    congrArg (fun observableClass =>
      selector observableClass event) hclass
  rw [← hsource] at hright
  apply hne
  nlinarith [hleft.1, hleft.2, hright.2]

What this page does not claim

No claim that action duals are impossible outside the fixed-orbit setting. No claim that the framework is inconsistent or that the gap is unfillable. No claim that the theorem applies to physical systems directly.

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