My Name Is SiMON

FSL, a governed symbolic language for making autonomous-agent claims inspectable, has released version 1.1.8 of its public package, which includes 32 theorem records with 31 machine-checked by Lean 4 and one under explicit axioms. The package provides a formal evidence bundle for reviewing mathematical claims about bounded observers in spatial/temporal systems, aiming to replace vague agent assertions with stable, named, reviewable objects.

FSL is a governed symbolic language for making autonomous-agent claims inspectable. This repository is the public package for FSL and the governed bounded observer theorem stack. It explains a model of agents as bounded observers in a spatial/temporal system, publishes theorem and proof-status evidence, and provides machine-readable language exports that external tools can inspect. Current public package version: 1.1.8 This package should be read first as a formal evidence bundle, then as a symbolic language/adoption package. Start here if you are reviewing the mathematical and evidence claims: formal whitepaper.md states the theorem-by-theorem proof-status boundary. THEOREM REGISTRY.md and theorem registry.json identify the 32 public theorem records. lean coverage report.md and lean coverage.json report 31 machine-checked theorem records and 1 machine-checked-under-axioms record. ASSUMPTIONS APPENDIX.md and CRYPTO AXIOM BOUNDARY.md explain the declared axioms and the named cryptographic binding assumption. REPLAY MATRIX.md , replay matrix.json , and scripts/replay fsl claim.py show how a reviewer can replay one public theorem claim. theorem lifecycle.json records public lifecycle status; it is evidence of theorem-record publication state, not a substitute for Lean proof. CHECKSUMS.sha256 verifies that the exported package artifacts have not drifted. Only after that formal evidence path should a reader move to the broader FSL language, role-governance, Rust parity, semantic file object, repository-ingestion, and validated-event-kernel material. Those layers explain adoption and runtime context; they do not strengthen theorem proof status. | Evidence surface | Current public status | |---|---| | Theorem records | 32 public records | | Lean proof status | 31 machine-checked, 1 machine-checked under explicit axioms | | Open proof holes | 0 scanned code-level sorry / admit holes | | Declared axioms | 132 public assumptions/model primitives | | Central result | gbo v underdetermination and anchor nonuniqueness exists | | Cryptographic boundary | gbo vi non equivocating under a named binding assumption | | Lifecycle status | 32 active public theorem lifecycle records | | Replay layer | Per-claim replay through scripts/replay fsl claim.py | | Runtime event layer | Typed, UI-agnostic event evidence; not governance authority | | Runtime authority | Rust remains narrowly scoped; broad governance authority is not promoted | AI agents often describe actions with broad words like "safe", "approved", "verified", "allowed", or "in scope." Those words are useful in conversation, but too blurry for review. For example: I made the deployment change and it is verified. That can hide many different questions: - Was the agent allowed to touch those files? - Did it stay inside scope? - Was anything formally proved? - Was the proof checked by Lean 4, or checked under assumptions? - Was the result only tested by runtime parity? - Did the release artifact drift after export? - Can another reviewer replay the claim without trusting the author's summary? FSL separates those claims into stable, named, reviewable objects. This package connects five layers: php HTM manifold - governed bounded observer - Lean theorem evidence - SiMON governance/runtime evidence - FSL semantic references The spatial substrate is an HTM, or Hierarchical Triangular Mesh, surface. In plain terms, the system divides a spherical surface into addressable cells. Cells can have neighbors, parents, children, and movement relations. This gives the model a way to talk about where an observer is, what local region it can inspect, and how it can move without pretending it sees everything. An agent acts from somewhere. It does not have global vision. A governed bounded observer is an agent modeled with limits. It has: - identity; - position or local state; - visible neighborhood; - movement rule; - time/history constraint; - governance boundary; - record of what claims it is allowed to make. The observer model asks: - What can this agent see? - Where may it move? - What history must it preserve? - What scope is it allowed to act inside? - What claims can be supported by evidence? Lean 4 is a proof checker. A theorem is a precise claim that a proof checker can verify from definitions and allowed assumptions. Instead of only saying: The observer preserves valid history. this package gives the claim a theorem record, stable theorem ID, Lean declaration when available, proof status, assumption boundary, lifecycle status, and release checksums. This package includes: - 32 public theorem records; - 31 machine-checked theorem records; - 1 machine-checked-under-axioms record; - 0 partial records; - 0 definition-only records; - 0 planned records; - 132 declared Lean axioms; - 0 code-level sorry or admit proof holes; - 32 active theorem lifecycle records. The one axiom-dependent theorem is gbo vi non equivocating . Its boundary is documented in CRYPTO AXIOM BOUNDARY.md . The strongest public-facing result is the underdetermination family: gbo v underdetermination anchor nonuniqueness exists These theorems capture the core bounded-observer point: a local observer can have evidence that is consistent with more than one possible world state or semantic anchor. In plain English, the system does not merely say "the agent is bounded." It proves that bounded evidence can leave genuine ambiguity. The package separates theorem evidence into different classes: | Class | Meaning | Example | |---|---|---| | Structural Lean theorem | A checked statement about the model's structure, motion, cost, horizon, or ambiguity. | gbo v underdetermination | | Model-definition consequence | A checked consequence that follows closely from the definitions and is useful as a sanity check. | decomposition and preservation lemmas | | Cryptographic-assumption theorem | A checked theorem that depends on an explicit external cryptographic binding assumption. | gbo vi non equivocating | | Runtime/evidence lifecycle claim | Evidence that a claim was exported, attested, replayable, or checksummed. | lifecycle records, replay matrix, checksum manifest | Those classes should not be collapsed into one vague claim of "verified." A Lean theorem, an axiom-dependent theorem, a lifecycle attestation, a Rust parity check, and a checksum are different kinds of evidence. FSL uses step-admissibility for local observer, file, and governance-transition claims. A step-admissible transition is acceptable for the current bounded step. That is not the same as whole-trajectory admissibility. The current package does not claim to prove that an agent's entire future path remains globally viable, that cumulative burden is exhausted or preserved across all future actions, or that Rust owns those decisions. An axiom is an explicit assumption or model primitive that the proof checker is allowed to use. That is different from an unfinished proof. | Term | Plain meaning | In this package | |---|---|---| | Theorem | A claim checked by the proof system. | A stable theorem record with proof status and evidence links. | | Axiom | An explicit assumption or model boundary. | Publicly inventoried in ASSUMPTIONS APPENDIX.md and lean assumptions.json . | | Proof hole | An unfinished proof placeholder such as sorry or admit . | Count is 0 for scanned code-level Lean proof holes. | The 132 declared axioms are not 132 hidden failed proofs. They are the visible assumption inventory across scanned Lean files, including governance model bridge files. The SHA-256-related boundary is intentionally narrow: this package treats cryptographic binding as a named assumption for the commitment theorem. It does not claim that Lean proves SHA-256 collision resistance. SiMON is the governed runtime and research system from which this public package was exported. The full private/runtime system contains mission lifecycle records, governance execution, StateProof chain material, runtime code, and broader experimental surfaces. This repository is not the full runtime. It is the public evidence and language package. That separation is intentional. A reader should be able to inspect theorem records, proof boundaries, FSL exports, replay artifacts, and checksums without access to the private SiMON repository. The validated event kernel is the runtime-facing event model around FSL. It treats interface input, role outputs, FSL references, theorem references, traversal evidence, FileInspector context, Builder-readiness signals, Governor decisions, release evidence, and StateProof candidates as typed events. Those events can be replayed and inspected without pretending that a UI panel, chat message, Rust preflight, or StateProof candidate is governance authority. The intended path is: php any interface - typed runtime event - shape and authority-boundary checks - FSL/theorem/evidence references - Python/governance interpretation - optional StateProof candidate - Governor boundary before durable consequence The old SiMON chat UI is not the target runtime architecture. It is only a source of useful interaction concepts such as prompt intake, governance status visibility, FSL references, role-pipeline visibility, and replay visibility. The public runtime model is UI-agnostic: chat, CLI, API, repository ingestion, or future visual manifold tools can submit typed events without inheriting old chat-local authority. For the dedicated public explainer, see VALIDATED EVENT KERNEL.md . Important boundary: typed runtime event = governance authorization validated event trace = StateProof append Rust preflight pass = proof or permission UI visibility = authority SiMON's reference governance system uses roles to keep action, inspection, authorization, and evidence separate. In public terms: | Role | Public meaning | FSL-facing claim | |---|---|---| | Research Agent | Investigates current state and evidence before action. | What is known, unknown, or queryable. | | Scope Agent | Bounds the proposed work before implementation. | Which files, packages, and deltas are in scope. | | File Inspector | Reads allowed files without changing them. | What the authorized scope actually contains. | | Builder | Performs the scoped implementation. | What changed inside the allowed boundary. | | Governor | Authorizes or rejects durable governance transitions. | Which transition is allowed to become governance evidence. | | Commander | Owns mission-level authority in the reference system. | Which mission-level action may proceed. | FSL does not replace these roles. FSL gives stable names to the claims those roles produce. A scope boundary can be referenced as a declared scope. A builder delta can be referenced as a symbolic change. A Governor decision can be referenced as an authorization boundary. A StateProof can be referenced as a durable evidence class. Rust is being developed as a kernel/runtime hardening layer for selected governance checks. In this release, Rust is not the governance authority. Rust has one active narrow preflight boundary: it may reject malformed serialized FSL semantic records before Python/query-surface authority evaluates surviving records. Rust also mirrors selected StateProof candidate, append-gate, file-semantics, repository semantic, and role-bridge validation boundaries as shadow parity, helping detect malformed serialized records, policy drift, scope mismatch, and authority-escalation attempts. The intended long-term value of a Rust kernel is type-safe enforcement at carefully promoted boundaries. Promotion requires explicit evidence, compatibility checks, rollback rules, and a governed authority decision. Role-bridge malformed-packet rejection is currently decision-scoped for future promotion only; it is not active runtime authority. Until a boundary is explicitly promoted, Rust remains evidence-bearing validation, not constitutional authority. The current FSL runtime also models repository files as semantic objects. That means a file is not only treated as bytes on disk. It can be described by: - repository path; - file kind; - semantic role; - language or format; - allowed operation class; - RFC 2119-style constraints; - expected scope relationship; - dependency and invariant context; - advisory step-admissibility status; - public constraint catalog reference. This layer helps bridge ordinary repository work to FSL meaning. A markdown paper, a Lean theorem file, a Rust runtime module, a checksum file, and a public export manifest do not carry the same governance meaning. They have different roles, different risks, different allowed operations, and different evidence boundaries. In the reference SiMON runtime, ScopeAgent can express what kinds of files are expected, FileInspector can attach read-only context to allowed files, and the advisory file step-admissibility layer can classify a proposed file action as eligible, rejected, requiring Governor review, or not applicable. Important boundary: semantic file classification is not enforcement authority advisory step-admissibility is not Builder rejection authority Rust file-semantics parity is not governance authority The practical value is that a governed agent can reason about files with more precision than "this path is allowed." It can distinguish the meaning of the file, the constraints attached to that kind of file, and the evidence needed before a change should proceed. The public catalog for those constraints is included as FILE CONSTRAINT CATALOG.md and file constraint catalog.json . It turns stable constraint references into readable RFC 2119-style statements without granting enforcement authority. The repository semantic ingestion layer extends file semantics from one file at a time to a whole repository snapshot. The bridge is staged: php repository files - file inventory - path and content classification - repository profile override - semantic file object - constraint resolution - dependency and invariant context - advisory step-admissibility - HTM semantic placement - bounded observer traversal - optional StateProof candidate - optional Rust shadow parity The point is not only to know that a path exists. The point is to know what kind of meaning the file carries in the governed system. A public README, a release note, a Lean proof snapshot, a Rust runtime module, and a checksum manifest should not be treated as interchangeable files. In this model, each file can become a semantic object. That object can then be placed into the HTM/FSL manifold as a semantic-layer occupant. A bounded observer can traverse the resulting semantic map, and FileInspector can attach read-only context about visible files, constraints, dependencies, and ambiguity sources. Important boundary: semantic ingestion is not permission to edit HTM placement is not observer movement bounded traversal is not durable proof StateProof candidate is not StateProof append Rust repository semantic parity is not governance authority For the dedicated public explainer, see REPO SEMANTIC INGESTION.md . FSL is the semantic language layer connecting these pieces. It gives stable names to claims that would otherwise remain loose prose. A mission, theorem, proof status, assumption boundary, runtime boundary, release artifact, and external software identifier can all be connected through shared symbolic references. | Ordinary context | Project artifact | FSL / theorem reference | Meaning | |---|---|---|---| | Work request | mission or update packet | mission open , declared scope | A bounded mission exists and declares what may change. | | Changed files | commit or file delta | Δ FSL , ⊕ sync | Symbolic/export state changed and synchronized. | | Allowed scope | allowed packages | declared scope | The agent may act only inside the declared boundary. | | Agent identity | DID and StateProof identity | DID , identity , StateProof | Observer identity is tracked across history. | | Spatial position | HTM cell or observer location | space.htm surface , adjacent | The observer acts from a location on the manifold. | | Movement rule | movement/history packet | valid spatial motion , valid motion stay | Motion obeys the HTM neighbor/bounded-motion rule. | | History rule | trace or tick sequence | valid history preserved , tick | Valid history persists across a step-admissible motion. | | Observer bound | local view or horizon | gbo iii spatial horizon , bounded | The observer has a bounded spatial horizon. | | Temporal bound | tick/time horizon | gbo iii temporal horizon , time | The observer has a bounded temporal horizon. | | Formal proof reference | Lean declaration | gbo vi non equivocating | The theorem is checked under explicit cryptographic assumptions. | | Release integrity | checksum file | CHECKSUMS.sha256 | Package files can be checked for byte-level drift. | The point of FSL is not decorative notation. It is durable meaning that humans and tools can review. Recent hardening work added a governed path from semantic observation to durable evidence. The internal pipeline is: php observable semantics - StateProof anchor candidate - anchor decision - append request - dry-run StateProof payload - Governor authorization - controlled append integration - Rust shadow parity Important boundary: Candidate evidence is not StateProof evidence. Dry-run payload is not StateProof append. Governor authorization is not direct append execution. Rust parity is not governance authority. The canonical StateProof append entrypoint remains: governance.identity.state proof.generate state proof Rust currently mirrors candidate and append-gate validation as shadow parity only. It can help detect malformed records and authority escalation attempts, but it is not promoted to authority for StateProof decisions. Rust also mirrors file semantic classification and advisory step-admissibility status as shadow parity. That check can classify a path into a file kind and semantic role, compare expected scope metadata, inspect supplied constraint-evaluation summaries, and report whether the serialized record looks eligible, rejected, or requiring Governor review. It still cannot reject the Builder, expand scope, authorize governance, append StateProof, or promote Rust authority. Rust also mirrors repository semantic records as shadow parity. That check can validate supplied semantic object, placement, and advisory-status summaries for drift or authority escalation. It still does not scan repositories by itself, own FileInspector context, reject Builder actions, expand scope, authorize governance, append StateProof, or promote Rust authority. Rust also mirrors role-bridge packets as shadow parity. That check covers serialized ScopeAgent semantic regions, TourAgent traversal results, FileInspector context maps, Builder readiness packets, and Governor durable consequence decisions. It can reject malformed or authority-escalating serialized role-bridge packets in parity fixtures, but the future active gate for that surface has not been promoted. Rust still cannot authorize missions, move observers, own role outputs, override Governor, reject Builder work, expand scope, or append StateProof evidence. See: RUST PARITY NOTE.md RUST AUTHORITY CRITERIA.md docs/fsl rust authority promotion audit.md From the public package directory: python3.12 scripts/replay fsl claim.py gbo iii temporal horizon For an axiom-dependent example: python3.12 scripts/replay fsl claim.py gbo vi non equivocating To list available theorem IDs: python3.12 scripts/replay fsl claim.py --list The replay script is not a Lean prover and not a governance authority. It helps a reviewer traverse one public claim from theorem ID to evidence boundary. If a repository semantic map export is available, replay it with: python3.12 scripts/replay repo semantic map.py semantic map.json That command checks the exported semantic map for replay/placement drift. It does not scan a live repository, authorize edits, append StateProof evidence, or promote Rust authority. If you are new to this repository: - Read this README. - Read USE CASES.md for the governed production-change journey. - Read REPO SEMANTIC INGESTION.md to understand how repository files become semantic objects in the HTM/FSL manifold. - Read EVIDENCE CLASSES.md to understand evidence boundaries. - Replay one theorem claim with scripts/replay fsl claim.py . - Inspect THEOREM REGISTRY.md or theorem registry.json . - Read formal whitepaper.md for theorem-by-theorem proof status. - Map your own system names, such as tickets, commits, policies, CI jobs, deployment IDs, or audit records, to FSL-style semantic references. This package is: - a public, versioned release of the FSL language and observer theorem evidence bundle; - a formal proof-status package for 32 public theorem records; - a replayable evidence package with checksums; - a bridge between governed autonomous-agent action and inspectable semantic claims; - a public explanation of repository files as semantic objects placed into an HTM/FSL manifold; - a publication package containing human-readable and machine-readable artifacts. This package is not: - a full autonomous-agent runtime; - a production deployment framework; - a replacement for Lean; - a replacement for governance execution; - a runtime authority handoff to Rust; - a claim that generated exports are parser authority; - a claim that Rust can append StateProofs; - a claim that every governance axiom has been derived from first principles; - a claim that every real-world implementation detail is formally proved. - FSL symbols: 179 - FSL bundles: 15 - FSL tiers: A 94, B 70, C 8, D 7 - Glyph candidates: 25 - Glyph promotion state: 3 promotable now, 22 requiring alias plans - Observer kernel theorem records: 32 of 32 complete - Lean coverage snapshot: 31 checked theorem records, 1 axiom-dependent, 0 partial, 0 definition-only, 0 planned - Theorem lifecycle snapshot: 32 active records - Lean assumptions snapshot: 132 declared axioms, 0 code-level sorry / admit proof holes - FSL file-semantics layer: semantic classification and advisory step-admissibility only - FSL file constraint catalog: public vocabulary/evidence only - FSL repository semantic ingestion: semantic map/replay explanation only - Rust StateProof candidate parity: shadow only - Rust append-gate parity: shadow only - Rust file-semantics parity: shadow only - Rust repository semantic parity: shadow only - Rust role-bridge parity: shadow only - Rust semantic-record malformed rejection: active reject-only preflight - Rust role-bridge malformed rejection: decision-scoped only, not active - Broad Rust authority promotion: not granted For a compact overview: ABSTRACT.md For examples and conceptual walkthroughs: USE CASES.md REPO SEMANTIC INGESTION.md For evidence boundaries: EVIDENCE CLASSES.md INDEPENDENT REPLAY.md FILE CONSTRAINT CATALOG.md file constraint catalog.json REPLAY MATRIX.md replay matrix.json scripts/replay fsl claim.py scripts/replay repo semantic map.py For theorem and proof-status review: whitepaper.md formal whitepaper.md THEOREM REGISTRY.md theorem registry.json theorem lifecycle.json lean coverage report.md lean coverage.json ASSUMPTIONS APPENDIX.md lean assumptions.json FORMAL PROOF BUNDLE.md CRYPTO AXIOM BOUNDARY.md For FSL language review: fsl governed symbolic language.md fsl specification.md fsl registry.json fsl types.json fsl grammar.json fsl/SYSTEM.yaml FILE CONSTRAINT CATALOG.md file constraint catalog.json For release and runtime boundaries: RELEASE NOTES.md RELEASE POLICY.md RELEASE CANDIDATE AUDIT.md PUBLICATION TAG.md STATEPROOF NOTE.md RUST PARITY NOTE.md RUST AUTHORITY CRITERIA.md docs/fsl rust authority promotion audit.md PUBLIC REPO NOTES.md For PDF presentation: OVERLEAF README.md overleaf/main.tex overleaf/references.bib README.md : public landing page and orientation map ABSTRACT.md : compact overview for first-time readers USE CASES.md : practical adoption scenarios and governed autonomous-agent example REPO SEMANTIC INGESTION.md : public explainer for repository semantic objects, HTM placement, bounded traversal, StateProof candidates, and Rust shadow parity EVIDENCE CLASSES.md : distinctions between proof, attestation, export, parity, authorization, checksum, and StateProof evidence FILE CONSTRAINT CATALOG.md : human-readable RFC 2119-style file constraint catalog file constraint catalog.json : machine-readable file constraint catalog INDEPENDENT REPLAY.md : reviewer playbook for traversing theorem claims to evidence scripts/replay fsl claim.py : one-theorem public replay command scripts/replay repo semantic map.py : semantic-map replay command for exported repository semantic maps REPLAY MATRIX.md : human-readable theorem-by-theorem replay index replay matrix.json : machine-readable theorem-by-theorem replay index whitepaper.md : governed bounded observer theorem position paper formal whitepaper.md : formal proof-status whitepaper OVERLEAF README.md : Overleaf upload and compile instructions overleaf/ : PDF-ready LaTeX paper source STATEPROOF NOTE.md : public explanation of raw-chain status and repaired canonical verification RUST PARITY NOTE.md : public explanation of Rust/Python parity status and current authority boundary RUST AUTHORITY CRITERIA.md : public criteria for future Rust governance-authority promotion docs/fsl rust authority promotion audit.md : report-only audit explaining why Rust remains shadow parity THEOREM REGISTRY.md : human-readable observer theorem registry theorem registry.json : machine-readable observer theorem registry theorem lifecycle.json : machine-readable public theorem lifecycle export lean coverage report.md : human-readable Lean coverage audit lean coverage.json : machine-readable Lean coverage audit ASSUMPTIONS APPENDIX.md : human-readable no-sorry/no-axiom audit lean assumptions.json : machine-readable Lean assumption inventory FORMAL PROOF BUNDLE.md : guide to the public formal proof bundle lean/ : public Lean source snapshots used by coverage and assumptions audits CRYPTO AXIOM BOUNDARY.md : public assumption boundary for the axiom-dependent commitment theorem FORMAL COVERAGE BASELINE.md : formal-whitepaper-track proof-status baseline fsl governed symbolic language.md : FSL language paper fsl specification.md : human-readable FSL specification fsl registry.json : machine-readable symbol registry fsl types.json : machine-readable type, sort, and category export fsl grammar.json : machine-readable grammar and rendering export fsl/SYSTEM.yaml : canonical FSL source snapshot MANIFEST.md : include/reference/exclude manifest PACKAGE MAP.md : layer map connecting papers, exports, and provenance RELEASE NOTES.md : release contents and verification notes RELEASE POLICY.md : versioning, compatibility, and publication policy RELEASE CANDIDATE AUDIT.md : claim-safety and public-boundary audit ERRATA.md : horizon correction and spatial-horizon resolution HORIZON RECONCILIATION.md : governed reconciliation note for the horizon lifecycle gap PUBLICATION TAG.md : governed release-freeze and tag-ready record VERSION : current public package version EXPORT MANIFEST.json : allowlisted source map for rebuilding this package from the SiMON source tree PUBLIC REPO NOTES.md : public repository boundary and exclusions CHECKSUMS.sha256 : SHA-256 checksums for repository artifacts From the SiMON source tree, the public package can be refreshed with: python3.12 scripts/export public fsl package.py --check The exporter uses EXPORT MANIFEST.json , regenerates theorem registry exports, preserves repository metadata, refuses excluded private/runtime paths, copies the replay script, and rewrites CHECKSUMS.sha256 . From the public package directory, run: shasum -a 256 -c CHECKSUMS.sha256 Every listed file should return OK .