Skip to content

v12.0.0 — Judgment Orientation

Choose a tag to compare

View all tags
@unpingable unpingable released this 16 Jul 22:34
· 66 commits to main since this release
v12.0.0
b528af8

v12.0.0 — Judgment Orientation

Raw custody is a sequence; effective exact-origin contribution is its finite-support join-semilattice projection.

v12 introduces LeanProofs.JudgmentOrientation, a stable, Mathlib-free sibling theorem family beside admissibility, witnessing, authority, and view semantics.

The release separates inquiry posture from protected judgment state, localizes visible protected changes to privileged transition points, preserves ordered raw provenance while counting exact-origin contribution idempotently, and connects those results through a deliberately one-way bridge.

What v12 proves

The stable five-module public root establishes:

  • Orientation is not authority. Pure orientation may change inquiry posture, but it cannot write certification, probe authority, or action authority. Governed application requires separate admission evidence.
  • Protected changes localize to privileged steps. When an orientation-invariant protected observation differs between the endpoints of a mixed trace, some privileged step occurred along that trace. Localization identifies a change point; it does not justify the transition or detect changes later reverted.
  • Replay remains visible without double-counting contribution. Raw custody remains an ordered sequence of occurrences, while exact-origin accounting counts one caller-supplied origin once.
  • Effective origin support forms a finite join-semilattice. The public API provides bottom, join, membership, inclusion, partial-order and least-upper-bound laws, support cardinality, append-as-join, and streaming/batch projection agreement.
  • Visible protected change implies supported privileged provenance. Across an attributed mixed trace, an endpoint-visible difference in an orientation-invariant protected observation names a privileged step whose caller-supplied origin appears in the effective support of the trace’s privileged provenance.

Attribution is structural: a privileged step enters an attributed trace together with its Occurrence. The theorem therefore does not fabricate origin evidence after the fact.

The converse is false. Supported privileged provenance does not imply that a protected endpoint changed; the no-op witness remains in the examples annex.

Public surface

Import the stable family with:

import LeanProofs.JudgmentOrientation

Its exact public modules are:

LeanProofs.JudgmentOrientation.Core
LeanProofs.JudgmentOrientation.Attribution
LeanProofs.JudgmentOrientation.Provenance
LeanProofs.JudgmentOrientation.OriginSupport
LeanProofs.JudgmentOrientation.Bridge

Build the stable surface with:

lake build JudgmentOrientation

The Streetlamp, source-blind laundering, relay, accumulator, payload-conflict, bridge, non-vacuity, and non-converse fixtures remain ANNEX evidence under LeanProofs.JudgmentOrientation.Examples and are excluded from the stable root:

lake build JudgmentOrientationExamples

EffectiveSupport deliberately keeps its representation private. The compatibility promise is its algebraic operations and laws, not a frozen quotient carrier.

Boundaries

v12 does not prove:

  • authentication or trusted issuance of origins;
  • Sybil resistance or common-cause independence;
  • payload fidelity without an additional witness;
  • linear, one-shot, expiring, or revocable MayOrient evidence;
  • admissibility, safety, approval, or justification of privileged transitions;
  • the converse from supported provenance to visible protected change; or
  • runtime or deployment conformance.

The release also leaves LeanProofs/Scratch/BreakGlassAuthorization.lean in SCRATCH: compiling, tracked, Mathlib-free, unwired, and outside every v12 claim and promotion boundary.

Audit footprint

The Judgment Orientation family is regression-gated by:

bash scripts/check-judgment-orientation-footprint.sh

Its disclosed maximum footprint is exactly:

[propext, Classical.choice, Quot.sound]

Missing or renamed receipts, proof holes, sorryAx, or footprint drift fail closed.

The complete release tree also passed the full project build, Witnessed and Paid Recomposition gates, View Semantics gates, Mathlib isolation and pin checks, custody classification checks, native-decision and axiom audits, repository proof-hole scans, and metadata/version agreement checks.

v11 custody corrections

v12 records two release-hygiene corrections without changing any theorem, definition, import, or capability:

  1. The unchanged eight-module v11 paid stable closure is now classified consistently as PUBLIC-SHIPPED, matching the already-public Payment dependency graph.
  2. The permitted direct Scratch dependency of Applications.FiniteSupportOneCrossing is enforced as the exact singleton LeanProofs.Scratch.FiniteSupportChecker.

The tagged v11 tree is not rewritten.

Release record

The v12.0.0 tag and GitHub release archive the verified tree. GitHub release publication drives the corresponding Zenodo version deposit beneath concept DOI 10.5281/zenodo.20369489.

The version-specific DOI is assigned by Zenodo and is intentionally not guessed or hard-coded into the source tree.

Publication changes no custody class, theorem, API, import boundary, or proof footprint—and, as ever, compiling the formalization does not prove that any runtime conforms to it.

Assets 2
Loading