ConeEntropyFacts
plain-language theorem explainer
ConeEntropyFacts encodes the holographic area-law bound on light-cone entropy as a typeclass assumption. Researchers deriving discrete causality or exporting cone bounds to relativity would cite it when invoking the inequality without an explicit step count. The declaration is a bare class definition that introduces the bound as a field with no internal proof or reduction.
Claim. Assume that for any light cone and its area the entropy satisfies $entropy(cone) ≤ area / (4 λ_rec²)$.
background
The ConeExport module supplies a verification-level statement of the cone bound that removes the discrete step parameter from the light-cone reach relation. Upstream Kinematics structures in Causality.Basic, ConeBound and Reach each consist of a step : α → α → Prop relation. The sibling cone_entropy_bound theorem applies the class to state the bound and explicitly labels it an axiom whose justification would require voxel counting together with the holographic principle.
proof idea
The declaration is a class definition whose sole field is the cone_entropy_bound proposition. No lemmas are applied and no tactics appear; the construction is a direct hypothesis interface.
why it matters
ConeEntropyFacts supplies the assumption consumed by the cone_entropy_bound theorem, which in turn feeds the coneEntropyStub fixture in Relativity.NewFixtures. It implements the placeholder for holographic entropy bounds described in the module documentation, linking the area-law form to the recognition length λ_rec that appears throughout the constant derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.