Encyclopedia Foundation Foundation Pair Kernel Constructed Covector Event Occurrence Join Committed Even

ARTICLE 3 claims 2 theorems 1 open

Foundation Pair Kernel Constructed Covector Event Occurrence Join Committed Even

A formal theorem in the Recognition Science library shows that every posting event yields a committed ledger witness, provided a missing nonnegativity condition holds.

Verify this page

The committed witness theorem

In the Recognition Science framework, a ledger is a discrete record of events, and a committed witness is a verified record that ties a posting event to a specific spatial step. The declaration committedEventWitness_of_s8_existential_with_nonneg is a theorem in the framework's machine-checked library of formal theorems. It states that if a posting event satisfies the framework's core conditions, and if the missing nonnegativity condition holds, then a committed witness exists for that event.

The theorem works by taking an existential statement from an earlier stage, which asserts that for any posting event there exist ledger states A and B with a posting step and a minimal posting step. The new theorem strengthens this: it adds the condition that the pre-state A has nonnegative entries, and it adds the event-spatial occurrence tie, which matches the posting profile's address to the event's framed spatial step. The conclusion is that a committed witness exists, meaning the event can be recorded with a verified spatial occurrence.

What the theorem does not claim is that the nonnegativity condition itself holds. The declaration MissingNonnegLedgerOnS8PostingWitness is the actual missing proposition, and it is not inhabited as evidence. The theorem only eliminates the S8 existential under the strengthened hypothesis. It also does not claim that the constructed witness recovers an S8-chosen orientation; the model witness uses a forward/backward side convention, not a recovery of a specific choice.

The practical consequence is that the framework can build a committed witness for any posting event, provided the nonnegativity gap is filled. This is a step toward deriving physical structure from the ledger, but the gap itself remains open. The theorem is a conditional bridge, not a final derivation.

THEOREM committedEventWitness_of_s8_existential_with_nonneg · IndisputableMonolith/Foundation/PairKernelConstructedCovectorEventOccurrenceJoin.lean
committedEventWitness_of_s8_existential_with_nonneg · IndisputableMonolith/Foundation/PairKernelConstructedCovectorEventOccurrenceJoin.lean:487 
/-- Consume S8's existential half by genuinely eliminating it: the ledger
states of the produced witness are exactly those supplied by
`s8_existential_half_of_event` (`realizedPrimitivePostingPair_has_ledger_event`).
What the corpus does not supply for those S8 witnesses, the `NonnegLedger`
strengthening (the named OPEN gap `MissingNonnegLedgerOnS8PostingWitness`)
and the event-spatial occurrence tie, is carried as one universally
quantified hypothesis over whatever pre/post states S8 produces. -/
theorem committedEventWitness_of_s8_existential_with_nonneg
    {N : ℕ} [NeZero N]
    (event : RealizedPostingEvent3 N)
    (hmissing :
      ∀ A B : EventLedgerState,
        PostingStep A B →
          JMinimalPostingStep A B →
            (∑ k : Fin (TorusCard3 N),
              divF (elementaryPosting event.1.1 event.1.2) k) = 0 →
              NonnegLedger (d := 3) A ∧
                EventSpatialOccurrenceTie event
                  (postingOfProfiles (d := 3) A B).1
                  (postingOfProfiles (d := 3) A B).2) :
    Nonempty (CommittedEventWitness event) := by
  obtain ⟨A, B, hstep, hmin, hcons⟩ := s8_existential_half_of_event event
  obtain ⟨hn, htie⟩ := hmissing A B hstep hmin hcons
  exact
    ⟨committedEventWitness_of_posting_with_nonneg event A B hn hstep
      hmin htie⟩
THEOREM committedEventWitness_of_s8_existential_with_nonneg · IndisputableMonolith/Foundation/PairKernelConstructedCovectorEventOccurrenceJoin.lean
committedEventWitness_of_s8_existential_with_nonneg · IndisputableMonolith/Foundation/PairKernelConstructedCovectorEventOccurrenceJoin.lean:487 
/-- Consume S8's existential half by genuinely eliminating it: the ledger
states of the produced witness are exactly those supplied by
`s8_existential_half_of_event` (`realizedPrimitivePostingPair_has_ledger_event`).
What the corpus does not supply for those S8 witnesses, the `NonnegLedger`
strengthening (the named OPEN gap `MissingNonnegLedgerOnS8PostingWitness`)
and the event-spatial occurrence tie, is carried as one universally
quantified hypothesis over whatever pre/post states S8 produces. -/
theorem committedEventWitness_of_s8_existential_with_nonneg
    {N : ℕ} [NeZero N]
    (event : RealizedPostingEvent3 N)
    (hmissing :
      ∀ A B : EventLedgerState,
        PostingStep A B →
          JMinimalPostingStep A B →
            (∑ k : Fin (TorusCard3 N),
              divF (elementaryPosting event.1.1 event.1.2) k) = 0 →
              NonnegLedger (d := 3) A ∧
                EventSpatialOccurrenceTie event
                  (postingOfProfiles (d := 3) A B).1
                  (postingOfProfiles (d := 3) A B).2) :
    Nonempty (CommittedEventWitness event) := by
  obtain ⟨A, B, hstep, hmin, hcons⟩ := s8_existential_half_of_event event
  obtain ⟨hn, htie⟩ := hmissing A B hstep hmin hcons
  exact
    ⟨committedEventWitness_of_posting_with_nonneg event A B hn hstep
      hmin htie⟩
OPEN MissingNonnegLedgerOnS8PostingWitness · IndisputableMonolith/Foundation/PairKernelConstructedCovectorEventOccurrenceJoin.lean
MissingNonnegLedgerOnS8PostingWitness · IndisputableMonolith/Foundation/PairKernelConstructedCovectorEventOccurrenceJoin.lean:459 
/-- **Named OPEN residual (actual missing proposition).**  The S8 lemma
`realizedPrimitivePostingPair_has_ledger_event` returns a posting /
minimum-J / conservation witness but not `NonnegLedger` on the pre-state.
This proposition states the missing strengthening.  It is **not** proved or
inhabited as evidence in this module. -/
def MissingNonnegLedgerOnS8PostingWitness : Prop :=
  ∀ {N : ℕ} [NeZero N] (e : PostingPair3 N),
    e ∈ realizedPrimitivePostingPairs3 N →
      ∃ A B : LedgerPostingAdjacency.LedgerState 3,
        NonnegLedger (d := 3) A ∧
          PostingStep A B ∧
            JMinimalPostingStep A B ∧
              (∑ k : Fin (TorusCard3 N),
                divF (elementaryPosting e.1 e.2) k) = 0

What this page does not claim

The theorem does not prove that the nonnegativity condition holds for all posting events. The theorem does not recover an S8-chosen orientation; it uses a forward/backward side convention.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND