cone_entropy_bound
plain-language theorem explainer
The theorem states that entropy inside a light cone is at most its area divided by four times the square of the recognition length. Discrete-spacetime modelers and holographic-bound researchers would cite the result when exporting cone constraints without explicit step counts. The proof is a one-line wrapper that applies the cone_entropy_bound method from the ConeEntropyFacts typeclass.
Claim. Let $cone$ be a light cone and $area$ a real number. Then the entropy of the cone satisfies $entropy(cone) ≤ area / (4 λ_rec²)$, assuming the ConeEntropyFacts hypothesis.
background
Entropy is defined in the initial-condition module as the total defect of a configuration, so that zero defect yields the minimum entropy state. Thermodynamic variants in the Boltzmann and partition-function modules give entropy as $β⟨E⟩ + k ln Z$ or $k_B (ln Z + β⟨E⟩)$. The present module exports a verification-level cone bound that removes the step-count parameter from the discrete light-cone construction.
proof idea
The proof is a one-line wrapper that applies ConeEntropyFacts.cone_entropy_bound cone area.
why it matters
The result supplies the concrete bound required by the ConeEntropyFacts class and is instantiated by coneEntropyStub in Relativity.NewFixtures. It fills the holographic-principle step in the cone-export chain, capping entropy at area over 4 λ_rec². The module documentation flags the assumption status and refers to docs/Assumptions.md for a future voxel-counting derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.