candidate onlypasspasssigmoid_logisticblock_missing_domain_guardno public savings claim

sigmoid_derivative_v0

Derivative-shaped logistic fixture with repeated sigmoid subexpressions for DAG reuse inspection.

DAG nodes

8

Replay frames

10

Reused nodes

6

Internal DAG delta

7

Obligation cards

2

Domain requirements

1

Checked witnesses

1

Blocked claims

7

Expression

(1 / (1 + exp(-x))) * (1 - (1 / (1 + exp(-x))))

x

Guard Lens

block_missing_domain_guarddepth 7

Division-like expression requires explicit denominator guard evidence before public/runtime strengthening.

matched rules

require_positive_log_domain_guard_v0

blocked claims

general EML superiorityruntime performancepublic expression claim

Tree vs DAG Boundary

Public tree SuperBEST baseline

17

Internal DAG SuperBEST candidate

10

Public tree EML baseline

90

Internal DAG EML candidate

54

Generated EML packet is candidate-only. DAG savings are internal evidence, not a public savings claim.

Inputs

Input	Unit	Range
x	dimensionless	-12 .. 12

Shared DAG Nodes

Node	Kind	Op	Reuse	Source
n0	constant	input	5	1
n1	input	input	2	x
n2	operation	neg	2	neg(n1)
n3	operation	exp	2	exp(n2)
n4	operation	add	2	add(n0, n3)
n5	operation	div	2	div(n0, n4)

Replay Frames

Tick	State	Kernel	Guard	Reason	Hash
0	INIT	eml_ir_loader	ANNOTATE	program accepted by local parser	sha256:e8a44b3439eaa91e98a6728721cdb27521ee329c56248b7ca68df70e00f5b8d5
1	READY	eml_ir_dag	ANNOTATE	DAG nodes assigned stable ids	sha256:b2daa517c8b07e4d6b50a252d8ff54560351d8ff61e05df7f8004600600b76bb
2	RUNNING	neg	PASS	static expression node	sha256:8c6bde4a0a0eb49439813cf93b974dd6eb40b2b4463b42e4719c01802e043677
3	RUNNING	exp	PASS	static expression node	sha256:74c79935f12da94a3700fcfc086f83f62a7a6dc4bd99e4a8265b0aca1f37cda3
4	RUNNING	add	PASS	static expression node	sha256:94b76129a7508938e12623371791638610033e69e88d0f57b36c84d9a7d44ccf
5	RUNNING	div	ANNOTATE	division node; denominator domain is not proven by this prototype	sha256:55e4863bc6ab42e2fb278137e8b6f696e831766b043300bac2fad2d1414cd8bd
6	RUNNING	sub	PASS	static expression node	sha256:f7bd60d45f58b08860d493a3145c8326958408f3db2342a1c94fffdbaae67dd8
7	RUNNING	mul	PASS	static expression node	sha256:9903dd874143fc7a7ca409e88e930319b61cad24c566fb5a18e5e952f2b14b34
8	END	eml_ir_runtime	ANNOTATE	output node n7 reached	sha256:a81eaba25de2a556287396a5a28455ce26c12f880a5ef7633fe46d3a0aa6c7b4
9	PARKED	eml_ir_runtime	ANNOTATE	explicit replay terminal boundary	sha256:670418e13844efc11296376b63a18c85a4f9978d0e5282d0e34df5658c2c7446

Domain Safety Lens

Unresolved obligations

1

Checked witnesses

1

Safe rewrite candidates

2

Proved by lens

1

divchecked_small_witness

denominator_nonzero

division denominator may be zero

MachLib.Real.sigmoid_denominator_nonzero

For all x, exp(-x) is positive, so 1 + exp(-x) is positive and therefore nonzero.

Introduce a guard or range proof before division.

rangedeclared_unverified

x: -12 .. 12

declared range is not runtime, hardware, or proof evidence

Attach runtime guard, sampled replay evidence, or MachLib range proof before promotion.

Blocked public claims

certified_safety_claimformal_verification_claimhardware_observedproduction_controller_claimpublic_savings_claimrange_safety_proved_claimtheorem_proof_claim

rewrite proposalcandidate_no_compiler_change

Mark this denominator_nonzero guard as proof-backed in review surfaces.

Do not change compiler lowering or public savings claims from this witness alone.

Obligation Cards

domainchecked_small_witnessdiv

denominator_nonzero

Division node requires evidence that the denominator is not zero over declared inputs/ranges.

sigmoid_derivative_v0:domain:n5:div-denominator-nonzeroMachLib.Real.sigmoid_denominator_nonzero

For all x, exp(-x) is positive, so 1 + exp(-x) is positive and therefore nonzero.

This checked witness discharges one local denominator-nonzero obligation; it is not complete EML safety, compiler correctness, or a public savings claim.

range_safetycandidate_onlysafe_range

input_range_respected

Input x declares range [-12.0, 12.0]; downstream runtime or proof work must preserve this boundary.

sigmoid_derivative_v0:range:x:declared-safe-range

This card records a declared range boundary; it is not hardware evidence or a certified safety proof.

Non-Claims

certified_safety_claim

false

compiler_behavior_changed

false

forge_behavior_changed

false

formal_verification_claim

false

hardware_observed

false

live_serial_capture_performed

false

production_controller_claim

false

public_ready

false

public_savings_claim

false

theorem_proof_claim

false