Configuration
plain-language theorem explainer
A structure packages N positive real numbers as ledger entries to formalize the zero-defect initial state. Foundational physicists and cosmologists cite it when converting the Past Hypothesis into the Past Theorem. The declaration is a plain structure definition that enforces positivity on each entry through a Fin-indexed map to the reals.
Claim. A configuration of $N$ ledger entries is a map $entries : Fin(N) → ℝ$ such that $entries(i) > 0$ for every index $i$.
background
The module formalizes the low-entropy initial condition as F-005. It shows that the only RSExists state is the unity value $x=1$ with zero defect, so a collection of $N$ such entries yields total defect zero, which is the global minimum entropy state. Defect is the functional that equals $J$ on positive reals, as defined upstream in LawOfExistence. A closely related single-value structure appears in RecognitionForcing, where Configuration carries a positive real value together with its positivity witness.
proof idea
This is a structure definition with no proof body. It directly introduces the type of configurations by declaring the entries field and the accompanying positivity predicate.
why it matters
The structure supplies the domain for the entropy definition and for the past_theorem, which proves that the unity configuration is the unique zero-defect state and the global minimizer of total defect. It thereby resolves the F-005 registry item, converting the Past Hypothesis into the Past Theorem. Within the Recognition framework it rests on the zero-cost state forced by the cost axioms and on J-uniqueness from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.