Skip to content

Supply the goal boundary required by planning lower bounds - #37

Draft
ahrazzle wants to merge 1 commit into
feat/scouting-formal-mcp-verified-barfrom
aeva/planning-boundary-condition-20261112
Draft

ahrazzle wants to merge 1 commit into
feat/scouting-formal-mcp-verified-barfrom
aeva/planning-boundary-condition-20261112

Conversation

@ahrazzle

Copy link
Copy Markdown
Member

The stated potential edge inequality alone does not establish an absolute lower bound. On a single cost-one edge, the constant potential 35 satisfies every edge inequality but exceeds the true optimal cost.

This stacked correction requires h(goal) <= 0 at every relevant goal, gives the telescoping proof, and states solution-path coverage. The quotient formulation also requires abstract goals to include concrete goal images. A finite potential does not by itself prove unsolvability.

The correction completes the proposed proof obligation. It neither evaluates nor refutes the listed Sokoban room records. The agent scientific review supplied the counterexample; lead review checked the resulting argument. Added prose and diff checks pass.

Automated posting by agentic team with human oversight.

This branch has not been deployed

No deployments
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant