Pith. sign in
module module high

IndisputableMonolith.Foundation.Determinism

show as:
view Lean formalization →

The Foundation.Determinism module establishes determinism of recognition projections by proving unique minimizers for constrained J-cost problems. Researchers deriving variational dynamics or probability interpretations would cite it. The argument structure combines the algebraic fact J''(x) = x^{-3} > 0 with the unique_minimizer_principle and the law of existence.

claimFor the J-cost with second derivative $J''(x) = x^{-3} > 0$ ($x > 0$), every ConstrainedProblem has a unique minimizer; under the law of existence ($x$ exists $\\$ defect$(x) = 0$), this yields determinism_resolution.

background

The module imports Cost.Convexity, whose doc states it proves Jlog(t) = cosh t - 1 strictly convex on R and Jcost(x) = ½(x + x^{-1}) - 1 strictly convex on R_+, foundational for T5 J-uniqueness. It also imports LawOfExistence, which formalizes x exists iff defect(x) = 0. Sibling declarations introduce Observer, project, projection_lossy, ConstrainedProblem, unique_minimizer_principle, and determinism_resolution; the supplied DOC_COMMENT identifies J''(x) = x^{-3} > 0 as the key strict-convexity fact.

proof idea

The module first records the direct differentiation establishing J''(x) > 0, defines ConstrainedProblem, invokes unique_minimizer_principle to obtain uniqueness, and concludes with determinism_resolution. It is a short collection of supporting results rather than a single long tactic script.

why it matters in Recognition Science

This module supplies determinism_resolution, which is imported by VariationalDynamics (F-008: the ledger update rule), ProbabilityMeaningStructure (PH-006: probability equals J-cost projection weight), and Relativity.InformationConservation (BH-002: black-hole information resolution). It converts the upstream convexity of Jcost into a determinism claim required by those downstream modules.

scope and limits

used by (3)

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 (7)