Features / Where content may go

Proved in Lean 4Working today

One rule decides where every copy may go.

Folders, windows, the clipboard, the printer and each kind of AI all ask the same proven decision. A file's content can move up a level, never down, and every place has a ceiling it can never exceed.

1 rule

for every place a copy of a file's content can reach

Up, never down

content of a level reaches only that level or higher

L5

never printed, and kept to L5 places

How it works

Ask, decide, record

1

Ask

Save As, paste, the clipboard, print and sending to an AI all ask before they act. The apps, the browser and the key agent's clipboard use the same question.

2

Decide

The answer comes from one program built from the Lean proofs. If it cannot answer, the answer is no.

  • The same rule everywhere
  • No app has its own exception
3

Record

Every copy and every refusal goes into the ledger with its level, so a leak names whose copy it was.

  • Printed pages carry the level, the file, the person and the time

Ceilings

The highest level each place may hold

The system clipboardL2
An AI outside the governmentL2
The government's own AIL3
The printer (policy default: L3)L4
The ministry's own AIL5
Folders and windowsTheir own level

L3 and above never reach the system clipboard or an AI outside the government. L4 and above reach no AI but the ministry's own.

Proven, and what is not

Six theorems about where content goes

Proved in Lean 4

Checked on every build

  • Content of a level reaches only folders and windows of that level or higher
  • No place ever holds more than its ceiling, whatever the configuration says
  • L3 and above never reach the system clipboard or an AI outside the government
  • L5 is never printed
  • Moving a copy hop by hop never lowers its level
Trusted, not proved

Tested and listed openly

  • For AI, the packet filter goes by the highest level opened on the PC, and covers only the AI services ZENOS has been told about
  • Programs outside the ZENOS apps
  • A camera pointed at the screen

Try it in the preview

Try it yourself

1

Open an L4 sheet

From the Red folder, with clearance or an approval.

2

Try to copy it out

Ctrl+C leaves the clipboard unchanged. Paste into another L4 window works.

3

Try to print it

Above the policy line, printing is refused and recorded.