# Marquee axiom receipt — serving-limits + State-Fabric + transport headline theorems
#
# Generated by scripts/gen_marquee_axioms.py. Every footprint must be
# subset of {propext, Quot.sound} (or 'no axioms'). No sorry / native_decide / custom axiom / mathlib.
# This is the shipped RECEIPT behind the data room's 'axiom-free' marquee claims.

## transport (theory/lean)
'Reorder.gap_states_lower_bound' depends on axioms: [Quot.sound, propext]
'ReorderTight.state_count_lower_bound' depends on axioms: [Quot.sound, propext]
'ReorderTight.pow_le_choose_window' depends on axioms: [Quot.sound, propext]
'ReorderTight.reorder_state_log_factor' depends on axioms: [Quot.sound, propext]
'ReorderSurface.ingress_wall_lower_bound' depends on axioms: [Quot.sound, propext]
'ReorderSurface.egress_wall_lower_bound' depends on axioms: [Quot.sound, propext]
'ReorderSurface.wall_achievable' does not depend on any axioms
'ReorderSurface.wall_tight' depends on axioms: [Quot.sound, propext]
'Incast.overshoot_bound_tight' does not depend on any axioms
'Incast.overshoot_linear_in_fanin' depends on axioms: [Quot.sound, propext]
'Compose.stack_preserves_all' depends on axioms: [Quot.sound, propext]
'Compose.stack_preserves_whole' depends on axioms: [Quot.sound, propext]
'LatencyFloor.fetch_latency_floor' does not depend on any axioms
'LatencyFloor.remote_never_wins_below_floor' depends on axioms: [propext]
'LatencyFloor.pooling_wins_implies_above_floor' does not depend on any axioms
'LatencyFloor.prop_floor_mono' does not depend on any axioms

## serving-limits (serving_limits/formal/lean)
'SpecOptimal.scheme_le_maximal' UNRESOLVED (not found in build output)
'SpecOptimal.two_maxAccept_add_tv' UNRESOLVED (not found in build output)
'IsolationBound.spec_forces_injective' UNRESOLVED (not found in build output)
'IsolationBound.no_three_state_policy' UNRESOLVED (not found in build output)
'IsolationBound.tag_table_sound' UNRESOLVED (not found in build output)
'IsolationBound.essential_bits_general' UNRESOLVED (not found in build output)
'IsolationBound.essential_state_count' UNRESOLVED (not found in build output)
'IsolationBound.stateless_cannot_pool' UNRESOLVED (not found in build output)
'EssentialBits.authMatrix_ext' UNRESOLVED (not found in build output)
'EssentialBits.denseWorld_injective' UNRESOLVED (not found in build output)
'EssentialBits.kv_pool_state_floor' UNRESOLVED (not found in build output)
'EssentialBits.kv_pool_bits_floor' UNRESOLVED (not found in build output)
'EssentialBits.kv_pool_bytes_floor' UNRESOLVED (not found in build output)
'EssentialBits.no_policy_below_floor' UNRESOLVED (not found in build output)
'EssentialBits.kv_pool_theta' UNRESOLVED (not found in build output)
'EssentialBits.tag_table_attains' UNRESOLVED (not found in build output)
'EssentialBits.kv_cache_pool_bits_floor' UNRESOLVED (not found in build output)
'EssentialBits.single_owner_state_floor' UNRESOLVED (not found in build output)
'EssentialBits.single_owner_bits_floor' UNRESOLVED (not found in build output)
'EssentialBits.single_owner_below_dense_strict' UNRESOLVED (not found in build output)
'EssentialBits.single_owner_store_cannot_serve_dense' UNRESOLVED (not found in build output)
'EssentialBits.zero_leak_alone_is_free' UNRESOLVED (not found in build output)
'EssentialBits.full_reuse_alone_is_free' UNRESOLVED (not found in build output)
'StructuredIsolation.structured_forces_injective' UNRESOLVED (not found in build output)
'StructuredIsolation.structured_state_floor' UNRESOLVED (not found in build output)
'StructuredIsolation.structured_state_attained' UNRESOLVED (not found in build output)
'StructuredIsolation.structured_state_theta' UNRESOLVED (not found in build output)
'StructuredIsolation.structured_below_dense' UNRESOLVED (not found in build output)
'StructuredIsolation.structured_bits_concrete' UNRESOLVED (not found in build output)
'StructuredIsolation.shared_forces_injective' UNRESOLVED (not found in build output)
'StructuredIsolation.shared_state_floor' UNRESOLVED (not found in build output)
'StructuredIsolation.shared_state_theta' UNRESOLVED (not found in build output)
'StructuredIsolation.shared_above_owner' UNRESOLVED (not found in build output)
'HierarchicalIsolation.ideals_recursion' UNRESOLVED (not found in build output)
'HierarchicalIsolation.nodes_lt_ideals' UNRESOLVED (not found in build output)
'HierarchicalIsolation.ideals_le_pow' UNRESOLVED (not found in build output)
'HierarchicalIsolation.hier_forces_injective' UNRESOLVED (not found in build output)
'HierarchicalIsolation.hier_state_floor' UNRESOLVED (not found in build output)
'HierarchicalIsolation.hier_between' UNRESOLVED (not found in build output)
'HierarchicalIsolation.undersized_hierarchy_collides' UNRESOLVED (not found in build output)
'HierarchicalIsolation.hier_concrete' UNRESOLVED (not found in build output)
'DisaggCoherence.safe_transfer_forces_distinct' UNRESOLVED (not found in build output)
'DisaggCoherence.isolation_raises_floor' UNRESOLVED (not found in build output)
'DisaggCoherence.safe_above_shared' UNRESOLVED (not found in build output)
'DisaggCoherence.batched_transfer_leaks' UNRESOLVED (not found in build output)
'CertifiedElision.elide_preserves_output' UNRESOLVED (not found in build output)
'CertifiedElision.elide_deployed_drift_bounded' UNRESOLVED (not found in build output)
'CertifiedElision.inconclusive_falls_back_exact' UNRESOLVED (not found in build output)
'CertifiedElision.elision_never_slower' UNRESOLVED (not found in build output)
'CertifiedElision.elide_high_contribution_unsound' UNRESOLVED (not found in build output)
'CertifiedElision.elide_without_fallback_diverges' UNRESOLVED (not found in build output)
'CertifiedElision.cheapEnough_sound' UNRESOLVED (not found in build output)
'CertifiedElision.elide_without_cost_check_slower' UNRESOLVED (not found in build output)
'CertifiedElision.exactness_gate_admits_expensive_skip' UNRESOLVED (not found in build output)
'CertifiedElision.obj_cost_concrete' UNRESOLVED (not found in build output)
'CertifiedElision.page_elision_sound' UNRESOLVED (not found in build output)
'CertifiedElision.vocab_elision_preserves_argmax' UNRESOLVED (not found in build output)
'CertifiedElision.vocab_elision_sound' UNRESOLVED (not found in build output)
'CertifiedElision.vocab_gap_too_small_flips' UNRESOLVED (not found in build output)
'StructuredCapabilityEngine.testBit_fieldOf' UNRESOLVED (not found in build output)
'StructuredCapabilityEngine.field_write_reads_back' UNRESOLVED (not found in build output)
'StructuredCapabilityEngine.field_write_noninterference' UNRESOLVED (not found in build output)
'StructuredCapabilityEngine.undersized_field_collides' UNRESOLVED (not found in build output)
'StructuredCapabilityEngine.structured_engine_attains_floor' UNRESOLVED (not found in build output)
'StructuredCapabilityEngine.structured_engine_attainment' UNRESOLVED (not found in build output)
'StructuredCapabilityEngine.structured_concrete_ops' UNRESOLVED (not found in build output)
'StructuredCapabilityEngine.structured_engine_nonvacuous' UNRESOLVED (not found in build output)
'EvictionSafety.evict_never_pinned' UNRESOLVED (not found in build output)
'EvictionSafety.evict_refuses_when_all_pinned' UNRESOLVED (not found in build output)
'EvictionSafety.evict_is_stalest_unpinned' UNRESOLVED (not found in build output)
'EvictionSafety.lru_evicts_pinned' UNRESOLVED (not found in build output)
'EvictionSafety.evict_admit_safe' UNRESOLVED (not found in build output)
'EvictionSafety.evict_nonvacuous' UNRESOLVED (not found in build output)
'LeakyIsolationBound.bounded_fanin_le' UNRESOLVED (not found in build output)
'LeakyIsolationBound.leaky_dense_floor' UNRESOLVED (not found in build output)
'LeakyIsolationBound.leaky_structured_floor' UNRESOLVED (not found in build output)
'LeakyIsolationBound.rank_lt_k' UNRESOLVED (not found in build output)
'LeakyIsolationBound.rank_mono' UNRESOLVED (not found in build output)
'LeakyIsolationBound.enc_inj' UNRESOLVED (not found in build output)
'LeakyIsolationBound.base_k_unique' UNRESOLVED (not found in build output)
'LeakyIsolationBound.leak_budget_floor' UNRESOLVED (not found in build output)
'LeakyIsolationBound.leaky_2to1_satisfiable' UNRESOLVED (not found in build output)
'LeakyIsolationBound.leaky_witness_leaks' UNRESOLVED (not found in build output)
'CacheCeiling.cold_miss_lower' UNRESOLVED (not found in build output)
'CacheCeiling.hits_upper_wall' UNRESOLVED (not found in build output)
'SubmodularCover.fleet_miss_lower' UNRESOLVED (not found in build output)
'TreeSpec.row_le_bound' UNRESOLVED (not found in build output)
'TreeSpec.row3_le_bound' UNRESOLVED (not found in build output)
'TreeSpec.SpecTree.accept_le_bound' UNRESOLVED (not found in build output)
'PagingLowerBound.genFaults_le_length' UNRESOLVED (not found in build output)
'MdsOptimal.rs_mds_k2' UNRESOLVED (not found in build output)
'MdsOptimal.singleton_attained_k2' UNRESOLVED (not found in build output)
'StateClassBound.spec_forces_injective' UNRESOLVED (not found in build output)
'StateClassBound.essential_states' UNRESOLVED (not found in build output)
'StateClassBound.session_fixation_leaks' UNRESOLVED (not found in build output)
'StateClassBound.confidential_no_three_state_policy' UNRESOLVED (not found in build output)
'StateClassBound.confidential_unowned_serve_leaks' UNRESOLVED (not found in build output)
'KvFloor.kv_floor' UNRESOLVED (not found in build output)
'KvFloor.kv_bits_floor' UNRESOLVED (not found in build output)
'KvFloor.below_floor_collides' UNRESOLVED (not found in build output)
'KvFloor.no_8bit_resume_512' UNRESOLVED (not found in build output)
'KvFloor.identity_attains_floor' UNRESOLVED (not found in build output)
'KvCodec.split_join' UNRESOLVED (not found in build output)
'KvCodec.reblock2_valid' UNRESOLVED (not found in build output)
'KvCodec.lossy_stride_not_injective' UNRESOLVED (not found in build output)
'DistillContract.distill_contract' UNRESOLVED (not found in build output)
'DistillContract.gap_from_acceptance' UNRESOLVED (not found in build output)
'DistillContract.far_student_large_gap' UNRESOLVED (not found in build output)
'BoundedCodec.roundtrip_err_le' UNRESOLVED (not found in build output)
'BoundedCodec.step_one_exact' UNRESOLVED (not found in build output)
'BoundedCodec.floor_quant_unsound' UNRESOLVED (not found in build output)
'BoundedCodec.codec_stage_admit' UNRESOLVED (not found in build output)
'BoundedCodec.codec_concrete' UNRESOLVED (not found in build output)
'SecureFloor.secure_floor' UNRESOLVED (not found in build output)
'SecureFloor.floor_gate_no_leak' UNRESOLVED (not found in build output)
'SecureFloor.floor_gate_interferes' UNRESOLVED (not found in build output)
'SecureFloor.floor_gate_branchless_eq' UNRESOLVED (not found in build output)
'SecureFloor.floor_gate_ungated_leaks' UNRESOLVED (not found in build output)
'SecureFloor.secure_pool_lower_bound' UNRESOLVED (not found in build output)
'SecureFloor.secure_pool_attained' UNRESOLVED (not found in build output)
'CommBound.rectangle' UNRESOLVED (not found in build output)
'CommBound.eq_transcript_injective_on_diagonal' UNRESOLVED (not found in build output)
'CommBound.auth_transcript_injective' UNRESOLVED (not found in build output)
'CommBound.one_machine_breaks_rectangle' UNRESOLVED (not found in build output)
'CommBound.enc_inj' UNRESOLVED (not found in build output)
'CommBound.all_transcripts_short_impossible' UNRESOLVED (not found in build output)
'CommBound.eq_forces_k_wire_bits' UNRESOLVED (not found in build output)
'EnergyFloor.auth_energy_floor' UNRESOLVED (not found in build output)
'EnergyFloor.energy_floor_lower' UNRESOLVED (not found in build output)
'EnergyFloor.recompute_wins_below_energy_floor' UNRESOLVED (not found in build output)
'CostFloor.unified_cost_floor' UNRESOLVED (not found in build output)
'CostFloor.latency_floor_binds' UNRESOLVED (not found in build output)
'CreditEssential.credit_spec_forces_injective' UNRESOLVED (not found in build output)
'CreditEssential.essential_occupancy_count' UNRESOLVED (not found in build output)
'KDraftOT.kdraft_accept_le_ot' UNRESOLVED (not found in build output)
'KDraftOT.ot_beats_naive' UNRESOLVED (not found in build output)
'KDraftOT.cover2_lt_naive' UNRESOLVED (not found in build output)
'KDraftOT.ot_attained' UNRESOLVED (not found in build output)
'KDraftOT.kdraft_generalizes_k1' UNRESOLVED (not found in build output)

## State-Fabric (statefabric/formal/lean)
'TenantGate.tenant_gate_no_leak' depends on axioms: [Quot.sound, propext]
'TenantGate.public_read_noninterference' depends on axioms: [propext]
'TenantGate.servedCT_eq' does not depend on any axioms
'TenantGate.servedMask_eq' depends on axioms: [Quot.sound, propext]
'TenantGate.tenant_gate_no_leak_mask' depends on axioms: [Quot.sound, propext]
'LayoutBijection.layout_roundtrip_id' does not depend on any axioms
'LayoutBijection.layout_roundtrip_id'' does not depend on any axioms
'RemoteReadGate.remote_read_tenant_safe' depends on axioms: [Quot.sound, propext]
'ControlPlane.control_plane_admits_safe' depends on axioms: [Quot.sound, propext]
'TransportStateCompose.compose_read_consistent' does not depend on any axioms
'TransportStateCompose.compose_transport_violation_tears' depends on axioms: [Quot.sound, propext]
'QuantBound.attnBound_perhead_le_global' depends on axioms: [Quot.sound, propext]
'DriftLedger.stack_append' depends on axioms: [Quot.sound, propext]
'DriftLedger.compose_sound' depends on axioms: [Quot.sound, propext]
'DriftLedger.stack_le_pin_max' depends on axioms: [Quot.sound, propext]
'DriftLedger.unaccounted_stack_unsound' does not depend on any axioms
'DriftLedger.codec_stack_admitted_int4_stack_rejected' does not depend on any axioms
'BranchShare.branch_memory_saving' depends on axioms: [Quot.sound, propext]
'BranchShare.readsOnlyPrefix_noninterference' does not depend on any axioms
'BranchShare.readPrefix_readsOnly' does not depend on any axioms
'BranchShare.interferingRead_not_readsOnly' depends on axioms: [propext]
'BranchShare.interfering_read_leaks' does not depend on any axioms
'RolloutGate.admit_sound' does not depend on any axioms
'RolloutGate.mismatch_refused' does not depend on any axioms
'RolloutGate.nonfinite_refused' does not depend on any axioms
'RolloutGate.select_admitted_sound' depends on axioms: [propext]
'RolloutGate.select_falls_back' does not depend on any axioms
'RolloutGate.rollout_concrete' does not depend on any axioms
'MlaBound.mla_admit_sound' depends on axioms: [Quot.sound, propext]
'MlaBound.mla_stage_composes' does not depend on any axioms
'MlaBound.bound_only_unsound' depends on axioms: [propext]
'MlaBound.recovery_needle_fail_refused' depends on axioms: [propext]
'OrderPreservation.topk_stable_under_gap' depends on axioms: [Quot.sound, propext]
'OrderPreservation.no_gap_flips' does not depend on any axioms
'OrderPreservation.retentionOk_sound' depends on axioms: [Quot.sound, propext]
'OrderPreservation.recovery_retention_mechanistic' depends on axioms: [propext]
'OrderPreservation.stable_under_certified_drift' depends on axioms: [Quot.sound, propext]

## runtime-gates (runtime_gates/formal/lean)
'RuntimeGate.spec_gated_never_slower' depends on axioms: [propext]
'RuntimeGate.spec_always_on_strictly_loses' depends on axioms: [propext]
'RuntimeGate.prec_l2_only_unsound' does not depend on any axioms
'RuntimeGate.attest_null_no_gain' depends on axioms: [propext]

## inference-gates:MoeVram (inference_gates/formal/lean)
'MoeVram.moe_vram_admits' does not depend on any axioms
'MoeVram.moeAdmit_sound' depends on axioms: [propext]
'MoeVram.moe_vram_oom' does not depend on any axioms

## applied-domains (applied_domains/formal/lean)
'GraphDeadlock.acyclic_has_drain' depends on axioms: [Quot.sound, propext]
'GraphDeadlock.no_closed_walk' does not depend on any axioms
'DroneSwarmDeadlock.swarm_no_deadlock' depends on axioms: [Quot.sound, propext]
'DroneSwarmDeadlock.swarm_cycle_deadlocks' depends on axioms: [propext]
'NocDeadlock.noc_no_deadlock' depends on axioms: [Quot.sound, propext]
'NocDeadlock.noc_cycle_deadlocks' depends on axioms: [propext]
'WarehouseGrid.grid_no_gridlock' depends on axioms: [Quot.sound, propext]
'WarehouseGrid.grid_4way_gridlock' depends on axioms: [Quot.sound, propext]
'K8sZeroTrust.pod_isolation_no_leak' does not depend on any axioms
'BgpConvergence.bad_gadget_no_stable' does not depend on any axioms
'PipeSchedule.pipe_no_deadlock' depends on axioms: [Quot.sound, propext]
'PipeSchedule.bubble_floor' depends on axioms: [Quot.sound, propext]
'PipeSchedule.pipe_cycle_wedges' does not depend on any axioms
'PipeSchedule.bubble_floor_finOpt' depends on axioms: [Quot.sound, propext]
'AgentFabric.cap_monotone' depends on axioms: [propext]
'AgentFabric.toolAdmit_sound' does not depend on any axioms
'AgentFabric.escalation_refused' does not depend on any axioms
'AgentFabric.agent_no_deadlock' depends on axioms: [Quot.sound, propext]
'AgentFabric.agent_tool_cycle_wedges' does not depend on any axioms

## exchange-gates (exchange_gates/formal/lean)
'ExchangeGate.settle_implies_safe' depends on axioms: [propext]
'ExchangeGate.settled_trade_splits_recompute' depends on axioms: [Quot.sound, propext]
'SpotSettle.spot_settle_contract' depends on axioms: [Quot.sound, propext]
'SpotSettle.drain_zero_loss' depends on axioms: [Quot.sound, propext]
'SpotSettle.unverified_resume_admits_torn' does not depend on any axioms
'SpotSettle.ungated_double_settles' depends on axioms: [propext]
'SpotSettle.spot_settle_concrete' does not depend on any axioms
'CachedTokenMeter.conservation' does not depend on any axioms
'CachedTokenMeter.no_overbill' does not depend on any axioms
'CachedTokenMeter.meterAdmit_sound' does not depend on any axioms
'CachedTokenMeter.phantom_hit_refused' does not depend on any axioms
'CachedTokenMeter.eviction_monotone' does not depend on any axioms
'BillingLedger.invoice_append' depends on axioms: [Quot.sound, propext]
'BillingLedger.invoice_conservation' depends on axioms: [Quot.sound, propext]
'BillingLedger.invoice_mono' depends on axioms: [Quot.sound, propext]
'BpeTokenCount.count_le_bytes' depends on axioms: [Quot.sound, propext]
'BpeTokenCount.count_mono_merges' depends on axioms: [Quot.sound, propext]
'BpeTokenCount.overcount_impossible' depends on axioms: [Quot.sound, propext]
'KvMarketplace.reblock_valid_is_id' depends on axioms: [propext]
'KvMarketplace.listing_clears_safe' depends on axioms: [propext]
'KvMarketplace.listing_clears_provenance' depends on axioms: [propext]
'KvMarketplace.listing_clears_deliverable' depends on axioms: [propext]
'KvMarketplace.unprovenanced_refused' depends on axioms: [propext]
'KvMarketplace.no_layout_refused' depends on axioms: [propext]
'KvMarketplace.basket_conservation' depends on axioms: [Quot.sound, propext]
'PricedBilling.invoice_cost_append' depends on axioms: [Quot.sound, propext]
'PricedBilling.cached_read_discount_saves' depends on axioms: [Quot.sound, propext]
'PricedBilling.safe_bill_sound' depends on axioms: [Quot.sound, propext]
'PricedBilling.overbill_refused_at_any_price' does not depend on any axioms
'PricedBilling.priced_concrete' does not depend on any axioms

## training-gates (training_gates/formal/lean)
'ShardMemory.shardAdmit_sound' does not depend on any axioms
'ShardMemory.more_shards_less_resident' depends on axioms: [Quot.sound, propext]
'ShardMemory.underprovisioned_refused' does not depend on any axioms
'CommSchedule.step_le_serial' depends on axioms: [Quot.sound, propext]
'CommSchedule.step_ge_compute' depends on axioms: [Quot.sound, propext]
'CommSchedule.full_overlap_hides_comm' depends on axioms: [Quot.sound, propext]
'CommSchedule.no_overlap_serial' depends on axioms: [Quot.sound, propext]
'RestartReceipt.verified_restart' depends on axioms: [propext]
'RestartReceipt.torn_checkpoint_refused' does not depend on any axioms
'RestartReceipt.double_restart_refused' does not depend on any axioms
'RestartReceipt.over_parity_unrecoverable' does not depend on any axioms
'RestartReceipt.restart_contract' depends on axioms: [propext]
'ShardMemory3D.nested_ceilDiv_eq' depends on axioms: [Quot.sound, propext]
'ShardMemory3D.shard3D_admit_sound' does not depend on any axioms
'ShardMemory3D.dp_helps' depends on axioms: [Quot.sound, propext]
'ShardMemory3D.underprovisioned3D_refused' does not depend on any axioms
'PlanAdmit.plan_admits_safe' depends on axioms: [propext]
'PlanAdmit.commAdmit_sound' does not depend on any axioms
'PlanAdmit.drop_comm_admits_networkbound' does not depend on any axioms
'PlanAdmit.plan_admits_legit' does not depend on any axioms

## compression-gates (compression_gates/formal/lean)
'EvictionGate.ev_admit_sound' does not depend on any axioms
'EvictionGate.single_probe_only_unsound' does not depend on any axioms
'EvictionGate.ev_verify_or_fallback_exact' does not depend on any axioms
'EvictionGate.ev_deployed_drop_bounded' depends on axioms: [propext]
'AttentionMass.drift_decomposes' depends on axioms: [propext]
'AttentionMass.retained_mass_bounds_drift' depends on axioms: [propext]
'AttentionMass.massAdmit_sound' depends on axioms: [propext]
'AttentionMass.drop_high_mass_unsound' does not depend on any axioms
'AttentionMass.no_drop_no_drift' depends on axioms: [propext]

## moe-routing (moe_routing_gates/formal/lean)
'MoeRouting.route_isolated_noninterference' depends on axioms: [propext]
'MoeRouting.seeded_adversary_influence_bound' depends on axioms: [propext]
'MoeRouting.det_tiebreak_leaks' does not depend on any axioms
'MoeRouting.seeded_survives_where_det_leaks' does not depend on any axioms
'MoeRouting.batch_leak_forces_outcomes' depends on axioms: [Quot.sound, propext]
'MoeRouting.seeded_leak_free' depends on axioms: [Quot.sound, propext]
'MoeRouting.routeAdmit_sound' depends on axioms: [propext]
'MoeRouting.admit_implies_kept' depends on axioms: [propext]
'MoeRouting.routeAdmit_refuses_position' does not depend on any axioms
'RoutingCore.inj_le' depends on axioms: [Quot.sound, propext]

## moe-hardness (moe_hardness/formal/lean)
'MoeHardness.red_correct' depends on axioms: [Quot.sound, propext]
'MoeHardness.red_sound' depends on axioms: [propext]
'MoeHardness.red_complete' depends on axioms: [Quot.sound, propext]
'MoeHardness.fiber_sum' depends on axioms: [Quot.sound, propext]
'MoeHardness.all_eq_of_le_and_sum' depends on axioms: [Quot.sound, propext]
'MoeHardness.sumFin_single' depends on axioms: [Quot.sound, propext]
'MoeHardness.item_le_groupSum' depends on axioms: [propext]
'MoeHardness.moe_place_decide_correct' depends on axioms: [propext]
'MoeHardness.reduction_yes_witness' depends on axioms: [propext]
'MoeHardness.reduction_no_witness' depends on axioms: [Quot.sound, propext]
'MoeHardness.makespan_gap' depends on axioms: [Quot.sound, propext]
'MoeHardness.red_yes_makespan_le_B' depends on axioms: [propext]
'MoeHardness.red_no_makespan_gt_B' depends on axioms: [Quot.sound, propext]
'MoeHardness.no_makespan_witness' depends on axioms: [propext]

## io-complexity (io_complexity/formal/lean)
'IoComplexity.flash_io_le' does not depend on any axioms
'IoComplexity.flash_trajectory_valid' depends on axioms: [Quot.sound, propext]
'IoComplexity.flash_io_concrete' does not depend on any axioms
'IoComplexity.compulsory_io_lower' depends on axioms: [Quot.sound, propext]
'IoComplexity.io_lb_matches_ub_restricted' depends on axioms: [Quot.sound, propext]
'IoComplexity.mem_invariant_holds' does not depend on any axioms
'IoComplexity.recompute_breaks_compulsory' depends on axioms: [Quot.sound, propext]

## comm-floor (comm_floor/formal/lean)
'CommFloor.lw_cube_tight' depends on axioms: [propext]
'CommFloor.cube_meets_cap' depends on axioms: [propext]
'CommFloor.lw_box_tight' depends on axioms: [propext]
'CommFloor.box_meets_cap' depends on axioms: [propext]
'CommFloor.gemm_comm_lower' depends on axioms: [propext]
'CommFloor.gemm_floor_tight_witness' does not depend on any axioms
'CommFloor.memory_cap_load_bearing' does not depend on any axioms
'CommFloor.bisection_time_lower' depends on axioms: [Quot.sound, propext]
'CommFloor.cluster_bandwidth_floor' does not depend on any axioms
'CommFloor.cluster_floor_violated' does not depend on any axioms
'CommFloor.cluster_floor_composed' does not depend on any axioms
'CommFloor.cluster_floor_concrete' does not depend on any axioms
'CommFloor.commAdmit_sound' does not depend on any axioms
'CommFloor.commAdmit_refuses_underprovisioned' does not depend on any axioms
'CommFloor.sfCommAdmit' does not depend on any axioms
'CommFloor.gate_refuse_forces_network_bound' does not depend on any axioms
'CommFloor.gate_admit_meets_floor' does not depend on any axioms
'CommFloor.cs_weighted' depends on axioms: [Quot.sound, propext]
'CommFloor.box2d' depends on axioms: [Quot.sound, propext]
'CommFloor.discrete_loomis_whitney' depends on axioms: [Quot.sound, propext]
'CommFloor.loomis_whitney_cube_cap' depends on axioms: [Quot.sound, propext]
'CommFloor.gemm_comm_lower_selfcontained' depends on axioms: [Quot.sound, propext]
'CommFloor.gemm_selfcontained_witness' depends on axioms: [Quot.sound, propext]
'CommFloor.ring_meets_floor' depends on axioms: [Quot.sound, propext]
'CommFloor.ring_is_optimal' depends on axioms: [Quot.sound, propext]
'CommFloor.ring_total_crossing' depends on axioms: [propext]
'CommFloor.naive_exceeds_ring' depends on axioms: [Quot.sound, propext]
'CommFloor.collective_floor_concrete' does not depend on any axioms

## audit-chain (audit_chain/formal/lean)
'AuditChain.chain_binds_history' depends on axioms: [propext]
'AuditChain.no_orphan_action' depends on axioms: [propext]
'AuditChain.record_complete' depends on axioms: [propext]
'AuditChain.record_sound' depends on axioms: [propext]
'AuditChain.dropping_loses_record' depends on axioms: [Quot.sound, propext]
'AuditChain.audit_trail_binds' depends on axioms: [propext]
'AuditChain.chainLink_sound' does not depend on any axioms
'AuditChain.chainLink_refuses_mismatch' does not depend on any axioms
'AuditChain.sfChainVerify' does not depend on any axioms

## record-floor (serving_limits/formal/lean)
'RecordFloor.rectangle_mix' depends on axioms: [propext]
'RecordFloor.allEq_transcript_injective_on_diagonal' depends on axioms: [Quot.sound, propext]
'RecordFloor.allEq_forces_k_record_bits' depends on axioms: [Quot.sound, propext]
'RecordFloor.cap_monotone' depends on axioms: [propext]
'RecordFloor.auditable_chain_record_floor' depends on axioms: [Quot.sound, propext]
'RecordFloor.one_machine_breaks_box3' depends on axioms: [propext]
'RecordFloor.eqProt3_correct' depends on axioms: [propext]
'RecordFloor.diag_injective_fin2' depends on axioms: [Quot.sound, propext]
'RecordFloor.chain_narrows_concrete' does not depend on any axioms

## key-domain separation (theory/lean KeyDomainSeparation)
'KeyDomainSeparation.untagged_admits_cross_source' UNRESOLVED (not found in build output)
'KeyDomainSeparation.lora_ne_salt' UNRESOLVED (not found in build output)
'KeyDomainSeparation.separating_insufficient' UNRESOLVED (not found in build output)
'KeyDomainSeparation.tagged_refuses_cross_source' UNRESOLVED (not found in build output)
'KeyDomainSeparation.tagged_preserves_same_source' UNRESOLVED (not found in build output)
'KeyDomainSeparation.tagged_separates_tenants' UNRESOLVED (not found in build output)
'KeyDomainSeparation.domain_separation_contract' UNRESOLVED (not found in build output)
'KeyDomainSeparation.untagged_list_admits_cross_source' UNRESOLVED (not found in build output)
'KeyDomainSeparation.lora_list_ne_salt_list' UNRESOLVED (not found in build output)
'KeyDomainSeparation.separating_insufficient_list' UNRESOLVED (not found in build output)
'KeyDomainSeparation.tagged_list_refuses_cross_source' UNRESOLVED (not found in build output)
'KeyDomainSeparation.tListEq_refl' UNRESOLVED (not found in build output)
'KeyDomainSeparation.tagged_list_preserves_same_source' UNRESOLVED (not found in build output)
'KeyDomainSeparation.order_is_load_bearing' UNRESOLVED (not found in build output)
'KeyDomainSeparation.tagged_list_separates_tenants' UNRESOLVED (not found in build output)
'KeyDomainSeparation.untagged_list_admits_any_cross_source' UNRESOLVED (not found in build output)
'KeyDomainSeparation.tagged_list_refuses_any_cross_source' UNRESOLVED (not found in build output)
'KeyDomainSeparation.four_source_contract' UNRESOLVED (not found in build output)
'KeyDomainSeparation.lora_salt_really_collides' UNRESOLVED (not found in build output)
'KeyDomainSeparation.lora_mm_impossible' UNRESOLVED (not found in build output)
'KeyDomainSeparation.lora_embed_impossible' UNRESOLVED (not found in build output)
'KeyDomainSeparation.mm_salt_impossible' UNRESOLVED (not found in build output)
'KeyDomainSeparation.mm_embed_impossible' UNRESOLVED (not found in build output)
'KeyDomainSeparation.salt_embed_impossible' UNRESOLVED (not found in build output)
'KeyDomainSeparation.exactly_one_real_cross_source_collision' UNRESOLVED (not found in build output)

## block-chain hash (theory/lean BlockChainHash)
'BlockChainHash.chain_prefix_stable' depends on axioms: [propext]
'BlockChainHash.chain_length_le' depends on axioms: [propext]
'BlockChainHash.chain_diverges_after_salt' depends on axioms: [propext]
'BlockChainHash.first_block_only_bounds_collision' depends on axioms: [propext]
'BlockChainHash.chain_separating_of_first_block_separating' depends on axioms: [propext]
'BlockChainHash.blocksFuel_flatten' depends on axioms: [Quot.sound, propext]
'BlockChainHash.blocks_flatten' depends on axioms: [Quot.sound, propext]
'BlockChainHash.partial_block_kept' depends on axioms: [propext]
'BlockChainHash.predictReuse_quantised' depends on axioms: [propext]
'BlockChainHash.predictReuse_le_shared' depends on axioms: [propext]
'BlockChainHash.predictReuseDiffKeys_zero_regardless' does not depend on any axioms

## salt secrecy (theory/lean SaltSecrecy)
'SaltSecrecy.public_is_recomputable' does not depend on any axioms
'SaltSecrecy.recomputed_key_matches' does not depend on any axioms
'SaltSecrecy.attack_does_not_violate_separation' does not depend on any axioms
'SaltSecrecy.keyed_not_publicly_recomputable' does not depend on any axioms
'SaltSecrecy.keyed_separating_of_injective' does not depend on any axioms
'SaltSecrecy.reuse_preservation_is_free' does not depend on any axioms
'SaltSecrecy.request_dependent_derivation_breaks_reuse' does not depend on any axioms
'SaltSecrecy.hardening_contract' does not depend on any axioms

## salt-entropy (theory/lean SaltEntropy)
'SaltEntropy.salt_floor' depends on axioms: [Quot.sound, propext]
'SaltEntropy.undersized_cannot_separate' depends on axioms: [Quot.sound, propext]
'SaltEntropy.collision_forced' depends on axioms: [Quot.sound, propext]
'SaltEntropy.collision_admits_cross_tenant_match' depends on axioms: [propext]
'SaltEntropy.undersized_salt_leaks' depends on axioms: [Quot.sound, propext]
'SaltEntropy.bits_floor' depends on axioms: [Quot.sound, propext]
'SaltEntropy.insufficient_bits' depends on axioms: [Quot.sound, propext]
'SaltEntropy.modKey8_not_separating' depends on axioms: [propext]
'SaltEntropy.modKey8_leaks_concretely' depends on axioms: [propext]
'SaltEntropy.three_bits_cannot_separate_nine' depends on axioms: [Quot.sound, propext]
'SaltEntropy.padKey_separating' does not depend on any axioms
'SaltEntropy.padKey_clears_floor' depends on axioms: [Quot.sound, propext]
'SaltEntropy.nine_tenants_need_four_bits' does not depend on any axioms
'SaltEntropy.ten_thousand_tenants_need_fourteen_bits' does not depend on any axioms
'SaltEntropy.thirteen_bits_cannot_separate_ten_thousand' depends on axioms: [Quot.sound, propext]
'SaltEntropy.deployed_salt_space_clears_floor' does not depend on any axioms

## disagg-coherence-3 (serving_limits/formal/lean)
'DisaggCoherence3.safe_hop_forces_distinct' depends on axioms: [Quot.sound, propext]
'DisaggCoherence3.safe_two_hops_force_distinct' depends on axioms: [Quot.sound, propext]
'DisaggCoherence3.safe_disagg3_floor' does not depend on any axioms
'DisaggCoherence3.safe3_is_two_tolls' does not depend on any axioms
'DisaggCoherence3.safe3_eq_T_mul_shared' does not depend on any axioms
'DisaggCoherence3.isolation_raises_floor3' depends on axioms: [Quot.sound, propext]
'DisaggCoherence3.safe_above_shared3' depends on axioms: [Quot.sound, propext]
'DisaggCoherence3.gap_grows_with_T' depends on axioms: [Quot.sound, propext]
'DisaggCoherence3.safe_monotone_in_T' depends on axioms: [Quot.sound, propext]
'DisaggCoherence3.three_stage_exceeds_two_stage' depends on axioms: [Quot.sound, propext]
'DisaggCoherence3.batched_second_hop_leaks' depends on axioms: [Quot.sound, propext]
'DisaggCoherence3.batched_first_hop_leaks' depends on axioms: [Quot.sound, propext]
'DisaggCoherence3.safe_three_stage_exists' does not depend on any axioms
'DisaggCoherence3.disagg3_concrete' does not depend on any axioms

## randomized-isolator (serving_limits/formal/lean)
'RandomizedIsolator.no_seed_is_injective' depends on axioms: [Quot.sound, propext]
'RandomizedIsolator.every_seed_has_big_fiber' depends on axioms: [Quot.sound, propext]
'RandomizedIsolator.seed_secrecy_does_not_shrink_state' depends on axioms: [Quot.sound, propext]
'RandomizedIsolator.family_floor_uniform' depends on axioms: [Quot.sound, propext]
'RandomizedIsolator.witness_every_seed_fiber_ge_four' does not depend on any axioms
'RandomizedIsolator.identity_seed_is_injective' does not depend on any axioms
'RandomizedIsolator.identity_no_aliasing' does not depend on any axioms

## residency-bound (theory/lean ResidencyBound)
'ResidencyBound.eviction_forced' depends on axioms: [propext]
'ResidencyBound.oracle_precondition_fails' depends on axioms: [propext]
'ResidencyBound.fits_implies_probeable' depends on axioms: [propext]
'ResidencyBound.kv_ratio_is_96_over_7' does not depend on any axioms
'ResidencyBound.kv_ratio_not_exactly_13_7' does not depend on any axioms
'ResidencyBound.phi3_precondition_fails' depends on axioms: [propext]
'ResidencyBound.phi3_only_eight_resident' does not depend on any axioms
'ResidencyBound.qwen_precondition_holds' depends on axioms: [propext]
'ResidencyBound.residency_separates_the_two_models' depends on axioms: [propext]
'ResidencyBound.phi3_observable_with_headroom' depends on axioms: [propext]

## leaky-rate-bound (serving_limits/formal/lean)
'LeakyRateBound.max_fiber_floor' depends on axioms: [Quot.sound, propext]
'LeakyRateBound.big_fiber_of_small_state' depends on axioms: [Quot.sound, propext]
'LeakyRateBound.worst_case_leak_rate_floor' depends on axioms: [Quot.sound, propext]
'LeakyRateBound.exact_is_rate_zero' does not depend on any axioms
'LeakyRateBound.exact_floor_recovered' depends on axioms: [Quot.sound, propext]
'LeakyRateBound.rate_floor_at_witness_params' depends on axioms: [Quot.sound, propext]
'LeakyRateBound.rate_witness_concrete' depends on axioms: [propext]
'LeakyRateBound.drop_size_premise_fails' does not depend on any axioms
'LeakyRateBound.boundary_tight' depends on axioms: [propext]
'LeakyRateBound.fibCount_le_maxFib' depends on axioms: [propext]
'LeakyRateBound.le_foldr_max' depends on axioms: [propext]

## verified-kernels:BatchInvariance (verified_kernels/formal/lean)
'BatchInvariance.batch_invariant' depends on axioms: [propext]
'BatchInvariance.variable_split_varies' depends on axioms: [propext]
'BatchInvariance.split_order_matters' does not depend on any axioms
'BatchInvariance.invariance_iff_fixed_split' depends on axioms: [propext]

## reuse-receipt (exchange_gates/formal/lean)
'ReuseReceipt.net_settle_splits_recompute' depends on axioms: [Quot.sound, propext]
'ReuseReceipt.overhead_can_flip_gainful' does not depend on any axioms
'ReuseReceipt.phantom_hit_refused' does not depend on any axioms
'ReuseReceipt.net_settle_implies_safe' depends on axioms: [propext]
'ReuseReceipt.net_savings_pos' depends on axioms: [Quot.sound, propext]
'ReuseReceipt.clearsNet_gain' depends on axioms: [propext]
'ReuseReceipt.reuse_concrete' does not depend on any axioms

## cap-engine (serving_limits/formal/lean)
'CapabilityEngine.grant_serves' depends on axioms: [Quot.sound, propext]
'CapabilityEngine.revoke_unsets' depends on axioms: [Quot.sound, propext]
'CapabilityEngine.grant_preserves_other' depends on axioms: [Quot.sound, propext]
'CapabilityEngine.revoke_preserves_other' depends on axioms: [Quot.sound, propext]
'CapabilityEngine.cap_engine_sound_concrete' depends on axioms: [propext]
'CapabilityEngine.cap_engine_injective' does not depend on any axioms
'CapabilityEngine.cap_engine_attains_floor' depends on axioms: [Quot.sound, propext]
'CapabilityEngine.cap_engine_state_count' depends on axioms: [Quot.sound, propext]
'CapabilityEngine.undersized_aliases' depends on axioms: [propext]
'CapabilityEngine.grant_revoke_concrete' depends on axioms: [propext]
'CapabilityEngine.sfCapServe' depends on axioms: [propext]

## state-transaction (statefabric/formal/lean)
'StateTransaction.txn_admits_all_three' depends on axioms: [propext]
'StateTransaction.drop_atomicity_admits_split_brain' does not depend on any axioms
'StateTransaction.drop_record_admits_orphan' does not depend on any axioms
'StateTransaction.drop_econ_admits_net_loss' does not depend on any axioms
'StateTransaction.flagship_admits_all_four' depends on axioms: [propext]
'StateTransaction.drop_witness_admits_fabricated' does not depend on any axioms
'StateTransaction.flagship_admits_legit' does not depend on any axioms
'StateTransaction.txn_admits_legit' does not depend on any axioms

## branch-txn (statefabric/formal/lean)
'BranchTxnState.branch_txn_safe' depends on axioms: [Quot.sound, propext]
'BranchTxnState.branch_reads_serializable' depends on axioms: [propext]
'BranchTxnState.atomic_xor' depends on axioms: [propext]
'BranchTxnState.abort_no_trace' depends on axioms: [propext]
'BranchTxnState.branch_share_identity' depends on axioms: [Quot.sound, propext]
'BranchTxnState.branchTxnAdmit_sound' depends on axioms: [Quot.sound, propext]
'BranchTxnState.commit_without_fence_tears_sibling' depends on axioms: [propext]
'BranchTxnState.broken_abort_drops_owner' depends on axioms: [propext]
'BranchTxnState.unbound_read_tears' does not depend on any axioms
'BranchTxnState.branch_txn_admits_concrete' depends on axioms: [propext]
'BranchTxnState.sfBranchTxnAdmit' depends on axioms: [propext]

## selective-recovery (fabric_gates/formal/lean)
'SelectiveRecovery.partial_reconstruct_selective' depends on axioms: [Quot.sound, propext]
'SelectiveRecovery.reconstruct_selective_survivor' depends on axioms: [propext]
'SelectiveRecovery.reconstruct_touches_survivor_unsound' does not depend on any axioms
'SelectiveRecovery.survivors_make_progress' depends on axioms: [Quot.sound, propext]
'SelectiveRecovery.stalled_survivors_dont_progress' depends on axioms: [Quot.sound, propext]
'SelectiveRecovery.rebuild_hidden_under_slack' depends on axioms: [Quot.sound, propext]
'SelectiveRecovery.rebuild_exceeds_slack_stalls' depends on axioms: [propext]
'SelectiveRecovery.selective_recovery_contract' depends on axioms: [Quot.sound, propext]
'SelectiveRecovery.selectiveRecoveryAdmit_sound' depends on axioms: [propext]
'SelectiveRecovery.sfSelectiveRecoveryAdmit' does not depend on any axioms

## confidential-offload (confidential_offload/formal/lean)
'ConfidentialOffload.offload_noninterference' does not depend on any axioms
'ConfidentialOffload.padded_serves_kept' depends on axioms: [Quot.sound, propext]
'ConfidentialOffload.naive_demand_load_leaks' does not depend on any axioms
'ConfidentialOffload.demand_needs_full_pattern_space' depends on axioms: [Quot.sound, propext]
'ConfidentialOffload.offloadAdmit_sound' depends on axioms: [propext]
'ConfidentialOffload.offloadAdmit_refuses_demand' does not depend on any axioms
'ConfidentialOffload.offload_concrete' does not depend on any axioms
'ConfidentialOffload.sfOffloadAdmit' does not depend on any axioms

## reuse-control (reuse_control/formal/lean)
'ReuseControl.reuse_admit_implies_all' depends on axioms: [propext]
'ReuseControl.reuse_receipt_binds_log' depends on axioms: [Quot.sound, propext]
'ReuseControl.drop_isolation_leaks' does not depend on any axioms
'ReuseControl.drop_provenance_forges' does not depend on any axioms
'ReuseControl.drop_settlement_mints' does not depend on any axioms
'ReuseControl.drop_logging_orphans' does not depend on any axioms
'ReuseControl.reuseAdmitBits_sound' depends on axioms: [propext]
'ReuseControl.reuse_concrete' does not depend on any axioms
'ReuseControl.control_plane_admits_confidential' depends on axioms: [propext]
'ReuseControl.control_plane_drop_offload_overbudget' does not depend on any axioms
'ReuseControl.control_plane_drop_offload_demand' does not depend on any axioms
'ReuseControl.control_plane_drop_reuse' does not depend on any axioms
'ReuseControl.sfKvReuseAdmit' does not depend on any axioms

## crypto-erasure (crypto_erasure/formal/lean)
'CryptoErasure.erase_forbids_serve' does not depend on any axioms
'CryptoErasure.erase_forbids_decrypt' does not depend on any axioms
'CryptoErasure.erase_tenant_complete' depends on axioms: [Quot.sound, propext]
'CryptoErasure.erase_keyless_noninterference' depends on axioms: [propext]
'CryptoErasure.soft_delete_leaks' does not depend on any axioms
'CryptoErasure.eraseAdmit_sound' depends on axioms: [propext]
'CryptoErasure.eraseAdmit_refuses_erased' does not depend on any axioms
'CryptoErasure.sfEraseAdmit' does not depend on any axioms

## data-residency (data_residency/formal/lean)
'DataResidency.residency_no_cross_region' depends on axioms: [Quot.sound, propext]
'DataResidency.residency_in_region' depends on axioms: [Quot.sound, propext]
'DataResidency.serve_store_in_region' depends on axioms: [Quot.sound, propext]
'DataResidency.cross_region_leaks' does not depend on any axioms
'DataResidency.residencyAdmit_sound' depends on axioms: [Quot.sound, propext]
'DataResidency.sfResidencyAdmit' does not depend on any axioms

## agent-lineage (agent_lineage/formal/lean)
'AgentLineage.lineage_no_orphan' does not depend on any axioms
'AgentLineage.lineage_admits_rooted' does not depend on any axioms
'AgentLineage.orphan_effect_leaks' does not depend on any axioms
'AgentLineage.admit_batch_all_rooted' depends on axioms: [propext]
'AgentLineage.sfLineageAdmit' does not depend on any axioms

## write-isolation (write_isolation/formal/lean)
'WriteIsolation.write_noninterference' does not depend on any axioms
'WriteIsolation.write_noninterference_twice' does not depend on any axioms
'WriteIsolation.serve_own' does not depend on any axioms
'WriteIsolation.ungated_poisons' does not depend on any axioms
'WriteIsolation.sfWriteAdmit' does not depend on any axioms

## weight-extraction (weight_extraction/formal/lean)
'WeightExtraction.extraction_query_floor' depends on axioms: [Quot.sound, propext]
'WeightExtraction.undersized_channel_collides' depends on axioms: [Quot.sound, propext]
'WeightExtraction.extractionSafe_sound' does not depend on any axioms
'WeightExtraction.extraction_concrete_safe' does not depend on any axioms
'WeightExtraction.sfExtractionSafe' does not depend on any axioms

## compliance-plane (compliance_plane/formal/lean)
'CompliancePlane.compliant_serve_honors_all_mandates' depends on axioms: [Quot.sound, propext]
'CompliancePlane.compliance_admits_all_mandates' depends on axioms: [Quot.sound, propext]
'CompliancePlane.drop_erasure_admits_forgotten' does not depend on any axioms
'CompliancePlane.drop_residency_admits_transfer' does not depend on any axioms
'CompliancePlane.drop_lineage_admits_orphan' does not depend on any axioms
'CompliancePlane.drop_write_admits_poison' does not depend on any axioms
'CompliancePlane.drop_extraction_admits_theft' does not depend on any axioms
'CompliancePlane.compliance_concrete' does not depend on any axioms
'CompliancePlane.sfComplianceAdmit' does not depend on any axioms

## tenant-partition close (theory/lean TenantPartition)
'TenantPartition.separated_no_cross_tenant_match' does not depend on any axioms
'TenantPartition.same_tenant_same_prefix_matches' depends on axioms: [propext]
'TenantPartition.cross_tenant_match_implies_not_separating' does not depend on any axioms
'TenantPartition.blind_not_separating' does not depend on any axioms
'TenantPartition.blind_admits_cross_tenant_match' depends on axioms: [propext]
'TenantPartition.unsalted_refused' does not depend on any axioms
'TenantPartition.foreign_key_refused' does not depend on any axioms
'TenantPartition.bound_key_admitted' depends on axioms: [propext]
'TenantPartition.tenant_partition_contract' depends on axioms: [propext]
'TenantPartition.taggedKey_separating' depends on axioms: [propext]
'TenantPartition.separation_instantiated' depends on axioms: [propext]
'TenantPartition.instantiated_reuse_preserved' depends on axioms: [propext]
'TenantPartition.separating_nontrivial' depends on axioms: [propext]
'TenantPartition.separated_concrete' does not depend on any axioms
'TenantPartition.reuse_concrete' does not depend on any axioms
'TenantPartition.leak_concrete' does not depend on any axioms
'TenantPartition.separating_imp_injective' does not depend on any axioms
'TenantPartition.injective_imp_separating' does not depend on any axioms
'TenantPartition.separating_iff_injective' does not depend on any axioms

## essentiality-atlas (theory/lean UalinkAtlas+UecAtlas+UalinkAtlas2)
'Ualink.containment_requires_isolation' depends on axioms: [Quot.sound, propext]
'Ualink.buggy_no_isolate_spreads' depends on axioms: [propext]
'UalinkAtlas.givenport_forces_injective' does not depend on any axioms
'UalinkAtlas.givenport_state_floor' depends on axioms: [Quot.sound, propext]
'UalinkAtlas.givenport_tight' does not depend on any axioms
'UalinkAtlas.global_kill_violates_given_port' depends on axioms: [propext]
'UalinkAtlas.podkill_satisfies_c1' does not depend on any axioms
'UalinkAtlas.underprovisioned_impossible' depends on axioms: [Quot.sound, propext]
'UalinkAtlas.two_outcomes_conflate' depends on axioms: [Quot.sound, propext]
'UalinkAtlas.three_outcomes_distinct' depends on axioms: [propext]
'UalinkAtlas.distinctness_needs_three' depends on axioms: [Quot.sound, propext]
'UecAtlas.exactonce_forces_injective' depends on axioms: [propext]
'UecAtlas.rud_state_floor' depends on axioms: [Quot.sound, propext]
'UecAtlas.no_three_state_tracker' depends on axioms: [propext]
'UecAtlas.counter_tracker_fails' depends on axioms: [Quot.sound, propext]
'UalinkAtlas2.detection_requires_redundancy' does not depend on any axioms
'UalinkAtlas2.all_valid_detects_nothing' does not depend on any axioms
'UalinkAtlas2.no_orphan_iff_no_hang' does not depend on any axioms
'UalinkAtlas2.drop_orphans' does not depend on any axioms
'UalinkAtlas2.isolate_but_drop_contained_yet_orphans' depends on axioms: [Quot.sound, propext]
'UalinkAtlas2.isolate_and_complete_satisfies_both' depends on axioms: [Quot.sound, propext]