Holography Recognition Event Capacity Event Access Additive

Additivity of access

In information theory, entropy measures the average information carried by an event. The Recognition Science framework defines a specific recognition event, a single act of resolving a signal into discrete outcomes, and assigns it a fixed information content of about 1.741 nats, or 2.51 bits. This number is not chosen freely; it is computed as the Shannon entropy of a probability distribution forced by the framework's axioms. The declaration eventAccess_additive states a simple scaling property: the information accessible across j plus k recognition events equals the sum of the information accessible across j events and across k events separately.

This additivity is true by definition. The framework defines eventAccess k as k times the per-event information, so the equation eventAccess (j + k) = eventAccess j + eventAccess k follows immediately from ordinary arithmetic. It records the intended scaling shape: if one event gives H nats, two events give 2H, three give 3H, and so on. The declaration is a theorem in the machine-checked library of formal theorems, but its content is definitional linearity, not a physical law about how independent events combine.

The substantive claim, that the entropy of k independent recognition events equals k times the single-event entropy via a product measure, remains an open target. The framework has not yet proved that independence factorization. What eventAccess_additive establishes is only the algebraic identity that follows from the chosen definition. It does not assert that recognition events are independent, that their information adds in any physical sense, or that the per-event rate applies to any particular real-world channel.

The practical consequence of the declaration is modest but real: it fixes the arithmetic framework within which access capacity will be discussed. Any future theorem about multiple events must respect this scaling shape, or explicitly revise the definition. The additivity is a constraint on how the framework talks about accumulated information, not a statement about how information actually accumulates in nature.

/-- Definitional linearity of `eventAccess` (MODEL). This is true by the definition
`eventAccess k = k·H`; it is NOT the substantive product-measure additivity theorem (which
is open). Kept only to record the scaling shape. -/
theorem eventAccess_additive (j k : ℕ) :
    eventAccess (j + k) = eventAccess j + eventAccess k := by
  unfold eventAccess; push_cast; ring

/-- The information accessible across `k` recognition events, at the forced per-event
rate. MODEL definition: this is `k·H` by construction. The SUBSTANTIVE additivity (that
the entropy of `k` INDEPENDENT events equals `k·H`, via the product measure and the
forced-measure factorization `Factorizes`) is the open next target, NOT this definitional
linearity. -/
noncomputable def eventAccess (k : ℕ) : ℝ := (k : ℝ) * forcedEntropy

What this page does not claim

The declaration does not prove that recognition events are independent. It does not establish that information adds physically across events. It does not claim the per-event rate applies to any particular real-world channel.

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/Holography/RecognitionEventCapacity.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: