Repository navigation
Expand file tree
/
Copy pathRMQRankSelect.lean
More file actions
50 lines (46 loc) · 2.74 KB
/
Copy pathRMQRankSelect.lean
File metadata and controls
50 lines (46 loc) · 2.74 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
import RMQ.Core.RankSelectPublic
import RMQ.Core.RankSelectPublicRAM
/-!
# Standalone rank/select spoke
This import root exposes the plain-bitvector rank/select API and public
Jacobson/Clark theorem. It avoids the final RMQ capstone and backend roots, but
the current proof-support import closure still shares the succinct-space,
shape/lower-bound infrastructure. The exposed API is plain bitvector
access/rank/select rather than an RMQ/LCA/Fischer-Heun backend.
The public plain-bitvector headline theorem is
`RMQ.RankSelect.jacobsonClarkNPlusOConstantQuery`; the strengthened
word-bounded profile is
`RMQ.RankSelect.jacobsonClarkWordBoundedNPlusOConstantQuery`.
The fixed-weight compressed/FID capstone family surface is
`RMQ.RankSelect.compressedFIDFixedWeightFamilyProfile`, with headline alias
`RMQ.Headlines.rankSelectCompressedFIDFixedWeightFamilyProfile`. It proves a
concrete compressed payload budget
`fixedWeightPayloadBudget bits + o(n)` with uniform constant modeled access,
rank, and select queries for every `bits : List Bool`. The pointwise theorem
`RMQ.RankSelect.compressedFIDFixedWeightConstantQueryProfile` remains available.
The single public fused capstone is
`RMQ.RankSelect.compressedFIDFixedWeightGlobalPayloadStoreFusedProfile`, with
headline alias
`RMQ.Headlines.rankSelectCompressedFIDFixedWeightGlobalPayloadStoreFusedProfile`.
It packages the compressed family profile, interpreted replay, target-independent
global payload store, and bounded trace-local event-width story in one theorem.
The interpreted replay surface
`RMQ.RankSelect.compressedFIDFixedWeightInterpretedFamilyProfile` strengthens
the same theorem shape by routing access/rank/select reads through `WordRAM`
bridges. These are word-RAM/indexed-read model theorems, not Lean runtime
claims. The access, rank, and select legs additionally expose store-backed
trace packets:
`RMQ.RankSelect.compressedFIDFixedWeightAccessTraceResult_execution_story` and
`RMQ.RankSelect.compressedFIDFixedWeightRankTraceResult_execution_story`, and
`RMQ.RankSelect.compressedFIDFixedWeightSelectTraceResult_execution_story`.
For each fixed `bits` and `target`, the relabeled access/rank/select packets
are combined under one concrete target-indexed payload store by
`RMQ.RankSelect.compressedFIDFixedWeightTargetGlobalPayloadStore_execution_story`.
The stronger public global-store theorem
`RMQ.RankSelect.compressedFIDFixedWeightGlobalPayloadStore_execution_story`
uses one target-independent store for shared access plus rank false/true and
select false/true. Its bounded companion
`RMQ.RankSelect.compressedFIDFixedWeightGlobalPayloadStore_bounded_execution_story`
adds trace-local finite-width bounds for every payload-read address and every
natural operand/result exposed by word-local rank/select primitives.
-/