Foundation Pair Kernel Constructed Covector Event Occurrence Join

The event-spatial tie

In Recognition Science, a ledger is a discrete record of events, each event a change in some quantity. The framework's library, a machine-checked collection of formal theorems, models these events as steps on a three-dimensional torus, a finite grid that wraps around. Each step has a direction, one of three axes, and an orientation, forward or backward. The module named in the question establishes a specific link: for any event that a ledger records, the direction of the spatial step and the accounting side of the posting, debit or credit, are locked together. A forward step is always a debit, a backward step is always a credit.

This link is not an assumption. The library proves it as a theorem, EventSpatialOccurrenceTie, which states that a posting address, a pair of an axis and a side, matches the event's framed spatial step. The proof runs through a structure called a committed event witness, a package of ledger states and properties that certifies an event is real. From that witness, the library extracts the occurrence, the specific axis and side, and shows the extracted poles, the source and sink of the posting, equal the oriented poles of that owner. The construction is witness-independent for the scale: the numeric value attached to the event does not depend on which witness you choose, only on the event itself.

The module also builds a covector, a linear map that reads a physical carrier and returns a number, from the event's occurrence. This covector is unique: two different readouts of the same channel give the same result. It also matches the boundary sign convention, so the covector's value on a probe equals the occurrence's boundary record times the scale. All of this is packaged into a certificate, a proposition that the join of constructed covector and event occurrence holds, and the library proves that certificate for every realized event.

One gap remains open. The library does not prove that every posting pair produced by the earlier stage, S8, carries a nonnegative ledger state. That missing proposition, MissingNonnegLedgerOnS8PostingWitness, is stated but not inhabited. The module instead proves a conditional: if such a nonnegative state exists and satisfies the tie, then a committed witness exists. The gap is a target for future work, not an axiom.

What this means in plain terms: the framework has shown, with machine-checked proofs, that the bookkeeping side of an event and its spatial direction are the same fact viewed twice. A debit is not just a number going down; it is a step forward along an axis. This ties the abstract ledger to the geometry of space, a step toward deriving physical structure from the cost of recognition.

/-- Relates a recovered owner occurrence `(k, side)` to the realized event's
ordered spatial pair: the torus sites of `event.1` form a framed axis step
on account `k`, with forward ↦ debit and backward ↦ credit. -/
def EventSpatialOccurrenceTie
    {N : ℕ} [NeZero N]
    (event : RealizedPostingEvent3 N)
    (k : Fin 3) (side : Side) : Prop :=
  let p : TorusSite3 N := (torusSiteEquivFin N).symm event.1.1
  let q : TorusSite3 N := (torusSiteEquivFin N).symm event.1.2
  (q = framedForward (Equiv.refl (Fin 3)) p k ∧ side = Side.debit) ∨
    (q = framedBackward (Equiv.refl (Fin 3)) p k ∧ side = Side.credit)

/-- Any two committed witnesses of the same event share the same instrument
scale factor (stage-1 scale).  Poles may differ. -/
theorem constructedEventSource_scale_witness_independent
    {N : ℕ} [NeZero N]
    {channelEnergy : PostingEventChannelEnergy3 N}
    (readout : FaithfulChannelReadout channelEnergy)
    (event : RealizedPostingEvent3 N) (n : ℕ)
    (_w₁ _w₂ : CommittedEventWitness event) :
    constructedSourceScale readout event n =
      constructedSourceScale readout event n :=
  rfl

/-- Across faithful readouts, stage-1 rigidity still kills scale freedom of
the event-joined covector. -/
theorem constructedEventSourceCovector_readout_unique
    {N : ℕ} [NeZero N]
    {channelEnergy : PostingEventChannelEnergy3 N}
    (readout₁ readout₂ : FaithfulChannelReadout channelEnergy)
    (event : RealizedPostingEvent3 N) (n : ℕ)
    (w : CommittedEventWitness event) :
    constructedEventSourceCovector readout₁ event n w =
      constructedEventSourceCovector readout₂ event n w := by
  simp only [constructedEventSourceCovector]
  exact constructedOccurrenceSourceCovector_unique
    readout₁ readout₂ event n
    (occurrenceOfCommittedWitness w).1
    (occurrenceOfCommittedWitness w).2

theorem constructedCovectorEventOccurrenceJoin_cert :
    ConstructedCovectorEventOccurrenceJoinCert where
  model_witness_nonempty := fun {_ _} => modelCommittedEventWitness_nonempty
  event_tie_field := fun {_ _} _event w => committedEventWitness_event_tie w
  poles_commute := fun {_ _} _event w => polesOfCommittedWitness_commutes w
  profile_commutes := fun {_ _} _event w =>
    orientedPolesOfCommittedWitness_eq_owner w
  scale_witness_independent := fun {_ _} {_} _readout _event _n _w₁ _w₂ => rfl
  evaluation_corollary := fun {_ _} {_} {_} =>
    constructedEventSource_matches_boundarySign
  s8_existential_half := fun {_ _} event =>
    realizedPrimitivePostingPair_has_ledger_event event.1 event.2
  documentation_s8_nonneg_gap_remains_open := trivial
  documentation_does_not_strengthen_s8_existential := trivial

What this page does not claim

The module does not prove that every S8 posting pair has a nonnegative ledger state; that remains an open gap. The event-spatial tie does not derive the fine-structure constant or any other coupling constant. The covector construction does not depend on a specific choice of readout, but the readout itself is not derived here.

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