Encyclopedia Foundation Foundation Pair Kernel Gap2a Production Orbit Residual Simple Closed Production

ARTICLE 5 claims 5 theorems

Foundation Pair Kernel Gap2a Production Orbit Residual Simple Closed Production

A machine-checked theorem shows that any non-repeating production cycle in this framework must have exactly five steps, not eight.

Verify this page

The five-step cycle

A production cycle is a repeating schedule of acts. In the Recognition Science framework, a ledger, a discrete record of events, tracks each act and the response it produces. The theorem simpleClosedProductionResponseOrbit_period_eq_five states a constraint on such cycles: if a cycle is closed, meaning it covers every possible response, and simple, meaning no response appears twice, then its period is exactly five.

The proof rests on a counting argument. The framework's catalog of committed responses has exactly five classes. A simple cycle must assign each phase of its period to a distinct response class, and to be complete it must cover all of them. Since there are five classes, a simple complete cycle needs five phases. The machine-checked library of formal theorems records this as a proved result, not a definitional choice.

The same library also constructs an eight-phase cycle. That cycle is closed, but it is not simple: it necessarily repeats a response. This distinction matters because completeness alone does not decide between five and eight as the fundamental window. The five-step cycle is the only one that avoids repetition while covering every response.

In Recognition Science, this result sharpens the picture of how production acts unfold. It does not, however, close the larger question of how these cycles connect to physical quantities. The library proves that no fixed selector can recover an absolute posting action from such an orbit, and that no source selector acts as a dual for all representatives. A future object would need to carry phase data beyond the five response classes and couple that data to physical action.

THEOREM simpleClosedProductionResponseOrbit_period_eq_five · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean
simpleClosedProductionResponseOrbit_period_eq_five · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean:145 
/-- 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 recognitionResponseEquivFinFive3 · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean
recognitionResponseEquivFinFive3 · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean:101 
/-- Canonical finite indexing of the five committed response classes. -/
noncomputable def recognitionResponseEquivFinFive3 :
    RecognitionParentResponse3 ≃ Fin 5 :=
  Fintype.equivFinOfCardEq
    recognitionParentResponse_card_eq_five
THEOREM canonicalEightProductionResponseOrbit3 · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean
canonicalEightProductionResponseOrbit3 · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean:173 
/-- A complete eight-phase orbit of actual production acts.  Its last three
phases repeat committed response classes, so existence does not make eight an
intrinsically selected response period. -/
noncomputable def canonicalEightProductionResponseOrbit3 :
    ClosedProductionResponseOrbit3 where
  period := 8
  period_pos := by norm_num
  phaseAct := fun phase =>
    productionActForResponse3
      (recognitionResponseEquivFinFive3.symm
        (eightToFiveProductionPhase3 phase))
  responseComplete := by
    intro response
    let phase5 : Fin 5 :=
      recognitionResponseEquivFinFive3 response
    let phase8 : Fin 8 :=
      ⟨phase5.val, lt_trans phase5.isLt (by norm_num)⟩
    refine ⟨phase8, ?_⟩
    change
      productionEventResponseAct_read
          (productionActForResponse3
            (recognitionResponseEquivFinFive3.symm
              (eightToFiveProductionPhase3 phase8))) =
        response
    rw [productionActForResponse3_read]
    apply recognitionResponseEquivFinFive3.injective
    simp [eightToFiveProductionPhase3, phase8, phase5,
      Nat.mod_eq_of_lt phase5.isLt]
THEOREM canonicalEightProductionResponseOrbit_not_simple · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean
canonicalEightProductionResponseOrbit_not_simple · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean:202 
theorem canonicalEightProductionResponseOrbit_not_simple :
    ¬ ProductionResponseOrbitIsSimple3
      canonicalEightProductionResponseOrbit3 := by
  intro hsimple
  have hperiod :=
    simpleClosedProductionResponseOrbit_period_eq_five
      canonicalEightProductionResponseOrbit3 hsimple
  norm_num [canonicalEightProductionResponseOrbit3] at hperiod
THEOREM no_fixed_productionOrbit_selector_recovers_absolutePostingAction · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean
no_fixed_productionOrbit_selector_recovers_absolutePostingAction · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean:271 
/-- 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)

What this page does not claim

The theorem does not claim that the five-step cycle is the only possible closed cycle; an eight-step closed cycle exists but repeats a response. The theorem does not claim that production cycles determine physical action; the library proves that no fixed selector recovers absolute posting action from an orbit. The theorem does not claim that the five-step cycle is physically realized; the orbit schedules are model witnesses, not proven physical events.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND