🛡️ The Gate — How A Claim Gets Proven

The technical heart. Two checkers turn "privacy is architectural" from a
slogan into a mechanical fact.

The problem the gate solves

Anyone can write English that sounds like a privacy guarantee. The question
is whether the guarantee is really in the structure of the text, or only in
the reader's imagination. The gate exists to answer that mechanically, in two
layers.

Layer one: the grammar checker (tools/lexon_check.mjs)

The first checker verifies that a text is valid Lexon in the attested subset,
in four stages:

1. Parse — every statement classifies and parses under the controlled
   grammar. Unknown words, unknown constructs, and malformed sentences are
   rejected.
2. Role binding — every noun is defined before use and bound immutably. A
   name that was never introduced, or redefined mid-document, fails.
3. Triple round-trip — every action sentence is turned into a
   subject-predicate-object triple, then re-serialized back into a sentence,
   then re-parsed. The triples must come out identical. This is the "grammar
   to graph" claim made mechanical: if the text and the graph are truly the
   same thing, the round-trip is lossless.
4. Promise typing — every obligation edge is typed (a may is a voluntary
   permission; a must or a recital act is a commitment) with a polarity,
   following promise theory.

Run node tools/lexon_check.mjs --selftest and it checks itself: known-good
example texts from lexon.org must pass, and deliberately broken "mutant"
versions must fail. If a mutant ever passes, the checker is broken and says
so.

This layer answers: is this valid, lossless, promise-typed Lexon? But it
does not answer the deeper question, and here is why that matters.

The hole the first layer cannot see

Early in the project the loop drew a held-out term — the "2D Fortress," a
cryptographic structure that falls to a quantum attacker. The prover expressed
it, and it passed the grammar gate perfectly. But it passed with the
adversary draining the protected secret — which is, in that specific case,
the canon-correct direction (the fortress is supposed to fall). The unsettling
discovery: the grammar gate would have equally accepted the opposite text,
where the defender keeps the secret. The two texts have the same clause shape.
The direction — the entire point of a privacy claim — lived only in a prose
Notes line the checker could not read.

That is the vulnerability at the core of "privacy is architecture." If the
gate cannot tell a guarantee from its opposite, it is not checking the
guarantee.

Layer two: the mutation probe (tools/relation_check.mjs)

The second checker closes that hole. Every folded expression now carries a
machine-readable relation claim — the structural guarantee it makes, in
one of four types:

• gate — a clause is reachable only under a stated condition.
• ordering — a clause performs its actions in exactly this sequence.
• conjunction — a defined term requires all of several conditions.
• absence — no clause routes a given thing to a given party. This is the
  important one: an impossibility, and therefore a privacy guarantee, is an
  absence. Direction is claimed as an absence: "the secret can never reach
  the defender's adversary" is a route that does not exist.

For each claim, the probe does something adversarial. It:

1. checks the claim actually holds on the text (as a property of the parsed
   clause graph, never a string search);
2. builds a mutated twin — the claim's minimal structural negation (strip
   the condition, reverse the order, drop a conjunct, or add the forbidden
   route);
3. confirms the twin still passes the grammar gate — proving the base gate
   alone cannot tell them apart;
4. confirms the claim now fails on the twin.

Only if all four hold does the claim earn RELATION PASS. In plain terms: a
guarantee is proven by showing the grammar can distinguish it from its own
opposite. The 2D Fortress now carries absence: Scalar Secret to Key Holder,
and the tool proves that adding a reclaim clause would break exactly that
claim. Direction lives in the structure, not the prose.

The canary: knowing the gate is passable

A gate no candidate can pass is as useless as a gate everything passes — you
cannot tell a bad candidate from an impossible test. So the mutation probe
ships with a canary: a small fixture authored together with its claims, which
passes the full pipeline by construction. node tools/relation_check.mjs --selftest runs it. If the canary ever fails, the gate itself is broken, not
the candidate.

What the gate deliberately does not do

Honesty is part of the design. The checker validates an attested subset of
Lexon derived from published examples — it is not the real Lexon compiler
(a macOS-only binary with unpublished source). So arithmetic is never
executed here: an expression carries a formula's structure (which quantities
gate which actions, what must precede what), not its computed values. The
entropy expression captures that residual uncertainty survives observation; it
does not compute Shannon's logarithm. Every entry names what it omits, and the
frontier.json gate string states the regime plainly.

This boundary is not a weakness to hide; it is the difference between "we
proved the structure" and "we ran the math," and the project never blurs it.

In one sentence

The grammar checker proves a text is lossless, promise-typed Lexon; the
mutation probe proves its privacy claim is really in the structure by showing
the grammar can tell it apart from its opposite — which is what it means for
privacy to be architectural rather than promised.

Assets

Navigation

← Welcome Visitors · The Grammar Workshop · The Results — Five Runs, 211 To 22

the wiki is a projection; github.com/mitchuski/lexon_pvm (git) is the source of truth · a Lexon x Privacy Value Model workshop, run through the The Harness — The Model Turned On Itself