Foundation Pair Kernel Recognition Transport Residuals S18 Event Survival And Ag

Survival and channel price

The declaration eventSurvivalAndAggregate_imply_channelApplicability is a formal theorem in the framework's machine-checked library of formal theorems. In plain language it says: if a recognized event has a survival value that obeys a self-similarity rule, and if the event's price factors through a specific aggregate, then the event's channel is applicable. The theorem is a bridge between two descriptions of the same event, one in time and one in cost.

The self-similarity rule is the key constraint. It says the survival value s of an event satisfies s = 1 / (1 + s). This equation has one positive solution, the golden ratio conjugate: s = 1/φ ≈ 0.618. The theorem proves that any survival function meeting this rule must assign this exact value to every event. It is not a choice or an approximation; it is forced by the rule itself.

The aggregate side says the event's price equals a particular function of the survival value and the channel carrier. The theorem connects these two: the self-similar survival value and the aggregate price together imply the channel is applicable. Applicability here means the channel can carry the event without contradiction, a coherence condition on the physical carrier structure.

In Recognition Science, this is a step toward deriving physical readouts from recognition structure. But the theorem does not claim which physical channels exist. The library explicitly states that the source arrows attaching these objects to physical duration, channel price, and event energy remain open. The canonical objects are witnesses, not conclusions. The theorem shows a consistency, not a uniqueness of the physical world.

What the theorem does not claim is equally precise. It does not select the unit of time: both the native and doubled tick-span measures are additive and satisfy the factorization, so the theorem cannot tell them apart. It does not fix the scale of energy: batch additivity and price-ratio invariance preserve any positive scalar, so energy is determined only up to a scale. And it does not imply that any particular channel carrier, such as the extra or incomplete ones, is applicable. Those carriers have explicit countermodels showing they fail injectivity or surjectivity.

theorem eventSurvival_forced_eq_inv_phi
    {N : ℕ} [NeZero N]
    {survival : PostingEventSurvival3 N}
    (hself :
      PostingEventSurvivalSelfSimilar3 survival)
    (event : RealizedPostingEvent3 N) :
    survival event = 1 / Constants.phi :=
  (recognitionChannelsFromEventSurvival3
    survival hself event).s_forced

theorem canonicalPostingEventPrice_reads_JAggregate :
    PostingEventPriceReadsJAggregate3
      (parentPhysicalChannelCarrier3 3)
      (@canonicalPostingEventSurvival3 3 _)
      (@canonicalPostingEventChannelPrice3 3 _) := by
  intro event
  rfl

theorem canonicalPostingEventSurvival_selfSimilar
    {N : ℕ} [NeZero N] :
    PostingEventSurvivalSelfSimilar3
      (@canonicalPostingEventSurvival3 N _) := by
  intro event
  exact
    ⟨canonicalChannel.s_pos,
      canonicalChannel.self_similar⟩

theorem doubledTickSpanMeasure_ne_native :
    doubledTickSpanMeasure ≠
      nativeTickSpanMeasure := by
  intro heq
  have hunit :=
    congrArg (fun span =>
      span.measure 1) heq
  simp [doubledTickSpanMeasure,
    nativeTickSpanMeasure] at hunit

theorem stretchedDuration_factors_doubledTickSpan :
    PostingDurationFactorsThroughTickSpan3
      doubledTickSpanMeasure
      (stretchedDurationKinematics3 3) := by
  intro event
  rw [postingEventTickSpan3_eq_one]
  simp [doubledTickSpanMeasure,
    stretchedDurationKinematics3]

theorem doubledEnergy_has_uniformScale_two :
    PostingEnergyHasUniformPriceScale3
      2
      (@canonicalPostingEventChannelPrice3 3 _)
      (doubledEnergyKinematics3 3) := by
  intro event
  change
    2 * Constants.E_coh =
      2 * canonicalPostingEventChannelPrice3 event
  rw [completeCarrier_channelPrice_eq_E_coh
    parentPhysicalChannelCarrier_is_complete
    canonicalPostingRecognitionChannel_applies
    event]

/-- Conversely, exact readout forces any uniform scale representation to have
scale one as soon as one positive-price event exists. -/
theorem energyReadout_forces_uniformScale_one
    {N : ℕ} [NeZero N]
    {scale : ℝ}
    {price : PostingEventChannelPrice3 N}
    {kinematics : PostingEventKinematics3 N}
    [Nonempty (RealizedPostingEvent3 N)]
    (hprice : ∀ event, 0 < price event)
    (hscale :
      PostingEnergyHasUniformPriceScale3
        scale price kinematics)
    (hread :
      PostingEnergyReadsEventChannelPrice3
        price kinematics) :
    scale = 1 := by
  let event : RealizedPostingEvent3 N :=
    Classical.choice inferInstance
  have hscaled := hscale event
  have hexact := hread event
  nlinarith [hprice event]

What this page does not claim

The theorem does not prove that any particular physical channel exists. The theorem does not determine the unit of time. The theorem does not fix the absolute scale of energy. The theorem does not establish the physical recognition-to-linking bridge.

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