mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
127 lines
4.6 KiB
Text
127 lines
4.6 KiB
Text
import Semantics.FixedPoint
|
|
import Semantics.OrthogonalAmmr
|
|
import Semantics.LandauerCompression
|
|
import Semantics.EnvironmentMechanics
|
|
|
|
namespace Semantics.AtomicResolution
|
|
|
|
open Semantics
|
|
open Semantics.OrthogonalAmmr
|
|
open Semantics.LandauerCompression
|
|
open Semantics.EnvironmentMechanics
|
|
|
|
/--
|
|
Conservative witness for what atomic support remains distinguishable after
|
|
compression. This does not identify chemistry; it only budgets distinguishable
|
|
sites and bounded coordinate residual against an admissible environment witness.
|
|
-/
|
|
structure AtomicResolutionWitness where
|
|
environment : EnvironmentWitness
|
|
resolvedSites : Nat
|
|
occupancyBound : Nat
|
|
coordinateResidual : Q16_16
|
|
deriving Repr, Inhabited, DecidableEq
|
|
|
|
/--
|
|
The retained basis supports at least the claimed number of distinguishable
|
|
sites.
|
|
-/
|
|
def siteCovered (w : AtomicResolutionWitness) : Bool :=
|
|
decide (w.resolvedSites ≤ w.environment.summary.shape.basisDim)
|
|
|
|
/--
|
|
The claimed occupancy cardinality does not exceed the supported site count.
|
|
-/
|
|
def occupancyCovered (w : AtomicResolutionWitness) : Bool :=
|
|
decide (w.occupancyBound ≤ w.resolvedSites)
|
|
|
|
/--
|
|
Coordinate-level residual remains inside the environment residual budget.
|
|
-/
|
|
def coordinateResidualBounded (w : AtomicResolutionWitness) : Bool :=
|
|
Q16_16.le w.coordinateResidual w.environment.residualBudget
|
|
|
|
/--
|
|
Atomic-resolution claims are admissible only when the environment is already
|
|
admissible and the site / occupancy / residual bounds all hold.
|
|
-/
|
|
def atomicallyAdmissible (w : AtomicResolutionWitness) : Bool :=
|
|
longRangeAdmissible w.environment &&
|
|
siteCovered w &&
|
|
occupancyCovered w &&
|
|
coordinateResidualBounded w
|
|
|
|
/--
|
|
Canonical constructor over an existing environment witness.
|
|
-/
|
|
def witnessOfEnvironment
|
|
(environment : EnvironmentWitness)
|
|
(resolvedSites occupancyBound : Nat)
|
|
(coordinateResidual : Q16_16) :
|
|
AtomicResolutionWitness :=
|
|
{ environment := environment
|
|
, resolvedSites := resolvedSites
|
|
, occupancyBound := occupancyBound
|
|
, coordinateResidual := coordinateResidual }
|
|
|
|
/--
|
|
If all constituent bounds hold, the atomic-resolution witness is admissible.
|
|
-/
|
|
theorem atomicallyAdmissibleOfBounds
|
|
(w : AtomicResolutionWitness)
|
|
(hEnv : longRangeAdmissible w.environment = true)
|
|
(hSites : siteCovered w = true)
|
|
(hOcc : occupancyCovered w = true)
|
|
(hCoord : coordinateResidualBounded w = true) :
|
|
atomicallyAdmissible w = true := by
|
|
simp [atomicallyAdmissible, hEnv, hSites, hOcc, hCoord]
|
|
|
|
/--
|
|
The site-coverage predicate exposes the underlying cardinality bound.
|
|
-/
|
|
theorem resolvedSitesLeBasisDim
|
|
(w : AtomicResolutionWitness)
|
|
(hSites : siteCovered w = true) :
|
|
w.resolvedSites ≤ w.environment.summary.shape.basisDim := by
|
|
simpa [siteCovered] using hSites
|
|
|
|
/--
|
|
Compression cannot increase the number of distinguishable sites beyond the
|
|
pre-compression retained basis together with the erased directions.
|
|
-/
|
|
theorem compressionContractsAtomicResolution
|
|
(compression : CompressionWitness)
|
|
(w : AtomicResolutionWitness)
|
|
(hAlign : w.environment.summary = compression.postSummary)
|
|
(hContract : compression.postSummary.shape.basisDim ≤ compression.preSummary.shape.basisDim)
|
|
(hSites : siteCovered w = true) :
|
|
w.resolvedSites + erasedDirections compression ≤
|
|
compression.preSummary.shape.basisDim := by
|
|
have hResolved :
|
|
w.resolvedSites ≤ compression.postSummary.shape.basisDim := by
|
|
simpa [hAlign] using resolvedSitesLeBasisDim w hSites
|
|
unfold erasedDirections
|
|
have hStep :
|
|
w.resolvedSites + (compression.preSummary.shape.basisDim - compression.postSummary.shape.basisDim) ≤
|
|
compression.postSummary.shape.basisDim +
|
|
(compression.preSummary.shape.basisDim - compression.postSummary.shape.basisDim) := by
|
|
exact Nat.add_le_add_right hResolved _
|
|
calc
|
|
w.resolvedSites + (compression.preSummary.shape.basisDim - compression.postSummary.shape.basisDim)
|
|
≤ compression.postSummary.shape.basisDim +
|
|
(compression.preSummary.shape.basisDim - compression.postSummary.shape.basisDim) := hStep
|
|
_ = compression.preSummary.shape.basisDim := by
|
|
exact Nat.add_sub_of_le hContract
|
|
|
|
def sampleAtomicEnvironment : EnvironmentWitness :=
|
|
witnessOfCompression sampleWitness 1 (Q16_16.ofInt 2) Q16_16.one Q16_16.one
|
|
|
|
def sampleAtomicResolutionWitness : AtomicResolutionWitness :=
|
|
witnessOfEnvironment sampleAtomicEnvironment 1 1 Q16_16.one
|
|
|
|
#eval siteCovered sampleAtomicResolutionWitness
|
|
#eval occupancyCovered sampleAtomicResolutionWitness
|
|
#eval coordinateResidualBounded sampleAtomicResolutionWitness
|
|
#eval atomicallyAdmissible sampleAtomicResolutionWitness
|
|
|
|
end Semantics.AtomicResolution
|