Foundation Pair Kernel Gap2a Production Orbit Residual

The closed response orbit

A production orbit is a repeating schedule of witnessed acts. In the Recognition Science framework, reality keeps a ledger, a discrete record of events, where each act posts a response that is read back. A closed orbit is one such schedule that is complete: over one full cycle it produces every possible response at least once. The module under discussion builds these orbits from actual posting events, not from a free list, and proves what they can and cannot do.

The central result is a theorem about the smallest complete orbit. The committed production-response quotient has exactly five classes, and the theorem proves that any simple closed orbit, one where no response repeats within a cycle, must have period five. A period-eight orbit also exists and is complete, but it necessarily repeats an observable response. The framework's library, a machine-checked collection of formal theorems, proves both facts: the five-orbit is simple, the eight-orbit is not. Completeness alone therefore does not select five versus eight as the source window.

The no-go results are the sharper ones. A selector is a fixed rule that assigns a real number to each production act. Two theorems prove that no fixed selector can recover absolute posting action, and no fixed source selector can act as a dual for all representatives. In plain terms, the five and eight orbits are witnesses that the schedule exists, but the schedule cannot carry the full physical content. The independent positive duration and energy rescaling remain intact, and the absolute action and its multiplicative dual do not descend from the orbit data.

What this establishes is a boundary. The closed orbit is the smallest intrinsically closed source object available, but it still does not close the three physical joins. A future closing object must carry phase data beyond the five response classes and couple that phase to physical action and pair-kernel source transport. The orbit schedules are model witnesses; the no-go results are theorems. No axiom and no sorry appear in the module.

/-- Every response-simple complete production orbit has period exactly five.
This is the intrinsic closure count supplied by S24's response catalog. -/
theorem simpleClosedProductionResponseOrbit_period_eq_five
    (orbit : ClosedProductionResponseOrbit3)
    (hsimple : ProductionResponseOrbitIsSimple3 orbit) :
    orbit.period = 5 := by
  let read :
      Fin orbit.period → RecognitionParentResponse3 :=
    fun phase =>
      productionEventResponseAct_read
        (orbit.phaseAct phase)
  have hcard :
      Fintype.card (Fin orbit.period) =
        Fintype.card RecognitionParentResponse3 :=
    Fintype.card_congr
      (Equiv.ofBijective read
        ⟨hsimple, orbit.responseComplete⟩)
  calc
    orbit.period =
        Fintype.card (Fin orbit.period) := by simp
    _ = Fintype.card RecognitionParentResponse3 := hcard
    _ = 5 := recognitionParentResponse_card_eq_five

theorem canonicalEightProductionResponseOrbit_not_simple :
    ¬ ProductionResponseOrbitIsSimple3
      canonicalEightProductionResponseOrbit3 := by
  intro hsimple
  have hperiod :=
    simpleClosedProductionResponseOrbit_period_eq_five
      canonicalEightProductionResponseOrbit3 hsimple
  norm_num [canonicalEightProductionResponseOrbit3] at hperiod

/-- Fixing any entire closed response-complete production orbit does not turn
absolute event action into a function of the unit quotient. -/
theorem no_fixed_productionOrbit_selector_recovers_absolutePostingAction
    (orbit : ClosedProductionResponseOrbit3) :
    ¬ ∃ selector : ProductionOrbitAbsoluteActionSelector3 orbit,
      SelectsAllProductionOrbitRepresentativeActions3
        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
  rw [hclass] at hleft
  exact hne (hleft.symm.trans hright)

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

The module does not prove that five is the only possible period for a complete orbit, only for a simple one. The module does not derive the fine-structure constant or any physical coupling constant. The module does not close the three physical joins; it proves a boundary result about what the orbit alone cannot do.

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: