GUAF Notation Decoder — Building the Internal Model
Status: proposal / active working document
Date: 2026-10-08
Context: Scott's request to build a stable mental model of the mathematics underlying the GUAF formalization, specifically targeting the gap between formal notation and intuitive meaning. This document operationalizes the Five Questions scaffold from 0004-math-foundation-proposal.md by applying it directly to every symbol in Guaf.Core.
Epistemic class: proposal (a learning protocol awaiting disposition)
The Core Method: Symbol → Role → Meaning
When you encounter a mathematical expression, do not try to "read" it like English prose. Instead, classify every symbol into one of three roles:
| Role | Question | Analogy (Software Engineering) |
|---|---|---|
| Noun (Object) | What thing is this? | A type, a struct, an interface |
| Verb (Operation/Map) | What action or transformation does this perform? | A function, a method, a cast |
| Constraint (Axiom/Rule) | What must be true about these nouns and verbs? | An invariant, a contract, a type bound |
Once classified, the notation stops being alien symbols and becomes a specification — exactly like reading a TypeScript interface or a Rust trait.
Decoding Guaf.Core — Line by Line
This section takes the actual Lean code we compiled today and translates it through the scaffold.
1. The Universe Declaration
universe u
| Aspect | Decoding |
|---|---|
| Symbol | universe u |
| Role | Constraint (meta-level) |
| Plain meaning | "We are working at a specific level of 'size'." In Lean, types have types. Type 0 contains things like Nat and String. Type 1 contains Type 0. u is a variable standing for "some level." Think of it as a generic type parameter for the size of the container, preventing paradoxes where a set contains itself. |
| SE analogy | Like declaring <T> in generics, but for the type system's own hierarchy. |
2. The Site (The Space of Contexts)
class Site (Ctx : Type u) extends PartialOrder Ctx where
top : Ctx
is_top : ∀ U : Ctx, U ≤ top
| Aspect | Decoding |
|---|---|
| Nouns | Site (the structure), Ctx (the type of "contexts" or "faces"), top (a specific context) |
| Verbs | ≤ (the partial order relation — "is contained in" or "is more specific than") |
| Constraints | extends PartialOrder (the contexts must form a valid partial order: reflexive, antisymmetric, transitive), is_top (every context U is below or equal to top) |
| Plain meaning | A Site is a collection of viewpoints (contexts) organized by specificity. There is a "widest" viewpoint (top) that tries to see everything at once. Every other viewpoint is narrower (more local). |
| SE analogy | A directory tree where top is / (root) and every other path is a subdirectory. Or a class hierarchy where top is object. |
| GUAF intuition | The "whole" — the attempt to name the referent globally. |
3. Proper Contexts
def Proper {Ctx : Type u} [Site Ctx] (U : Ctx) : Prop := U < Site.top
| Aspect | Decoding |
|---|---|
| Nouns | Proper (a property/predicate), U (a context), Prop (the type of true/false statements) |
| Verbs | < (strictly less than — strictly more specific than) |
| Constraints | [Site Ctx] means "assuming Ctx has a Site structure" |
| Plain meaning | A context is "proper" if it is NOT the global top. It's a genuinely local viewpoint. |
| SE analogy | isProper = (path !== '/') |
4. The Presheaf (The Content Assignment)
structure Presheaf (Ctx : Type u) [Site Ctx] where
F : Ctx → Type u
restr : ∀ {U V : Ctx}, V ≤ U → F U → F V
| Aspect | Decoding |
|---|---|
| Nouns | Presheaf (the data structure), F (the assignment function), F U (the "content" available at context U) |
| Verbs | → (maps to), restr (restriction — the operation that narrows content from a broad view to a narrow view) |
| Constraints | If V ≤ U (V is more specific than U), then there must exist a restr map from F U to F V |
| Plain meaning | For every viewpoint, we assign some data. When we zoom in from a broad viewpoint to a narrow one, we can consistently restrict the data. |
| SE analogy | A configuration system: F(U) is the config visible at scope U. restr is how you inherit/shadow config when moving to a child scope V. |
| GUAF intuition | The manifold of contents across all faces. |
5. Questions and Global Resolvability
structure Question {Ctx : Type u} [Site Ctx] (F : Presheaf Ctx) where
spec : F.F Site.top → Prop
def GloballyResolvable {Ctx : Type u} [Site Ctx] (F : Presheaf Ctx) (q : Question F) : Prop :=
∃ c : F.F Site.top, q.spec c
| Aspect | Decoding |
|---|---|
| Nouns | Question (a demand/specification), spec (the predicate defining what would satisfy the question), c (a candidate answer) |
| Verbs | ∃ ("there exists"), function application q.spec c ("does c satisfy the spec?") |
| Constraints | A question is defined over F.F Site.top — the content at the global top |
| Plain meaning | A question asks: "Is there a global piece of data that satisfies my condition?" If yes, it's globally resolvable. |
| SE analogy | A unit test assertion that can only pass if the root/global state satisfies a condition. |
6. The Ladder
structure Ladder {Ctx : Type u} [Site Ctx] (F : Presheaf Ctx) where
mu : Question F → Question F
| Aspect | Decoding |
|---|---|
| Nouns | Ladder, mu (the ladder map) |
| Verbs | mu takes a Question and returns a new Question |
| Plain meaning | Given any question, the ladder produces a "higher" question (the question about whether the original question is resolvable). |
| SE analogy | A meta-query generator. Given a query Q, mu(Q) is "can Q be answered?" |
7. Productivity
def Productive {Ctx : Type u} [Site Ctx] (F : Presheaf Ctx) (L : Ladder F) : Prop :=
∀ (n : Nat) (q : Question F), ¬ GloballyResolvable F ((L.mu ^[n]) q)
| Aspect | Decoding |
|---|---|
| Symbols | ∀ (for all), ¬ (not), ^[n] (apply n times) |
| Plain meaning | No matter how many times you climb the ladder (apply mu), starting from any question, you never reach a globally resolvable one. The ladder never terminates at the top. |
| SE analogy | An infinite regress of meta-queries. Query → "Can I answer this?" → "Can I answer whether I can answer this?" → ... forever without resolution. |
8. Representability
class Representable {Ctx : Type u} [Site Ctx] (F : Presheaf Ctx) where
res : ∀ (U : Ctx), Proper U → F.F U → Question F → Prop
faithful : ∀ (U : Ctx) (hU : Proper U),
(∀ c q, res U hU c q → ∃ d : F.F U, d = c)
| Aspect | Decoding |
|---|---|
| Nouns | res (internal resolution predicate), faithful (consistency guarantee) |
| Plain meaning | At every proper (local) context, the structure can internally talk about whether questions are resolvable. And this internal talk is faithful — it doesn't hallucinate answers. |
| SE analogy | Reflection/introspection API. The system can inspect its own query-resolution mechanism from within, and the inspection is accurate. |
| GUAF intuition | The "Aware" (A) property. Self-reference without collapse. |
9. The GUAF Class Itself
class GUAF (Ctx : Type u) [Site Ctx] (F : Presheaf Ctx) where
emptyGlobal : F.F Site.top ≃ PEmpty
properFull : ∀ U, Proper U → Nonempty (F.F U)
ladder : Ladder F
noFixedPt : ∀ q, ladder.mu q ≠ q
productive : Productive F ladder
representable : Representable F
notSheaf : ¬ DeltaCollapsible F
| Aspect | Decoding |
|---|---|
| Plain meaning | A GUAF is a presheaf where: (1) the top is empty, (2) every local view has content, (3) there's a ladder, (4) the ladder never loops back on itself, (5) the ladder never reaches a global answer, (6) the structure can introspect faithfully, (7) the structure cannot be collapsed to a single axis. |
The Notation Rosetta Stone
Keep this table as a reference when reading any mathematical text:
| Symbol | Name | Role | Plain English | SE Equivalent |
|---|---|---|---|---|
∀ x, P x |
Universal quantifier | Constraint | "For every x, P holds" | Array.every(x => P(x)) |
∃ x, P x |
Existential quantifier | Noun/Claim | "There is at least one x where P holds" | Array.some(x => P(x)) |
→ |
Arrow / Implication | Verb | "Maps to" (functions) or "Implies" (logic) | => (lambda) or if...then |
¬ |
Negation | Verb | "Not" | ! |
≃ |
Equivalence / Isomorphism | Constraint | "Structurally identical to" | Deep equality / isomorphic mapping |
⊥ or PEmpty |
Bottom / Empty | Noun | "The empty type" (no inhabitants) | never in TypeScript, uninhabited enum |
:= |
Definition binding | Verb | "Is defined as" | = in const declaration |
: |
Type ascription | Constraint | "Has type" | : in TypeScript/Rust |
{...} |
Structure/Record | Noun | "A bundle of fields" | struct, interface, type {} |
^[n] |
Iteration | Verb | "Applied n times" | f(f(...f(x))) loop |
≤, < |
Order relations | Constraint | "Less specific than", "Strictly inside" | Subtype relation, path prefix |
How We Build the Mental Model Together
Protocol for Every New Concept
When we encounter new math (in Phase A witness design, or while closing T2/T4):
- I decompose: I will present the concept using the Noun/Verb/Constraint table above before showing the formal definition.
- You verify: You tell me which row doesn't click. Is the noun unclear? Is the verb unmappable to something you know? Is the constraint too abstract?
- We ground: I provide a concrete software engineering analogy. You stress-test it — "does this analogy break down here?"
- We formalize: Only after steps 1-3 do we write the Lean code.
Why This Works for Your Specific Background
Your fragments of Calculus and Linear Algebra lacked this scaffold because those courses typically teach operations (differentiate, multiply matrices) without first establishing the structural roles (what kind of object is a derivative? Answer: a linear map — a verb between vector spaces).
By classifying every symbol as Noun, Verb, or Constraint before attempting computation, you bypass the need for fluent algebraic manipulation. You don't need to compute the integral; you need to recognize that integration is a verb (Q2) that inverts differentiation (Q2) and preserves area (Q5).
The Stable Base
The Five Questions scaffold + the Noun/Verb/Constraint decoder gives you a fixed coordinate system. When you encounter a new paper, a new Lean error, or a new mathematical claim:
- Find the nouns (what objects exist?)
- Find the verbs (what maps/operations connect them?)
- Find the constraints (what axioms bind them?)
- Ask what maps preserve between structures
- Ask what is lost in translation
This is not a simplification of mathematics. It is the actual methodology mathematicians use to orient themselves in unfamiliar territory. We are just making the implicit explicit.