lean

V15 public formal index

V15 is the Cross-Calculus Atlas for selected, receipt-indexed correspondences among three independently defined source domains. It is public under explicit integration and qualification targets. It does not change a v14 stable root or make PJ the owner of a source calculus.

For a plain technical introduction, terminology bridge, and worked example, start with the governed-computation orientation.

Primary formal surfaces

Surface Public role in v15
Governed Transport (GT) Existing public source calculus. PJ maps four edge shapes while retaining native route witnesses and endpoint bindings.
Execution Custody Existing public source calculus. PJ maps eight same-stage native constructor edges and keeps every additional premise explicit.
Continuity.Admission Identity-bound continuity admission on the reachable fragment. PJ maps three preservation edges using native reachability receipts. The private excavation name was Someone.lean.
StaticRole Held-out partial instance over the R0–R3 structural role hierarchy, closed at R3. Its functional-dependence theory remains local.
PJ Minimal indexed-judgment and receipt substrate used to record the selected mappings; not a shared native semantics.
Inquiry Frozen independent Track A calculus; comparison-only neighbor outside the PJ primary surface.
Preparation Frozen independent Track A calculus; comparison-only neighbor outside the PJ primary surface.

Canonical roots build under V15Integration. Seven direct qualification leaves and five declaration-audit roots remain isolated under V15IntegrationQualification so campaign checks do not enter stable import graphs.

Exact mapping scope

Governed Transport

The adapter maps positive translation, positive target-local reliance, negative translation, and negative target-local reliance as four distinct PJ bridges. A translation receipt contains the native Span.Witness plus equality bindings for both endpoints. A reliance receipt binds the same target.

This is not a reduction of governed transport to a morphism. The native Span is deliberately only crossing geometry. Certificate-dependent lift, artifact translation, and target-local reliance are different laws, while authority, custody, spend, obligation, and runtime correspondence are absent unless another exact calculus supplies them.

The carry functions are total given source evidence and those receipts. The adapter does not assert that every source has a route; does not combine translation and reliance; and does not import GT coverage, residue, composition, federation, or runtime-correspondence laws into PJ.

Execution Custody

The adapter maps the eight native edges from ticket freshness through attempt, commit, outcome, safety, and discharge. Source and target indices are the complete same ExecutionStage. Receipts retain local preconditions, ticket consumption and send evidence, the exact succeeded/refused/unknown outcome, safety evidence, or the obligation receipt as required by the native constructor.

There is no direct synthetic MayCommit → DidExecute bridge. A refused result and an unknown result remain different judgments. Safety does not supply discharge.

Continuity Admission

The adapter maps native reachability preservation for WellFormed, Coherent, and OwnsPacket. Each receipt is the native Reachable source target proposition. Identity and composition of receipts remain local Continuity laws because the other source calculi do not force a generic PJ composition law.

The mapping is restricted to the reachable fragment. It preserves an asserted AgentId; it does not authenticate identity or establish durable revocation, substrate rebinding, retained route history, typed refusal, obligations, or operational Continuity correspondence.

StaticRole

Downward R1→R0, R2→R1, and R3→R2 projections and evidence-bearing upward R0→R1, R1→R2, and R2→R3 bridges fit PJ. The upward receipts retain the native additional structure rather than storing their conclusions. StaticRole’s evaluator, de-se erasure, presentation, factorization, dependence, and correctness-independence laws remain local. No R4 exists.

Anti-minting boundary

exact_receipt_prevents_target_minting concerns one bridge and one source / target index pair. If source evidence and target evidence both exist but exact entitlement is refuted, no ReceiptFreeMintAt function taking only those two values can produce the missing source-relative EntitledFrom. Positive collapse controls show why the exact receipt fiber, indices, and consumer discipline are load-bearing.

The theorem is non-definitional and source-relative. It is not a generic qualification rule for arbitrary PJ bridge values, a global authority law, or a cryptographic unforgeability theorem. In particular, it does not by itself prohibit minting standing, custody, spend, discharge, closure, historical identity, or origin-bound support in calculi whose types are not its conclusion.

Exact failures and final classification

These are negative scientific results, not unimplemented features. PJ is not a shared bridge algebra or a universal calculus. No equivalence among the source calculi, arbitrary round trip, generic composition, runtime conformance, JCP implementation, or operational AG/NQ realization is claimed.

This site is open source. Improve this page.