pith. sign in
module module high

IndisputableMonolith.Relativity.InformationConservation

show as:
view Lean formalization →

This module establishes information conservation as a structural property of the Recognition Science ledger: total content is preserved under transformations because the J-cost function is defined on all states with no sinks. Researchers deriving relativistic conservation laws from RS foundations would cite it. The structure extends the upstream determinism result on unique minimizers via convexity of J.

claimIn Recognition Science the ledger substrate obeys information conservation: total content $I$ satisfies $I' = I$ under any update, with the strictly convex $J$-cost defined on $(0,∞)$ excluding sinks.

background

The module resides in the Relativity domain and imports the Determinism module. That upstream result states: 'The J-cost function is strictly convex on (0, ∞). For any constrained optimization (ledger update), the minimizer is UNIQUE.' The module doc-comment supplies the core setting: 'In RS, the ledger is the fundamental substrate. Total ledger content (information) is conserved: entries can move, transform, but not vanish. This is structural: the cost function J is defined on all states; there is no sink that destroys information.'

proof idea

This is a module collecting related theorems rather than a single proof. It organizes results around ledger_conservative and information_conserved by applying the convexity and uniqueness from the determinism import to rule out sinks.

why it matters in Recognition Science

The module supplies the conservation substrate required for relativistic extensions in Recognition Science. It directly implements the structural invariance stated in its doc-comment and feeds the sibling theorems on no_information_sink and information_conserved_implies_no_distinct_zero_defect. No downstream used_by edges are recorded yet.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)