AreaOperator
plain-language theorem explainer
AreaOperator packages a self-adjoint operator on an RS Hilbert space with the simplicial surface whose recognition flux it measures. Quantum-gravity researchers deriving discrete area spectra from ledger bits cite this definition when stating the area quantization theorem. The declaration is a pure structure definition carrying no proof obligations.
Claim. Let $H$ be a type with an instance of RSHilbertSpace. An area operator consists of a set $S$ of 3-simplices, a map op$: H→H$, and a proof that op is self-adjoint: for all states ψ₁, ψ₂ one has ⟨ψ₁, op ψ₂⟩ = ⟨op ψ₁, ψ₂⟩.
background
The module formalizes the claim that spatial area is quantized in integer multiples of ℓ₀², obtained from the planarity constraints of the eight-tick cycle together with the simplicial ledger. RSHilbertSpace supplies the inner product on the state space while Simplex3 denotes the 3-simplices whose faces each carry one bit of recognition flux. Upstream cost-algebra results supply the shifted functional H(x) = J(x) + 1 that converts the recognition composition law into the d'Alembert form used for flux bookkeeping.
proof idea
AreaOperator is introduced as a structure definition. It simply declares the three fields surface, op and is_self_adjoint; no lemmas are applied and no tactics are executed.
why it matters
The structure supplies the type required by the area_quantization theorem, which states that eigenvalues equal integer multiples of ℓ₀² on ledger eigenstates, and by the minimal_area_eigenvalue theorem that fixes the smallest nonzero eigenvalue at exactly ℓ₀². It realizes the T7–T8 prediction that the eight-tick octave forces D = 3 and therefore discrete area quanta. The hypothesis H_AreaQuantization encodes the empirical claim that the operator sums local flux bits; downstream results close the quantization argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.