pith. sign in
module module high

IndisputableMonolith.Foundation.PostingExtensivity

show as:
view Lean formalization →

The PostingExtensivity module defines the posting potential as the shifted J-cost satisfying the d'Alembert equation inside zero-parameter comparison ledgers. Researchers deriving the T5 to T6 bridge would cite it when establishing extensivity from ledger composition. The module supplies a sequence of definitions and lemmas that connect the J-cost to phi-forcing properties.

claimThe posting potential is the shifted J-cost satisfying the d'Alembert equation: $\Pi(x) = J(x) + 1 = \frac12(x + x^{-1})$, where $J(x) = \frac12(x + x^{-1}) - 1$.

background

The module sits inside the Recognition Science forcing chain and imports the ZeroParameterComparisonLedger from LedgerCanonicality. That ledger packages a countable carrier for discrete states, local binary comparison with symmetric cost, and a conserved log-charge scalar. It also imports HierarchyEmergence, whose doc-comment states that a zero-parameter comparison ledger with multilevel composition necessarily produces a minimal hierarchy and forces phi as the unique admissible scale.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module feeds the posting potential and its extensivity lemmas directly into HierarchyDynamics. That downstream module closes the T5 to T6 gap by deriving the Fibonacci recurrence from primitive ledger axioms, as described in its doc-comment on resolving the deepest structural gap in the Recognition Science forcing chain.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (11)