[GTrunSec]

All applicable Cedar domains now use the shared Functional owners, actual typed Case inputs, Contracts, whole-result equality proofs and independent Rust replay. This removes eager Program-dependent import observations and shares ancestor preparation without changing original successes, refusal/error order, source binding or SDK admission.

Implementation

• Pinned LeanPoo 050b2b33b5cc993d2cf2ac7e7e862cdbd8377485: one lazy audited ancestor table; one graph-wide uniqueness check; original compiler fallback for unaudited/duplicate branches. Root retention requires the original graph/root equality witness. 42 original and 80 reversed/fallback controls pass; no new trusted axiom.
• 43 static Programs retain real provider/model/schema/root inputs behind the existing owner. Whole-Program equality preserves the original projection. The native catalog has 49 actual Program/Compilation inputs plus two static results; about 60 public exports consume that owner. 57 Program-dependent Bool globals become observations; 40 independent data/model globals remain.
• Schema-free Compilation retains preparation as an explicit field; generated C no longer recreates its thunk through eta expansion. All three schema-free families, paired Delta calls and TicketSharing share their actual owners. HostSafety keeps its necessary original Program index; disclosure fixtures prove equality to their original authorized transitions.
• Certified native encoding retains public JSON projections and canonical duplicate/key behavior. Semantic catalog containers are lazy; bounded rows use one official Lean JSON compression queue per object. Output stays fragmented. Encoding certificates do not pretend to prove Lean's parser implementation.
• Existing external observer records raw Darwin task counters and public executable UUID/path in its bounded thread. 32 observer tests pass; Linux does not invent Darwin fields. No new timeout, heap, concurrency or cache-version escape hatch.

Complete validation and measured limits

Measured code eaa334d49ad6b5d1d49d9250445400977af38a55; publication 8d4f85db7c4bdbcfd8edae15597169cf2da3f7e3 only updates the audit. All 705 measured source inputs match the full gate, timing run and publication.

• Final source-stable just check: passed, 424.347 s. Types, Contracts, proofs/axiom audits, all applicable business controls, Rust replay/admission, negative controls and workspace Clippy remain aligned. Earlier complete owner migration gate passed separately in 593.999 s.
• Final fixed ordinary cohort: 48 children, 15 complete byte comparisons passed; normal Rust bridge is byte-identical on both sides. Reference/candidate pipeline walls: 2565.767/1985.656, 285.936/280.005, 300.701/285.785 ms. Median CPU 260/250 ms, peak child RSS 49.953/48.172 MiB. No task-owned builds overlap ordinary measurements; all samples remain.
• Actual cold-image diagnostic: import initialization 46.996/18.623 ms, main 28.195/69.250 ms; source preparation remains more expensive. These separate epochs/instruments do not establish stable whole-process acceleration. Original-object Plan metadata is not yet transferred into later ancestor preparation; deferral alone moves work into main.
• Final allocator committed space 35.3/28.8 MiB, diagnostic sampled RSS 49.633/48.297 MiB; virtual reservation remains 1 GiB and purge count zero. These are observed reductions, not live-heap decomposition or memory bounds.
• Cedar empty-project cold build: 941 tasks, 110.386 s, all five native targets generated. The three ordinary hot/cold images match. Two stale hot diagnostic/policy executables failed strict identity and are retained as invalid provenance; current cold images pass the full-wire and policy checks. Earlier phase samples cannot be attributed to final source. Rust project-package clean rebuild: 12.421 s; exact bridge hash and full cold catalog/replay bytes match.
• POO public-library cold gate remains failed: fixed 120-second timeout at 420/422 tasks, max child RSS 1311.219 MiB. The generated cold C4 executable passes eight result groups separately. Hot/cold linker SDK commands differ; no reproducible-image or full cold acceptance claim.
• One owned Lean sample shows _dyld_start + 0 with stationary raw CPU/fault/page-in counters before main. Rust has no qualified entry frames in that fixed sample. Owned PID/kernel UUID/path are verified; exact OS callback and sample image UUID remain unavailable. No security/signing/xattr changes.

All three raw 48-child stages and failed preflights remain outside Git, including the first allocation-observation Rust mismatch. Final measurements use the existing standard benchmark recipe; counts and watchdogs are unchanged. Generated CSV/JSON are not committed.

Complete architecture, receipts and remaining common-owner work.

Exact revision CI

• POO 050b2b3: 17/17 successful jobs.
• Initial Cedar owner implementation 0c3e59b: 4/4 successful Ubuntu jobs.
• Final publication 8d4f85d: 4/4 successful Ubuntu jobs. Downloaded raw evidence verifies 13 resource receipts, 12/18/186 native measurement markers and 30 diagnostic invocations (24 full catalog/replay successes, six intended rejections). Observer shutdown, complete stderr offsets/output hashes and all three dependency configuration hashes pass; the tested merge tree equals the final publication tree and includes the exact head parent.

Keep this PR open and unmerged, with auto-merge disabled.

Functional Zero Trust and Authorization frameworks

• The application-independent ZeroTrust directory retains typed functional composition and actual LeanPoo Dataflow inheritance, Contract, factory and Session. The transitive import-boundary gate excludes Gateway. Authorization/Delta remains independently organized; Gateway consumes both frameworks.
• The POO audit found that a root-indexed proof preserves the root but does not automatically preserve extra ancestor requirements under raw overrides. The actual POO counterexample retains a root-only valid child that drops the stricter parent condition.
• composeSessions now retains the independently required parent Session and selected Session; Composed.requirement conjoins both actual projections. Gateway fromFrameworkObject requires both. The composition theorem preserves source-bound reads, parent requirements, the generic framework and the original Gateway Contract. Ongoing object composition separately reuses continuing/current-state/CommittedPrefix laws without reconsuming the root.
• Isolated official CVC5 1.4.2 arm64 qualification checked archive SHA-256 and loader metadata, then completed four existing recipe backends: authorization-delta, authorization-delta-operational, payment-delta and payment-interaction. Solver/assertion checks and official Rust Cedar replay passed fourteen ordinary cases. Gateway loss/gain/equivalence and stale-binding solver controls passed separately. The existing payment schema-bound producer/consumer and manifest-relative assertions passed for thirty-two separate validated receipts. These cohorts are finite evidence, not Lean UNSAT certificates or runtime publication admission.
• Full public SPEC and existing Tests aggregate passed (588 Lake jobs), including real generic POO Session reads, raw override and retained-parent counterexamples, continuing consumption laws and inherited axiom audits. The existing source-layer checker passed. No new axioms or sorry were introduced.
• RFC 0010 records NIST/UCON/Cedar research alignment, current source evidence and remaining Host obligations: authentic required-parent commitment, native ledger/IO refinement, external fact projection and deployed anti-rollback authority. Raw source-bound Session identity is not independent publication authority.
• Weaver now retains a native expected counterexample that typed/fenced publication can widen Allow without mandatory Delta review evidence. Its local final-callback test observes durable claim/reservation/consumption/burn/unknown range and excludes a second SQLite writer; actual streaming/restart remains separately qualified. Native review-artifact admission is not claimed as implemented.
• Dependency pins and historical evidence remain unchanged. Gateway proof-only review additionally binds authoritative context and durable recovered-artifact registration; no Rust Gateway execution implementation is inferred. The production transport and evidence changes are described above; this PR remains unmerged.