Encyclopedia Foundation Foundation Pair Kernel Gap2a Production Orbit Residual Complete Production Respo

ARTICLE 4 claims 4 theorems

Foundation Pair Kernel Gap2a Production Orbit Residual Complete Production Respo

A machine-checked theorem shows that a complete production schedule can repeat every five or every eight steps, and that these two schedules cannot be rescaled into each other.

Verify this page

The five and eight source orbits

A production schedule is a finite repeating list of acts that, together, cover every possible committed response in a recognition ledger, a discrete record of events. The framework's library, a machine-checked collection of formal theorems, proves that two such complete schedules exist. One repeats every five steps and never shows the same response twice. The other repeats every eight steps and necessarily shows some response more than once.

The theorem completeProductionResponseOrbits_admit_distinct_five_and_eight_sources states both schedules exist and that their aggregate source scales differ. The aggregate source scale is the total posting magnitude multiplied by the period and divided by two. For a positive posting magnitude, the five-step and eight-step schedules therefore cannot be made equal by any rescaling of that magnitude.

The five-step schedule is the only simple one: any complete schedule that shows each response exactly once must have period five. The eight-step schedule is not simple, because with eight steps and only five response classes, repetition is forced. This is a proved theorem, not a model choice.

In Recognition Science, this result does not select five or eight as the physical source window. The framework models the orbits as witnesses, not as a derivation of a continuum. 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. That coupling remains open.

THEOREM completeProductionResponseOrbits_admit_distinct_five_and_eight_sources · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean
completeProductionResponseOrbits_admit_distinct_five_and_eight_sources · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean:232 
/-- Actual response-complete closed production orbits admit distinct
five-phase and eight-phase linear source aggregates at every positive posting
magnitude.  Thus response completeness does not select a unique window under
the already-banked linear per-posting Green aggregation law. -/
theorem completeProductionResponseOrbits_admit_distinct_five_and_eight_sources
    (postingMagnitude : ℝ)
    (hposting : 0 < postingMagnitude) :
    canonicalFiveProductionResponseOrbit3.period = 5 ∧
      canonicalEightProductionResponseOrbit3.period = 8 ∧
      productionResponseOrbitAggregateGreenSourceScale
          canonicalFiveProductionResponseOrbit3 postingMagnitude ≠
        productionResponseOrbitAggregateGreenSourceScale
          canonicalEightProductionResponseOrbit3 postingMagnitude := by
  refine ⟨rfl, rfl, ?_⟩
  rw [productionResponseOrbitAggregateGreenSourceScale_eq,
    productionResponseOrbitAggregateGreenSourceScale_eq]
  change
    (5 : ℝ) * postingMagnitude / 2 ≠
      (8 : ℝ) * postingMagnitude / 2
  nlinarith
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 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 productionResponseOrbitAggregateGreenSourceScale_eq · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean
productionResponseOrbitAggregateGreenSourceScale_eq · IndisputableMonolith/Foundation/PairKernelGap2aProductionOrbitResidual.lean:222 
theorem productionResponseOrbitAggregateGreenSourceScale_eq
    (orbit : ClosedProductionResponseOrbit3)
    (postingMagnitude : ℝ) :
    productionResponseOrbitAggregateGreenSourceScale
        orbit postingMagnitude =
      (orbit.period : ℝ) * postingMagnitude / 2 := by
  unfold productionResponseOrbitAggregateGreenSourceScale
    realGreenScaleFromPostingMagnitude
  ring

What this page does not claim

The theorem does not select five versus eight as the physical source window. The theorem does not derive absolute posting action or a representative-independent action dual. The theorem does not prove that a period-eight orbit is impossible; it proves such an orbit exists but repeats a response.

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