Lax58.StructuralPresentation

Structural presentations of finite data

concepts/Lax58/StructuralPresentation.lean · lax-58

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

Finite data may be presented through one universal shape: binary trees with natural-number leaves. A presentation consists of a map into this shape and a partial inverse. Its structural size counts shape nodes, independently of any binary serialization or in-memory layout.

$Presentation$ is deliberately low-level infrastructure. An arbitrary presentation is not automatically a neutral complexity-theoretic input representation: its forward map could compute and attach derived advice. Advice-freedom is supplied downstream by complete, kernel-checked constructor equations built from the fixed structural vocabulary.

Natural payload magnitude is recorded separately from structural size. This separation is useful for word-machine applications: a large natural leaf still occupies one structural node, but may require a wider machine word.

Lean source view on GitHub

1	/-!
2	---
3	title: Structural presentations of finite data
4	type: definition
5	---
6
7	Finite data may be presented through one universal shape: binary trees with
8	natural-number leaves. A presentation consists of a map into this shape and a
9	partial inverse. Its structural size counts shape nodes, independently of any
10	binary serialization or in-memory layout.
11
12	`Presentation` is deliberately low-level infrastructure. An arbitrary
13	presentation is not automatically a neutral complexity-theoretic input
14	representation: its forward map could compute and attach derived advice.
15	Advice-freedom is supplied downstream by complete, kernel-checked constructor
16	equations built from the fixed structural vocabulary.
17
18	Natural payload magnitude is recorded separately from structural size. This
19	separation is useful for word-machine applications: a large natural leaf still
20	occupies one structural node, but may require a wider machine word.
21	-/
22
23	namespace Lax58.StructuralPresentation
24
25	universe u
26
27	/-- The universal shape of structurally finite data. -/
28	inductive Raw where
29	\| nat : Nat → Raw
30	\| pair : Raw → Raw → Raw
31	deriving DecidableEq
32
33	namespace Raw
34
35	/-- Number of nodes in a universal structural representation. -/
36	def nodes : Raw → Nat
37	\| .nat _ => 1
38	\| .pair a b => nodes a + nodes b + 1
39
40	/-- Largest natural-number payload occurring in a representation. -/
41	def maxNat : Raw → Nat
42	\| .nat n => n
43	\| .pair a b => max a.maxNat b.maxNat
44
45	/-- Every natural payload in a representation fits into a `w`-bit word. -/
46	def PayloadsFitInWord (raw : Raw) (w : Nat) : Prop :=
47	raw.maxNat < 2 ^ w
48
49	end Raw
50
51	/-- An encoder into the universal shape and a partial inverse. -/
52	structure Presentation (α : Type u) where
53	toRaw : α → Raw
54	fromRaw : Raw → Option α
55
56	/-- Package an injective structural map as a low-level presentation by
57	choosing a preimage on its range. This construction certifies no complexity
58	or constructor-structurality property of the supplied map. -/
59	noncomputable def presentationOf {α : Type u} (f : α → Raw) : Presentation α := by
60	classical
61	exact {
62	toRaw := f
63	fromRaw := fun raw =>
64	if h : ∃ x, f x = raw then some (Classical.choose h) else none
65	}
66
67	namespace Presentation
68
69	/-- Distinguished representations round-trip. -/
70	def Lawful {α : Type u} (P : Presentation α) : Prop :=
71	∀ x : α, P.fromRaw (P.toRaw x) = some x
72
73	/-- Distinct values have distinct structural representations. -/
74	def Faithful {α : Type u} (P : Presentation α) : Prop :=
75	Function.Injective P.toRaw
76
77	/-- Structural size before any serialization or memory layout is chosen. -/
78	def structuralSize {α : Type u} (P : Presentation α) (x : α) : Nat :=
79	(P.toRaw x).nodes
80
81	/-- Largest natural payload in the distinguished representation. -/
82	def maxNat {α : Type u} (P : Presentation α) (x : α) : Nat :=
83	(P.toRaw x).maxNat
84
85	/-- Every natural payload of a value fits into a `w`-bit word. -/
86	def PayloadsFitInWord {α : Type u}
87	(P : Presentation α) (x : α) (w : Nat) : Prop :=
88	(P.toRaw x).PayloadsFitInWord w
89
90	end Presentation
91
92	end Lax58.StructuralPresentation
93

Builds on

none

Used by

From Mathlib

none

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Structural presentations of finite data

Flags

Flag this concept