The finite layer-preservation theorem now has an executable graph adapter. It constructs exact surface operations in Lean and binds each graph transformation through Verifier Standard (VSTD). The supported claim is that the output is precisely the stated lift or ordered composition of its inputs, and that the retained ground-record checker accepts it.
This implements a finite graph connection toward the author's proposed verification geometry. It does not establish that the graph or the represented operations are generated by the native self-derivation kernel.
Install the verification extra and the repository's declared Lean toolchain.
Run from the Hypermath checkout:
from datetime import datetime, timezone
from hypermath_foundations.layer_graph import LayerGraph
construction = LayerGraph(".", timeout=60)
ground = construction.primitive("groundSelf")
difference = construction.primitive("diff", depth=0)
first = construction.lift(ground)
second = construction.lift(difference)
composed = construction.compose(first, second)
reused = construction.lift(composed)
evidence = construction.finalize(recorded_at=datetime.now(timezone.utc).isoformat())
Initialization runs the existing source audit and requires its execution, source policy, and input stability to pass. The strict self-derivation and arithmetic gates can remain unresolved: their truth is not a premise silently supplied to this construction. A dirty development checkout is identified by its exact source inventory and recorded dirty state. This is separate from the existing adapter's clean-commit audit replay.
primitive creates an instance of one of the four ground rules: groundSelf,
diff, sim, or box. The dimensionless depth selects a free ground term.
groundSelf has no term argument and requires zero depth. add_surface
accepts an externally supplied encoded surface and checks it through Lean.
compose requires two successor-layer surfaces at the same layer. lift
turns the entire input into an atom at the next layer. finalize freezes this
construction and returns local evidence; it performs no publication.
SurfaceBridge.lean imports and executes the
existing LayeredDerivation definitions. The Python adapter does not reimplement
the inference rules or surface checker. Its JavaScript Object Notation (JSON)
transport represents a surface by exactly three fields:
| Field | Meaning |
|---|---|
format |
Literal hypermath-surface-1 |
layer |
Dimensionless nonnegative integer selecting the decoding layer |
code |
The complete binary prefix string for the encoded surface tree |
A zero bit represents a leaf; a one bit precedes the left and right child codes. The existing parser consumes the entire code. The bridge checks the embedded layer and requires canonical re-encoding. The transport and runtime are explicit host dependencies; their integration tests are not a formal correctness proof of the whole JSON transport.
Every artifact binds the canonical payload's Secure Hash Algorithm 256-bit (SHA-256) digest, byte count, format, and layer. Each edge records the operation, ordered operand ports, exact output, and source coordinate. A repeated operand appears in both positions. The mechanism checks all these bindings, executes the operation again through Lean, and compares its complete output with the claimed output. The raw code retains grouping and lower derivation trees. Edges operate on whole surfaces; individual inference steps remain within the encoded records rather than becoming separate graph edges in this adapter.
LayerSupportMechanism implements the vstd.graph.support predicate for this
bounded domain. Verifier's AssuranceLedger.record_trust separately enforces
graph identity, admissible statuses, and current prerequisite support for every
derived input. Its input-set check and the mechanism's ordered-operand check
serve different purposes. One prerequisite supports a repeated input artifact,
while both operand positions must still appear in the domain transformation.
At finalization, genesis surfaces are checked again, including unused roots.
Each derived edge earns support in construction order. The serialized assurance
log embeds its evidence and can be replayed with recheck_assurance_log and the
same source-bound mechanism. Replay reruns the Lean edge operations and checks
the resulting ledger against the serialized one. It does not promote the log
to a new VSTD conformance level or to an arithmetic proof.
The implementation bounds each code at 8,191 bits, the representation layer at 16, primitive term depth at 32, the graph at 64 nodes and 64 edges, a transport request at 65,536 bytes, and graph evidence at 2,097,152 bytes. These are resource limits, not mathematical restrictions on the finite preservation theorem. Every Lean process has an explicit timeout, 60 seconds by default.
Malformed codes, rejected records, mismatched output, reversed operands, and
lost repetition are negative checking results. Resource limits, unavailable
Lean execution, or changed source inputs produce SurfaceUnavailable and an
UNKNOWN mechanism outcome. They are not evidence that the represented
mathematical proposition is false. Accepted graph results still report native
self-derivation, source adequacy, ordinal interpretation, and arithmetic
completeness as UNKNOWN.
python -u scripts/check_layer_graph.py --output build/layer-graph --timeout 60
python -m pytest tests/test_layer_graph.py -vv -s --durations=10 --timeout=60
The first command uses the actual Lean toolchain and released Verifier 1.3.0 objects. It constructs seven surfaces, earns and replays five support events, and attempts five adversarial cases. The order and repetition cases rebind both the altered graph and its evidence digests while preserving the input set. They therefore exercise the operation check rather than just stale-hash detection. The remaining cases are an invalid projection, a wrong layer, and trailing code. The output includes the source audit, graph and assurance log, negative evidence, and a digest summary.
The Python tests use explicitly synthetic surface execution to isolate graph binding and failure propagation. They exercise the real Verifier ledger but are not Lean proof evidence. Continuous integration runs the real executable graph check in the native audit-integrity job and retains its artifacts; the strict mathematical job keeps its separate completion requirements.
The next mathematical connection is native realization of the constructors, checking transitions, and verification geometry. Internal acceptance, ordinal interpretation, limit stages, arithmetic-truth coverage, and novelty remain separate obligations. A graph that preserves this finite checking evidence does not yet generate new logical structures or establish the intended "formally closed-like" arithmetic.