pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Foundation.PostingExtensivity

show as:
view Lean formalization →

The PostingExtensivity module defines the posting potential Π(x) = ½(x + x^{-1}) as the shifted J-cost that satisfies the d'Alembert equation inside a zero-parameter comparison ledger. Researchers deriving the Fibonacci recurrence and phi scale from ledger axioms cite it when crossing from canonicality to hierarchy dynamics. The module establishes this via algebraic identities that follow directly from the Recognition Composition Law applied to the ledger's symmetric cost and conserved charge.

claim$Π(x) = J(x) + 1 = ½(x + x^{-1})$, where $J$ is the J-cost obeying the Recognition Composition Law $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$ inside a ZeroParameterComparisonLedger.

background

This module belongs to the Foundation layer and imports the J-cost from the Cost module together with the ZeroParameterComparisonLedger from LedgerCanonicality. The ledger packages a countable discrete carrier, local symmetric binary comparisons, and a conserved log-charge scalar. HierarchyEmergence supplies the upstream result that zero-parameter scale closure on such a ledger necessarily produces a minimal hierarchy and forces φ as the unique admissible scale.

proof idea

The module consists of the PostingPotential definition followed by lemmas such as posting_scales_compose, closure_forces_additive, posting_extensivity_forces_phi, and posting_gives_unit_recurrence. Each follows by direct substitution of the shifted J-cost into the Recognition Composition Law and simplification using the ledger's conservation and positivity properties. The argument is purely equational with no tactics beyond rewriting.

why it matters in Recognition Science

The module supplies the posting potential and its extensivity properties to HierarchyDynamics, which closes the T5 to T6 bridge by extracting the Fibonacci recurrence from discrete ledger composition. It thereby advances the forcing chain from J-uniqueness to the self-similar fixed point φ. The downstream module doc-comment states that this resolves the structural gap between physically primitive axioms and the recurrence.

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)